Email Gateway (Aug 19 2022 at 11:35): Email Gateway (Aug 19 2022 at 11:35):From: Yuting Wang <yuting@cs.umn.edu>
Abella version 2.0.0
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. A distinguishing feature of
Abella is that it uses generic quantification, a counterpart to the
devices of nominal logic, to reflect the treatment of binding in the
representation of syntactic objects into the reasoning process.
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
Last updated: Apr 16 2024 at 20:15 UTC