Homework # 5
due October 7

Reading

Please read Chapter 8, and the first two sections of Chapter 9 in your textbook.

Discussion

The rule E-PREDSUCC has a condition above the line. What happens if we remove this condition? Can we still prove progress and preservation? Explain!

The rule T-PRED has a condition above the line. What happens if we remove this condition? Can we still prove progress and preservation? Explain!

(You might find it helpful to try out what happens using the SASyLF proofs of program and preservation.)

Problems

Please do the following problems from the book:

8.3.5, 8.3.6 (p98), 9.2.2 (p103)
Only turn in your answer to 9.2.2. For the others, check your answers against the back of the book.

Proofs

Do the following exercises in SASyLF: 8.2.3 (you will need to define what it means to be a subterm) and 8.3.4.

About this document



John Tang Boyland 2008-09-30