Lecture 3: Mini-ML's Typing Discipline

We discuss a type system for Mini-ML. As in the previous lecture, we define valid typing derivations through a system of inference rules, and we start with the proof of a fundamental type preservation theorem: the previously introduced operational semantics for Mini-ML preserves types.

Suggested Reading Materials:

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

Previous lecture: Lecture 2
Next lecture: Lecture 4