Type safety

Remarks

Progress is proved by induction on the typing derivation, using a canonical forms lemma. The lemma says that a closed value of type $\mathsf{Bool}$ is $\mathsf{true}$ or $\mathsf{false}$, and a closed value of type $\sigma \to \tau$ is an abstraction. Preservation is proved by induction on the derivation of $t \to t'$, and its key case is a substitution lemma: if $\Gamma, x : \sigma \vdash t : \tau$ and $\Gamma \vdash u : \sigma$, then $\Gamma \vdash t[u/x] : \tau$. The term $\mathsf{if}\ (\lambda x{:}\mathsf{Bool}.\, x)\ \mathsf{then}\ \mathsf{true}\ \mathsf{else}\ \mathsf{false}$ is stuck: it is not a value and no rule applies. The theorem predicts this, since the term has no type: the condition is a function, not a $\mathsf{Bool}$. Progress needs the empty context: the open term $x$ with $x : \mathsf{Bool}$ is well typed, not a value and cannot step.

Going deeper

For a student

This syntactic form of type safety, split into progress and preservation, is due to Wright and Felleisen. The same two lemmas are the standard way to prove safety of any type system given by an operational semantics. Safety does not say that programs terminate: it also holds for languages with general recursion, where a safe program may run forever. For the simply typed calculus, strong normalization adds termination on top of safety.