  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.
