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