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.
Consult the full list of examples for more details.
Abella uses a two-level logic approach to reasoning. Specifications are made in the logic of 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 2.0.8, released on October 31, 2023.
$ opam install abella |
The changelog lists significant changes between versions. The development of Abella is tracked on GitHub. If you don't mind living on the bleeding edge, you can also try using the current development snapshot, available as a tarball or a zip.
The Abella system represents a collaboration between a group at the University of Minnesota led by Gopalan Nadathur and the Parsifal team at INRIA Saclay – Île-de-France and LIX/Ecole Polytechnique led by Dale Miller. Work on Abella began as part of an NSF-funded project at the University of Minnesota aimed at developing flexible frameworks for specifying, prototyping and reasoning about computational processes. Gopalan Nadathur provided guidance in the design of that version of Abella and he and Dale Miller contributed to the specific logic that Abella is based on. The recent extension of Abella to support a richer specification logic has been the result of a transatlantic collaboration supported by the Recent Advances in Proof Theory (RAPT) Associated Team, led by Kaustuv Chaudhuri (INRIA, France); international participants of this team include a group at McGill University (Canada) led by Brigitte Pientka and a group at the University of Minnesota (USA) led by Gopalan Nadathur. Work on this extension at the University of Minnesota has been supported by the NSF under the grants CCF-0917140 and OISE-1045885. As a part of this effort, Yuting Wang designed and implemented the extension to higher-order hereditary Harrop formulas as the specification language. Subsequent work, carried out by Gopalan Nadathur and Yuting Wang and supported by the NSF Grant CCF-1617771, has resulted in the addition of a form of schematic polymorphism to Abella. The reasoning logic underlying Abella 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.
Work on Abella was funded in its early stages by a grant from Boston Scientific. Subsequent funding has been provided by the National Science Foundation through the Grants CCR-0429572, CCF-0917140, OISE-1045885, and CCF-1617771. The first two NSF grants also included supplementary funding from the OISE for Slimmer, an international collaborative project between the University of Minnesota and the Parsifal group at Ecole Polytechnique and INRIA, France. Support for the French portion of this collaboration has been provided by a sequence of Associated Team grants 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.