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.
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.
The current version of Abella is 1.3.5.
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. Todd Wilson has created several large developments in Abella and has incorporated its use into some of his graduate courses; his resulting feedback has been invaluable for increasing the usability and robustness of the system.
This work was funded in its early stages by a grant from Boston Scientific. Further funding was obtained from the NSF through the Grants CCR-0429572 and CCF-0917140. The NSF grants include 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.