Homework # 7
due October 25

Reading

Please read Chapter 11 in your textbook.

Problems

Please do the following problems

1. Enums can be seen as a variation on ``variants''. Write new evaluation and typing rules (on paper, not SASyLF) for a type T written like [red,green,blue] with new syntax:
   
   $$\begin{array}{ccl} t &\mathtt{::=}& \ldots \\ &\mid& \tex... ...$\ -> $t_1$\ \vert \ldots\ \vert $n_m$\ -> $t_m$}. \end{array}$$
   
   

2. Explain informally why these type rules should be sound. (You might wish to write the SASyLF proofs for sum types first; otherwise your explanations may not be convincing!)

Proofs

Modify the proofs of type soundness of the simply-typed lambda calculus with ``unit'' types to add sums (See Figure 11-9). A skeleton file is available which gives the syntax. This file will only work with version ``SASyLF 1.0.2 (uwm 2)'' or later. You may need to fetch a new JAR file. Your evaluation and types rules should follow the book as closely as possible.

Extra

Optionally, add type, evaluation and proof rules for products too. The syntax is defined already.

Graduate Students

Read Chapter 12.

Could the proofs in the this chapter be expressed in (i) Twelf, (ii) Coq or (iii) Isabelle/HOL ? What about SASyLF? Explain! Give references/URLs to support your argument.

Which of the extensions in Chapter 11 (1,2,3,4,5,6,7,8,9,10,11,12) preserve normalization? For each, explain in your own words and/or give references/URLs to support your answer.

About this document