![]() |
Welcome to ftp.nluug.nl Current directory: /ftp/os/Linux/distr/salix/sbo/14.2/academic/abella/ |
|
Contents of README:Abella is an interactive theorem prover based on lambda-tree syntax. This means that Abella is well-suited for reasoning about the meta-theory of programming languages and other logical systems which manipulate objects with binding. For example, the following applications are included in the distribution of Abella. * Various results on the lambda calculus involving big-step evaluation, small-step evaluation, and typing judgments * Cut-admissibility for a sequent calculus * Part 1a and Part 2a of the POPLmark challenge * Takahashi's proof of the Church-Rosser theorem * Tait's logical relations argument for weak normalization of the simply-typed lambda calculus * Girard's proof of strong normalization of the simply-typed lambda calculus * Some ?-calculus meta-theory * Relation between ?-reduction and paths in A-calculus For Full List: http://abella-prover.org/examples/index.html Abella uses a two-level logic approach to reasoning. Specifications are made in the logic of second-order hereditary Harrop formulas using lambda-tree syntax. This logic is executable and is a subset of the AProlog language (see the Teyjus system for an implementation of this language). The reasoning logic of Abella is the culmination of a series of extensions to proof theory for the treatment of definitions, lambda-tree syntax, and generic judgments. The reasoning logic of Abella is able to encode the semantics of our specification logic as a definition and thereby reason over specifications in that logic. |
Name Last modified Size
Parent Directory -
README 17-Oct-2020 04:49 1.5K
abella.SlackBuild 10-Aug-2019 03:37 2.3K
abella.info 10-Aug-2019 03:37 312
slack-desc 10-Aug-2019 03:37 953
NLUUG - Open Systems. Open Standards
Become a member
and get discounts on conferences and more, see the NLUUG website!