diff options
| author | B. Watson <yalhcru@gmail.com> | 2020-10-11 15:38:01 -0400 |
|---|---|---|
| committer | Willy Sudiarto Raharjo <willysr@slackbuilds.org> | 2020-10-17 09:36:38 +0700 |
| commit | 1ca52074beb29e453ca41b31dae7866eb945329b (patch) | |
| tree | 0a1a2060c3a45bb8b3829e028a873cc49ff436e6 /academic | |
| parent | 48be03f9f049f0b436794a06da63d98c5d8b5e1c (diff) | |
academic/abella: Fix README.
Signed-off-by: B. Watson <yalhcru@gmail.com>
Signed-off-by: Willy Sudiarto Raharjo <willysr@slackbuilds.org>
Diffstat (limited to 'academic')
| -rw-r--r-- | academic/abella/README | 27 |
1 files changed, 15 insertions, 12 deletions
diff --git a/academic/abella/README b/academic/abella/README index a6f078794eaab..7954d1e751587 100644 --- a/academic/abella/README +++ b/academic/abella/README @@ -1,16 +1,19 @@ 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. +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 +* 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 +* 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 @@ -23,8 +26,8 @@ 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. +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. |