Programming Languages, Fall 2013
HW8 - Simply-Typed Lambda Calculus

Due electronically on Blackboard on Wednesday November 13, 11:59pm.

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.

4. give an example for each case in the proof of the substitution lemma.

5. complete the preservation theorem proof. 

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?

This section is intended to help us calibrate the homework assignments. 
Your answers to this section will *not* affect your grade; however, skipping it
will certainly do.