Abella: A System for Reasoning about Relational Specifications

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...

Full description

Saved in:
Bibliographic Details
Published in:Journal of Formalized Reasoning 2014-01, Vol.7 (2), p.1-89
Main Authors: Baelde, David, Chaudhuri, Kaustuv, Gacek, Andrew, Miller, Dale, Nadathur, Gopalan, Tiu, Alwen, Wang, Yuting
Format: Article
Language:English
Subjects:
Computer Science
Logic
Logic in Computer Science
Number theory
Programming languages
Reasoning
Syntax
Theorem proving
Citations: Items that cite this one
Online Access:Get full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary: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.
ISSN:1972-5787
1972-5787
DOI:10.6092/issn.1972-5787/4650