Mechanizing the Metatheory of LF

Christian Urban, James Cheney, Stefan Berghofer

LF is a dependent type theory in which many other formal systems can be conveniently embedded. However, correct use of LF relies on nontrivial metatheoretic developments such as pr…