Category: Software

Abella online tutorial

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.

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.

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-β …

Continue reading

A new web-site for Abella

The Abella interactive theorem prover now has a new web-site: Relatedly, the canonical GitHub repository for Abella has been changed to: 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 …

Continue reading