Miroirs/slackbuilds_ponce
1
0
Fork 0
mirror of https://github.com/Ponce/slackbuilds synced 2024-11-22 19:44:21 +01:00
Code Issues Projects Releases Packages Wiki Activity Actions

academic/abella: Fix README.

Browse source 
Signed-off-by: B. Watson <yalhcru@gmail.com>

Signed-off-by: Willy Sudiarto Raharjo <willysr@slackbuilds.org>
This commit is contained in:
B. Watson 2020-10-11 15:38:01 -04:00 committed by Willy Sudiarto Raharjo
parent 48be03f9f0
commit 1ca52074be
No known key found for this signature in database
GPG key ID: 3F617144D7238786
1 changed files with 15 additions and 12 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

27
academic/abella/README
View file

@ -1,16 +1,19 @@
Abella is an interactive theorem prover based on lambda-tree syntax. Abella is an interactive theorem prover based on lambda-tree syntax.
This means that Abella is well-suited for reasoning about the meta-theory This means that Abella is well-suited for reasoning about the
of programming languages and other logical systems which manipulate meta-theory of programming languages and other logical systems
objects with binding. For example, the following applications are included which manipulate objects with binding. For example, the following
in the distribution of Abella. 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 * Cut-admissibility for a sequent calculus
* Part 1a and Part 2a of the POPLmark challenge * Part 1a and Part 2a of the POPLmark challenge
* Takahashi's proof of the Church-Rosser theorem * Takahashi's proof of the Church-Rosser theorem
* Tait's logical relations argument for weak normalization of the simply-typed lambda calculus * Tait's logical relations argument for weak normalization of the
* Girard's proof of strong normalization of the simply-typed lambda calculus simply-typed lambda calculus
* Girard's proof of strong normalization of the simply-typed lambda
calculus
* Some ?-calculus meta-theory * Some ?-calculus meta-theory
* Relation between ?-reduction and paths in A-calculus * 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 AProlog language (see the Teyjus system for an implementation of this
language). language).
The reasoning logic of Abella is the culmination of a series of extensions The reasoning logic of Abella is the culmination of a series
to proof theory for the treatment of definitions, lambda-tree syntax, of extensions to proof theory for the treatment of definitions,
and generic judgments. The reasoning logic of Abella is able to encode lambda-tree syntax, and generic judgments. The reasoning logic of
the semantics of our specification logic as a definition and thereby Abella is able to encode the semantics of our specification logic as a
reason over specifications in that logic. definition and thereby reason over specifications in that logic.