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 language | English (US) |
|---|---|
| Pages (from-to) | 1-89 |
| Number of pages | 89 |
| Journal | Journal of Formalized Reasoning |
| Volume | 7 |
| Issue number | 2 |
| State | Published - 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.