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.
Category: Software
May 16
Yuting Wang and Mary Southern start their internships
This summer, Parsifal is hosting two interns from the University of Minnesota: Yuting Wang and Mary Southern. They will be working on the theory and implementation of Abella.
Jul 21
Abella 2.0.0 released
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-β …
Oct 29
A new web-site for Abella
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 …
