Please read Chapter 8 in your textbook.
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.)
Please do the following problems from the book:
8.3.5, 8.3.6 (p98)Do not turn in answers; check against back of book.
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. Put proofs in homework5.slf.
Find three papers in the literature that prove progress and preservation (or ``subject reduction''). What sort of errors are excluded by each system? Give the URL and the list of errors that are avoided.