Description

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
• Tait's logical relations argument for normalization of the simply-typed lambda-calculus

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 λProlog 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. More information about this approach and the logics involved is available in the publications section.

For an introduction to using Abella, please read this walkthrough of an example Abella session which covers a proof of subject reduction in the lambda-calculus.

Download

The current version of Abella is 1.1.

• Download and compile the source tarball. This requires an OCaml installation.
• For Windows, a binary package is available.

The changelog lists significant changes between versions.

Documentation

• New users are encouraged to read the walkthrough of an example Abella session.
• After the first walkthrough, users are encouraged to continue with the advanced walkthrough.
• After both walkthroughs, users should be ready to understand any of the examples included in the distribution of Abella.
• The Abella reference guide has a brief description of syntax, commands, and tactics.
• The Abella mailing list is open for questions and discussions.

User Contributed Proofs

• Randy Pollack has contributed a formalization of the Church-Rosser theorem using Takahashi's proof based on complete developments.

Some Relevant Publications

Reasoning in Abella about structural operational semantics specifications, by Andrew Gacek, Dale Miller, and Gopalan Nadathur, Available from http://arxiv.org/abs/0804.3914. To appear in LFMTP'08, 2008. [ bib | slides | .pdf ]

The Abella interactive theorem prover (system description), by Andrew Gacek, Available from http://arxiv.org/abs/0803.2305. To appear in IJCAR'08, 2008. [ bib | .pdf ]

Combining generic judgments with recursive definitions, by Andrew Gacek, Dale Miller, and Gopalan Nadathur, 23th Symposium on Logic in Computer Science (F. Pfenning, ed.), IEEE Computer Society Press, 2008, To appear. [ bib | slides | .pdf ]

A proof theory for generic judgments, by Dale Miller and Alwen Tiu, ACM Transactions on Computational Logic 6 (2005), no. 4, 749-783. [ bib | .pdf ]

Reasoning with higher-order abstract syntax in a logical framework, by Raymond McDowell and Dale Miller, ACM Transactions on Computational Logic 3 (2002), no. 1, 80-136. [ bib | .pdf ]

An Overview of λProlog, by Gopalan Nadathur and Dale Miller, Fifth International Logic Programming Conference (Seattle), MIT Press, August 1988, pp. 810-827. [ bib | .pdf ]

Support & Contact Information

Abella is under active development. For support, questions, or suggestions please use the Abella mailing list or contact Andrew Gacek.

Acknowledgments

This work has been supported by INRIA through the "Equipes Associées" Slimmer, by the NSF Grants OISE-0553462 (IRES-REUSSI) and CCR-0429572 and by a grant from Boston Scientific. Opinions, findings, and conclusions or recommendations expressed in this work are those of the authors and do not necessarily reflect the views of the National Science Foundation.