Reasoning about LF Specifications in Abella

This web-page documents the experimental lf branch of Abella, which we call Abella/LF. The theoretical basis of the branch is described in the following paper:

A Two-Level Logic Approach to Reasoning about Typed Specification Languages by Mary Southern and Kaustuv Chaudhuri,
IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS-34), December 2014.

The links below are to the HTML version of some example Abella/LF developments. The actual Abella sources are also linked therefrom, but the development can be browsed without running Abella yourself.

Note: the development below requires the lf branch of Abella from its Git repository. This version of Abella is also available as a zip from Github.


Last updated: 2014-10-16 12:06:46+0200