diff options
Diffstat (limited to 'academic/abella/README')
| -rw-r--r-- | academic/abella/README | 25 |
1 files changed, 25 insertions, 0 deletions
diff --git a/academic/abella/README b/academic/abella/README new file mode 100644 index 0000000000..aa13f891cd --- /dev/null +++ b/academic/abella/README @@ -0,0 +1,25 @@ +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. |