This repository comprises the public LFinLF development, including soundness and completeness of translation to canonical forms, family-level lambdas, and constants.

The paper draft documenting the proof structure is lfinlf.pdf.

All code by Chris Martens, 2008 - present.

Paper abstract:

We present a mechanized proof of the metatheory of LF, i.e. the decidability of typechecking and the existence and uniqueness of canonical forms. We use a syntactic approach in which we define a translation from LF to its canonical forms presentation (in which only beta-short, eta-long terms are well-formed) and prove soundness and completeness of the translation, establishing that definitional equivalence in LF corresponds to syntactic equivalence in canonical forms. Much recent work is based on the system of canonical forms and hereditary substitution presented herein; our proof also serves to reconcile that presentation with the traditional version based on definitional equivalence.