blob: aa13f891cdcc608d6d4367b4243e577c7d936730 (
plain)
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.
|
