Abella: A System for Reasoning about Relational Specifications
Baelde, David ; Chaudhuri, Kaustuv ; Gacek, Andrew ; Miller, Dale ; Nadathur, Gopalan ; Tiu, Alwen ; Wang, Yuting
Journal of Formalized Reasoning, Volume 7 (2014), / Harvested from Journal of Formalized Reasoning

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.

Published online : 2014-01-01
DOI : https://doi.org/10.6092/issn.1972-5787/4650
     title = {Abella: A System for Reasoning about Relational Specifications},
     journal = {Journal of Formalized Reasoning},
     volume = {7},
     year = {2014},
     doi = {10.6092/issn.1972-5787/4650},
     language = {EN},
     url = {http://dml.mathdoc.fr/item/4650}
Baelde, David; Chaudhuri, Kaustuv; Gacek, Andrew; Miller, Dale; Nadathur, Gopalan; Tiu, Alwen; Wang, Yuting. Abella: A System for Reasoning about Relational Specifications. Journal of Formalized Reasoning, Volume 7 (2014) . doi : 10.6092/issn.1972-5787/4650. http://gdmltest.u-ga.fr/item/4650/