[TYPES/announce] Abella version 2.0.0 -- new major release

[Kaustuv Chaudhuri]

   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.


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 nomalization 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

  - The Parsifal team at INRIA Saclay
    http://team.inria.fr/parsifal