Abella (original) (raw)

Abella Logo

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.

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.

Some of the design differences between Abella and proof assistants such as Rocq and Agda are describe in Miller's talk Proof Theory and Type Theory: Distinct Foundations for Designing Proof Assistants presented at a workshop in Banff in June 2025.

Download

The current version of Abella is 2.0.8, released on October 31, 2023.

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.

Documentation

Support

Some Relevant Publications

Contributors

History

The Abella system represents a collaboration between a group at the University of Minnesota led by Gopalan Nadathur and the Parsifal team atINRIA 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.

Funding

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.