Abella: A System for Reasoning about Relational Specifications


  • David Baelde LSV, CNRS & ENS de Cachan
  • Kaustuv Chaudhuri INRIA, France.
  • Andrew Gacek Rockwell Collins, USA
  • Dale Miller Inria & LIX/Ecole polytechnique, France
  • Gopalan Nadathur University of Minnesota, USA
  • Alwen Tiu Nanyang Technological University, Singapore
  • Yuting Wang University of Minnesota




The Abella interactive theorem prover is based on an intuitionistic logic that allows for inductive and co-inductive reasoning over relations. Abella supports the λ-tree approach to treating syntax containing binders: it allows simply typed λ-terms to be used to represent such syntax and it provides higher-order (pattern) unification, the nabla quantifier, and nominal constants for reasoning about these representations. As such, it is a suitable vehicle for formalizing the meta-theory of formal systems such as logics and programming languages. This tutorial exposes Abella incrementally, starting with its capabilities at a first-order logic level and gradually presenting more sophisticated features, ending with the support it offers to the two-level logic approach to meta-theoretic reasoning. Along the way, we show how Abella can be used prove theorems involving natural numbers, lists, and automata, as well as involving typed and untyped λ-calculi and the π-calculus.




How to Cite

Baelde, D., Chaudhuri, K., Gacek, A., Miller, D., Nadathur, G., Tiu, A., & Wang, Y. (2014). Abella: A System for Reasoning about Relational Specifications. Journal of Formalized Reasoning, 7(2), 1–89. https://doi.org/10.6092/issn.1972-5787/4650