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.

This requires: ocaml-findlib, ocamlbuild

Maintained by: Jefferson Rocha

Keywords: abella,interactive,lambda-tree,interactive theorem

ChangeLog: abella

**Homepage:**

http://abella-prover.org/

abella-2.0.6.tar.gz (077cb3fbbdf35159e4b8860faf431c6a)

**Download SlackBuild:**

abella.tar.gz

abella.tar.gz.asc (FAQ)

*(the SlackBuild does not include the source)*

Individual Files: |

• README |

• abella.SlackBuild |

• abella.info |

• slack-desc |

© 2006-2021 SlackBuilds.org Project. All rights reserved.

Slackware® is a registered trademark of
Patrick Volkerding

Linux® is a registered trademark of
Linus Torvalds