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.

Examples

Type-uniqueness for the simply typed λ-calculus
For a specification of the typing judgement for the simply typed lambda calculus, we show both that every term has a unique type, and that there is a unique derivation for the type of every term.
Isomorphism of De Bruijn and HOAS representations of λ-terms
This is an LF version of the existing isomorphism theorem from the mainline Abella. The interesting theorems are ho2db_det1_simple and ho2db_det3_simple that show that the same ho2db type family functions as a witness for both directions of the isomorphism. For those who are aware of Twelf and Beluga, note that this development uses a context relation ctx that is not regular: it counts the number of elements of the context, but regular languages cannot count.
Cut-elimination for minimal intuitionistic logic
This development follows the format of the standard cut-elimination example of Abella, except it uses the LF typing derivation of formulas directly to reason about the structure of the cut-formula, instead of using an auxiliary definition.
Divergence of Ω using co-induction
We show by co-induction that the term (λx. x x)(λx. x x) diverges. This simple example illustrates that Abella's standard co-induction mechanism can reason about LF specifications with no problem.
Progress for an intrinsically encoded λ-calculus
In contrast to the progress theorems for extrinsic typing, such as in the existing solution to the POPLMark 2a challenge, using an intrinsic encoding that can only describe well-typed λ-terms we obtain an extremely compact proof of progress.