Transporting Theorems about Typeability in LF Across Schematically Defined Contexts

Chase Johnson, Gopalan Nadathur

The dependently-typed lambda calculus LF is often used as a vehicle for formalizing rule-based descriptions of object systems. Proving properties of object systems encoded in this…