Programming Languages, Fall 2014 HW8 - Simply-Typed Lambda Calculus Due electronically on Blackboard on Tuesday November 11, 2pm. 1. Redo this question if you passed it in HW7: Draw the derivation tree for the three typing derivations on lec-7 slide 45. 2. Complete the full proof of the progress theorem on lec-7 slide 63. 3. Why in simply-typed lambda-calculus, the progress theorem has empty typing context, while the preservation theorem has a typing context? 4. Prove or give a counterexample (1-3): (1). \gamma |- t : T => |- t: T (2). |- t : T => \gamma |- t : T (3). t -> t' and \gamma |- t' : T and t does not include conditional expressions => \gamma |- t : T. 5. Give an example for each case in the proof of the substitution lemma. 6. Complete the preservation theorem proof. 7. Give an alternative proof of preservation theorem by induction on t->t'. Can you do the same for the progress theorem? Debriefing (required!): -------------------------- 1. Approximately how many hours did you spend on this assignment? 2. Would you rate it as easy, moderate, or difficult? 3. Did you work on it mostly alone, or mostly with other people? 4. How deeply do you feel you understand the material it covers (0%–100%)? 5. Any other comments?