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-β via paths illustrates the use of reasoning on higher-order contexts.
Much of the development of this release has been done by Yuting Wang during his internship at Parsifal as part of the RAPT Associated Team. Other major contributors to this release include Kaustuv Chaudhuri (Parsifal) and Andrew Gacek (Rockwell Collins, USA).
For the logicians, the new extensions of Abella are documented in the following paper to appear at PPDP 2013 later this year:
- Y. Wang, K. Chaudhuri, A. Gacek, and G. Nadathur, Reasoning about Higher-Order Relational Specifications, to appear at PPDP 2013, September 2013
