Lecture 4: Type Preservation for Mini-ML

We continue our discussion of the type system for Mini-ML from the previous lecture and finish the type preservation theorem. One important lemma in this proof is a substitution lemma which we first generalize before we can prove it by induction.

Suggested Reading Materials:

Frank Pfenning. Computation and Deduction, Chapter 2.6 - End of Chapter 2.

Previous lecture: Lecture 3
Next lecture: Lecture 5