Homework # 9
due November 8

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. (This work is done for you in comments.)
• 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.)

Extra

Prove soundness of subtyping with references, using the rule on page 198. (I don't recommend this--I haven't done it myself.)

Graduate Students

The textbook gives three different ways in which records can be subtyped. Can you find a widely used programming language that accepts all three? Describe four widely used languages that have something approximating records and indicate which of the subtyping rules apply, and explain how.

About this document