Lecture 12: Type preservation.

After formally specifying Mini-Haskell, we can be be investigate its properties. In this lecture we look at the operational semantics of Mini-Haskell and notice that it is type preserving. This means that evaluating a well-typed program will result in a well-typed value.

The result does not follow directly. We will prove a weakening lemma and define a typing discipline for environments.

Further Reading:

Previous lecture: Lecture 11
Next lecture: Lecture 13