Section: New Software and Platforms

Abella

Functional Description

Abella is an interactive theorem prover for reasoning about computations given as relational specifications. Abella is particuarly well suited for reasoning about binding constructs.

In 2015, Abella has been extended with

• support for polymorphic definitions and theorems;

• schemas and automatically derived theorems about them;

• the ability to record and replay automated search;

• a number of new examples from process calculi, including a contributed example from Horace Blanc about relating the $\pi$-calculus and the $\lambda$-calculus.

One further development is that Abella can now be compiled into JavaScript and run completely inside any modern browser, thanks to the js_of_ocaml compiler from OCaml bytecode to JavaScript. We expect this to become rather crucial in popularization of Abella, particularly in a pedagogical context, since it does not require any local software installation—just a modern web browser.

• Participants: Dale Miller, Kaustuv Chaudhuri, Horace Blanc

• Partner: Department of Computer Science and Engineering, University of Minnesota

• Contact: Kaustuv Chaudhuri

• URL: http://abella-prover.org/

• Online version: http://abella-prover.org/tutorial/try