The Coq mailing list

[Yuting Wang <yuting AT cs.umn.edu>]

Abella version 2.0.0
 
  http://abella-prover.org
 
We are pleased to announce a new major release of the Abella proof-assistant. Abella is designed to reason about computational systems specified relationally and using lambda-tree syntax, also known as higher-order abstract syntax. Another key feature of Abella is that it uses two different but interacting logics, one tuned to specifying formal systems and the other designed for reasoning about such specifications.
 
 
The key features of this release include:
 
  - support for higher-order specifications

  - the ability to reason inductively on dynamic contexts
 
These features remove many limitations in earlier versions of Abella.
 

Abella excels at specifying and reasoning about such systems as programming languages, process calculi, proof systems, and many kinds of lambda calculi. Abella uses Church's simple theory of types, and is based on the two-level logic approach that consists of:
 
  - a specification logic, here the logic of higher-order hereditary
    Harrop formulas (HH), to encode the objects and computations, and

  - a reasoning logic that has support for inductive and co-inductive
    definitions, generic quantification, and the ability to prove
    theorems by induction or co-induction. This logic is used to
    reason about the encoded objects and computations in terms of
    the HH proof system.
 
 
A number of example developments are available from the Abella
web-site. These include:

  - Solutions to the POPLmark challenge, including a new higher-order
    solution to a variant of challenge 1a

  - Proofs of strong normalization for typed lambda calculi using
    different methods

  - Formalized meta-theory of the lambda calculus: this release
    includes a new characterization of equivalence-upto-beta in
    terms of an inductive notion of "paths"

  - Highly declarative formalization of bisimulation and its
    properties in process calculi, including calculi with binding and
    mobility such as the pi calculus.
 
 
Abella is developed as part of a transatlantic collaboration between INRIA Saclay (in the Parsifal team) in France and the University of Minnesota in the USA. The principal developers of Abella are Andrew Gacek (Rockwell Collins, USA), Yuting Wang (University of Minnesota), and Kaustuv Chaudhuri (INRIA, France), with a number of other contributors that are listed on the main web-site.

 
Abella is actively used in a number of research projects around the world related to the formalized meta-theory of deductive and computational systems.

 
Some relevant URLs:

  - The GitHub repository for Abella
    https://github.com/abella-prover/abella

  - The Abella discussion list
    http://groups.google.com/group/abella-theorem-prover