A tutorial for Abella was recently presented at CADE 25 in Berlin by K. Chaudhuri and Gopalan Nadathur. The slides (PDF) are available online. All the demonstration examples in the tutorial can be viewed and executed online using the new experimental Abella in the Browser plugin.
After over a year of development, Abella 2.0.0 has been released! The new release removes all the arbitrary restrictions on the specification logic, which is now fully higher-order. As a result, this version of Abella allows backchaining in specification contexts, and therefore also supports inductive specifications of dynamic extensions of programs. This example characterizing equivalence-upto-β …
The Abella interactive theorem prover now has a new web-site: http://abella-prover.org. Relatedly, the canonical GitHub repository for Abella has been changed to: http://github.com/abella-prover/abella. Kaustuv Chaudhuri (Parsifal) and Yuting Wang (Univ. Minnesota) join Andrew Gacek (Rockwell Collins) as maintainers of Abella. A cumulative new release of Abella is planned during the remaining months of 2012. A …