[TYPES/announce] Abella: Interactive theorem proving with lambda-tree syntax

[Andrew Gacek]

I am happy to announce the public release of Abella, an interactive
theorem prover that is designed to reason about structural operational
semantics style specifications of dynamic and static properties of an
object language. 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. The most recent successes include solutions to parts 1a
and 2a of the POPLmark challenge and a proof of normalizability for
the simply-typed lambda-calculus using a logical relations argument in
the style of Tait.

Abella is a realization of a two-level logic approach to reasoning in
its application domain. One level is defined by a specification logic
that supports a transparent encoding of structural operational
semantics rules. This logic is a subset of the language of Lambda
Prolog and can therefore be animated. The second level, that is called
the reasoning logic, embeds the specification logic via definitions of
atomic judgments; complicated properties involving these atomic
judgments can then be stated and proved in the reasoning logic. An
important characteristic of Abella is that it supports the use of
lambda-tree syntax in both the specification and the reasoning logics
in providing treatments of binding constructs in object language
syntax. Reasoning over lambda-tree syntax is supported by the nabla
quantifier introduced by  Miller and Tiu and the notion of generic
judgments. Abella also incorporates a newly developed extension to the
notion of definitions of McDowell and Miller that uses the nabla
quantifier to encode stronger properties about atomic judgments that
are often essential in reasoning tasks.

For more information, the Abella website includes walkthroughs,
examples, downloads, and related publications:

  http://abella.cs.umn.edu/

The distribution material also contains proofs of the various example
properties mentioned in this message.

I welcome your feedback and any questions you may have. Please contact
me directly at andrew.gacek at gmail.com.

Thank you,
Andrew Gacek