Abella 1.3
Andrew Gacek
I'm happy to announce the release of Abella 1.3. The most significant
change in this version of Abella is the inclusion of simple typing.
The typing system is documented in the Abella reference guide and
manifest in all of the examples included with Abella. Other changes
include the following.
* The syntax of definitions has been changed so that all clauses
are listed in a single command. See examples/type-uniq. for an
example.
* Added the backchain tactic which is in some sense dual to the
apply tactic. The backchain tactic applies a lemma (or hypothesis) to
the current goal and produces new subgoals for each of the hypotheses
to the lemma.
* Added the permute tactic which permutes the nominal constants in
a hypothesis or goal.
* Improved the handling of non-Llambda unification and
constraints. After case analysis, lingering constraints are added as
equality hypotheses.
* Added Quit command.
* Added a development of some meta-theory of the pi-calculus
contributed by Dale Miller.
* Added a development which showcases some of the higher-order
logic programming features which are available in Abella's
specification logic.
The new version is available as always from
-Andrew