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

34 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

Copyright:
Copyright 2017 Elsevier B.V., All rights reserved.

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

Cite this