Skip to Main content Skip to Navigation
Journal articles

Abella: A System for Reasoning about Relational Specifications

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 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.
Document type :
Journal articles
Complete list of metadatas

https://hal.inria.fr/hal-01102709
Contributor : Kaustuv Chaudhuri <>
Submitted on : Tuesday, January 13, 2015 - 1:27:13 PM
Last modification on : Thursday, July 2, 2020 - 5:26:02 PM
Long-term archiving on: : Tuesday, April 14, 2015 - 10:51:08 AM

Files

abella-tutorial.pdf
Files produced by the author(s)

Licence


Distributed under a Creative Commons Attribution - NoDerivatives 4.0 International License

Identifiers

Collections

Citation

David Baelde, Kaustuv Chaudhuri, Andrew Gacek, Dale Miller, Gopalan Nadathur, et al.. Abella: A System for Reasoning about Relational Specifications. Journal of Formalized Reasoning, ASDD-AlmaDL, 2014, Special Issue: User Tutorials 2, 7 (2), pp.1-89. ⟨10.6092/issn.1972-5787/4650⟩. ⟨hal-01102709⟩

Share

Metrics

Record views

1426

Files downloads

425