Lecture 12: Type Preservation for Mini-ML

In this lecture we formalize another meta-theorem: the type preservation theorem for Mini-ML. We have shown the theorem already informally in lecture 3, however its formalization in LF is very short an concise, because appeals to substitution lemmas are directly supported by the logical framework.

Suggested Reading Materials:

Frank Pfenning. Computation and Deduction, Chapter 5.6

Source Code:

tp-preserve.elf