# Abella: A System for Reasoning about Relational Specifications

## D. Baelde, K. Chaudhuri, A. Gacek, D. Miller, G. Nadathur, A. Tiu, Y. Wang

### Journal of Formalized Reasoning. Vol 7, No 2, pp. 1-89

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.