Homework # 9
due November 4

Reading

Please read Chapter 15 in your textbook.

Problems

Please do the following problems

• Exercise 15.2.1
• Exercise 15.2.3

Check your answers against the solutions in the book, but do not turn in anything unless you have questions.

Please do the following problems:

• Exercise 15.5.1 (proof sketch only required)
• Exercise 15.5.2

Turn in your answers to these problems.

Proofs

Adding T-SUB drastically changes a type system, especially the canonical forms lemmas. You are provided with proof of type soundness for the simply-typed lambda calculus with records. You need to change the proofs to add subtyping.

The skeleton file for this homework, not only includes records and the proof of soundness but also the subtyping relation. You need to do several things:

• Modify the canonical forms definitions so that it handles the results of Lemma 15.3.3 and Lemma 15.3.6.
• Prove the subtyping inversion lemma (Lemma 15.3.2). (You may use the solution on page 519 to help.)
• Rewrite the canonical forms lemma to generate the updated definitions. (And fix the helper lemmas that generate typings.)
• Fix the proofs of progress and preservation to handle the updated canonical forms. (And add the cases for T-SUB, which are easy inductive cases.)

About this document