Abella: A system for reasoning about relational specifications

David Baelde, Andrew Gacek, Gopalan Nadathur, Yuting Wang, Kaustuv Chaudhuri, Dale Miller, Alwen Tiu

Research output: Contribution to journalArticlepeer-review

48 Scopus citations

Abstract

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 ∇ 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 incre- mentally, 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.

Original languageEnglish (US)
Pages (from-to)1-89
Number of pages89
JournalJournal of Formalized Reasoning
Volume7
Issue number2
StatePublished - 2015

Bibliographical note

Funding Information:
Acknowledgements: We thank Andrea Asperti, Roberto Blanco, Zakaria Chihani and Claudio Sacerdoti Coen for their comments on drafts of this tutorial. This work has been partially supported by the NSF Grants OISE-1045885 (REUSSI-2) and CCF-0917140, by the INRIA Associated Teams Slimmer and rapt, and by the ERC Advanced Grant ProofCert. Opinions, findings, and conclusions or recommendations expressed in this paper are those of the authors and do not necessarily reflect the views of the National Science Foundation, the European Research Council, INRIA, ENS Cachan, Nanyang Technological University, or Rockwell Collins.

Funding Information:
We thank Andrea Asperti, Roberto Blanco, Zakaria Chihani and Claudio Sacerdoti Coen for their comments on drafts of this tutorial. This work has been partially supported by the NSF Grants OISE-1045885 (REUSSI-2) and CCF-0917140, by the INRIA Associated Teams Slimmer and rapt, and by the ERC Advanced Grant ProofCert. Opinions, findings, and conclusions or recommendations expressed in this paper are those of the authors and do not necessarily re ect the views of the National Science Foundation, the European Research Council, INRIA, ENS Cachan, Nanyang Technological University, or Rockwell Collins.

Fingerprint

Dive into the research topics of 'Abella: A system for reasoning about relational specifications'. Together they form a unique fingerprint.

Cite this