Abella: A System for Reasoning about Relational Specifications

David Baelde 1 Kaustuv Chaudhuri 2, * Andrew Gacek 3 Dale Miller 2 Gopalan Nadathur 4 Alwen Tiu 5 Yuting Wang 4
* Auteur correspondant
2 PARSIFAL - Proof search and reasoning with logic specifications
LIX - Laboratoire d'informatique de l'École polytechnique [Palaiseau], Inria Saclay - Ile de France, X - École polytechnique, CNRS - Centre National de la Recherche Scientifique : UMR7161
5 School of Computer Engineering
NTU - School of Computer Engineering [Singapore]
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.
Type de document :
Article dans une revue
Journal of Formalized Reasoning, ASDD-AlmaDL, 2014, Special Issue: User Tutorials 2, 7 (2), pp.1-89. 〈10.6092/issn.1972-5787/4650〉
Liste complète des métadonnées

Contributeur : Kaustuv Chaudhuri <>
Soumis le : mardi 13 janvier 2015 - 13:27:13
Dernière modification le : jeudi 10 mai 2018 - 02:07:00
Document(s) archivé(s) le : mardi 14 avril 2015 - 10:51:08


Fichiers produits par l'(les) auteur(s)


Distributed under a Creative Commons Paternité - Pas de modifications 4.0 International License



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〉



Consultations de la notice


Téléchargements de fichiers