academic/abella: Added (interactive theorem prover).

Signed-off-by: Willy Sudiarto Raharjo <willysr@slackbuilds.org>

1 files changed, 25 insertions, 0 deletions

diff --git a/academic/abella/README b/academic/abella/README
new file mode 100644
index 0000000000000..aa13f891cdcc6
--- /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.