@article{JFR4650,
    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 {$\lambda$}-tree approach to treating syntax containing binders: it allows simply typed {$\lambda$}-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 {$\lambda$}-calculi and the {$\pi$}-calculus.},
    Author = {Baelde, David and Chaudhuri, Kaustuv and Gacek, Andrew and Miller, Dale and Nadathur, Gopalan and Tiu, Alwen and Wang, Yuting},
    File = {Abella - A System for Reasoning about Relational Specifications - document - a - a - a - l.pdf},
    ISSN = {1972-5787},
    Journal = {Journal of Formalized Reasoning},
    Number = {2},
    Pages = {1--89},
    Title = {Abella: A System for Reasoning about Relational Specifications},
    URL = {https://jfr.unibo.it/article/view/4650},
    Volume = {7},
    Year = {2014},
    bdsk-url-1 = {https://jfr.unibo.it/article/view/4650},
    bdsk-url-2 = {https://doi.org/10.6092/issn.1972-5787/4650},
    date-added = {2020-03-10 11:07:53 +0100},
    date-modified = {2020-03-10 11:07:53 +0100},
    doi = {10.6092/issn.1972-5787/4650}
}

@article{JFR4650, 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 {$\lambda$}-tree approach to treating syntax containing binders: it allows simply typed {$\lambda$}-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 {$\lambda$}-calculi and the {$\pi$}-calculus.}, Author = {Baelde, David and Chaudhuri, Kaustuv and Gacek, Andrew and Miller, Dale and Nadathur, Gopalan and Tiu, Alwen and Wang, Yuting}, File = {Abella - A System for Reasoning about Relational Specifications - document - a - a - a - l.pdf}, ISSN = {1972-5787}, Journal = {Journal of Formalized Reasoning}, Number = {2}, Pages = {1--89}, Title = {Abella: A System for Reasoning about Relational Specifications}, URL = {https://jfr.unibo.it/article/view/4650}, Volume = {7}, Year = {2014}, bdsk-url-1 = {https://jfr.unibo.it/article/view/4650}, bdsk-url-2 = {https://doi.org/10.6092/issn.1972-5787/4650}, date-added = {2020-03-10 11:07:53 +0100}, date-modified = {2020-03-10 11:07:53 +0100}, doi = {10.6092/issn.1972-5787/4650} }