2020-01-26 09:50:09 +01:00
|
|
|
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.
|
2019-08-09 20:23:33 +02:00
|
|
|
|
|
|
|
|
* 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
|
|
|
|
|
|
2020-01-26 09:50:09 +01:00
|
|
|
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.
|
