CMSC 221/321
Homework set 5
Due: Friday, Nov 11, 2011 at midnight

5.0 [Reading] Lectures 8 and 9.

5.1 [35]. Give a full and rigorous proof of the Substitution Lemma
(Lemma 4.9, Lecture 8), using the proof of the Substitution Lemma for
the ok judgement (Lemma 4.4, Lecture 7) as the template.

5.2 [25]. Prove Lemma 4.11 (Lecture 8), showing that an expression
(in a given type context) has a unique type.

5.2 [10]. Prove part (5) of the Inversion Lemma (Lemma 4.8, Lecture
8).

5.3 [10] Give an informal proof of Lemma 4.10(3) (cannonical forms
for function types).