SlackBuilds Repository

14.2 > Academic > abella (2.0.6)

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
* Some ?-calculus meta-theory
* Relation between ?-reduction and paths in A-calculus

For Full List:

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

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.

This requires: ocaml-findlib, ocamlbuild

Maintained by: Jefferson Rocha
Keywords: abella,interactive,lambda-tree,interactive theorem
ChangeLog: abella


Source Downloads:
abella-2.0.6.tar.gz (077cb3fbbdf35159e4b8860faf431c6a)

Download SlackBuild:
abella.tar.gz.asc (FAQ)

(the SlackBuild does not include the source)

Individual Files:

Validated for Slackware 14.2

See our HOWTO for instructions on how to use the contents of this repository.

Access to the repository is available via:
ftp git cgit http rsync

© 2006-2021 Project. All rights reserved.
Slackware® is a registered trademark of Patrick Volkerding
Linux® is a registered trademark of Linus Torvalds