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
• 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

The full list of examples is available here.

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.3.2.

• 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.

Some Relevant Publications

• A two-level logic approach to reasoning about computations, by Andrew Gacek, Dale Miller, and Gopalan Nadathur, Submitted 16 November, November 2009. [ bib | arXiv | .pdf ]
• A framework for specifying, prototyping, and reasoning about computational systems, by Andrew Gacek, Ph.D. thesis, University of Minnesota, September 2009. [ bib | arXiv | slides | .pdf ]
• Nominal abstraction, by Andrew Gacek, Dale Miller, and Gopalan Nadathur, Submitted 4 August, August 2009. [ bib | arXiv | .pdf ]
• The Abella interactive theorem prover (system description), by Andrew Gacek, Proceedings of IJCAR 2008 (A. Armando, P. Baumgartner, and G. Dowek, eds.), Lecture Notes in Artificial Intelligence, vol. 5195, Springer, August 2008, pp. 154-161. [ bib | slides | .pdf ]
• Combining generic judgments with recursive definitions, by Andrew Gacek, Dale Miller, and Gopalan Nadathur, Proceedings of LICS 2008 (F. Pfenning, ed.), IEEE Computer Society Press, June 2008, pp. 33-44. [ bib | slides | .pdf ]
• Reasoning in Abella about structural operational semantics specifications, by Andrew Gacek, Dale Miller, and Gopalan Nadathur, International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice (LFMTP 2008) (A. Abel and C. Urban, eds.), Electronic Notes in Theoretical Computer Science, no. 228, 2008, pp. 85-100. [ 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 ]

Contributors

The Abella system is a component of an ongoing project at the University of Minnesota that seeks to develop flexible frameworks for specifying, prototyping and reasoning about computational processes. The chief designer and implementor of Abella is Andrew Gacek who is also a significant player in the development of the logical foundations of the system. Gopalan Nadathur, who leads the larger project at the University of Minnesota, has provided guidance in the design of Abella and he and Dale Miller have contributed to the specific logic that Abella is based on. This logic builds on the previous work of several people, most prominently Alwen Tiu, Dale Miller and Raymond McDowell. Work on Abella has benefited from several comments and encouragement provided by Alwen Tiu and David Baelde who have also been amongst the first users of the system.

Grant Support

This work was funded in its early stages by a grant from Boston Scientific. Further funding was obtained from the NSF through the Grant CCR-0429572. The NSF grant includes support for Slimmer, a collaborative project with the Parsifal group at INRIA, France under whose aegis this work falls. Support for the French portion of this collaboration is provided by "Equipes Associées" award from INRIA. 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 or the other funding sources.

Support & Contact Information

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