CIS 500 — Software FoundationsHomework Assignment 7Extensions of simple typesDue: Monday, October 30, 2006, by noonSubmit your solutions as hw7, for example using the command:~cis500/bin/cis500submit hw7 hw7.pdf1 Exercise For each new extension to the simply-typed lambda calculus (λ→) with error (see Figure14-1), we must add new rules to propagate the error. For example, in the language λ→+ error +booleans, we need the rule:if error then t2else t3−→ errorWhat new rules do we need for λ→+ error + unit + references, i.e., the language of Figure 13-1extended with error?2 Exercise Suppose we extend the language λ→+ unit + references (Figure 13-1) with the followingnew syntax, typing rules, and evaluation rules:t ::= . . . terms:free t deallocationΓ | Σ ` t : Ref TT-FreeΓ | Σ ` free t : Unitl ∈ dom (µ)E-FreeReffree l | µ −→ unit | (µ \ {l})t | µ −→ t0| µ0E-Freefree t | µ −→ free t0| µ0where we use the notation µ \ {l} to indicate the store µ without any binding for the location l.Some questions about this language:1. Does progress (Theorem 13.5.7) hold for this language? If so, give the new case(s ) in theproofs. If not, give a counterexample.2. Does preservation (Theorem 13.5.3) hold for this language? If so, give the new case(s) in theproofs. If not, give a counterexample.3. Based on your answers to the previous two questions, can you give a program t in thislanguage with ∅ | ∅ ` t : T and t | ∅ −→∗t0| µ06−→ such that t0is not a value? If not, whynot? If so, give such a program.3 Exercise Exercise 13.3.1 from TAPL. (Again, this exercise has a solution in the back of the book.To get full value out of the assignment, don’t peek until after you have written out a completesolution of your own.)4 Debriefing1. Approximately how many hours (per person, on average) did you spend on this assignment?2. Would you rate it as e asy, moderate, or difficult?3. How deeply do you feel you understand the material it covers (0%–100%)?4. Any other comm
View Full Document
Unlocking...