Table of Contents
1 HW2
1.1 Part 1
Extend your model from HW1 with a type system.
1.2 Part 2
Prove the following cases of progress and preservation:
- lambda and application
- bool and If
- Dictionaries and Projection
- nat-fold
You may modify your model to do this if necessary.
If you need any additional lemmas, you may state them and use them without proofs (as long as they are not substantially similar to the lemma you are proving).