# The Abella interactive theorem prover (system description)

## A. Gacek

### Proceedings of IJCAR 2008 (A. Armando, P. Baumgartner, and G. Dowek, eds.), Lecture Notes in Artificial Intelligence, vol. 5195, Springer, August 2008, pp. 154-161

Abella is an interactive system for reasoning about aspects of object
languages that have been formally presented through recursive rules
based on syntactic structure. Abella utilizes a two-level logic
approach to specification and reasoning. One level is defined by a
specification logic which supports a transparent encoding of
structural semantics rules and also enables their execution. The
second level, called the reasoning logic, embeds the specification
logic and allows the development of proofs of properties about
specifications. An important characteristic of both logics is that
they exploit the lambda tree syntax approach to treating binding in
object languages. Amongst other things, Abella has been used to prove
normalizability properties of the lambda calculus, cut admissibility
for a sequent calculus and type uniqueness and subject reduction
properties. This paper discusses the logical foundations of Abella,
outlines the style of theorem proving that it supports and finally
describes some of its recent applications.