Due: By the beginning of lecture on Monday, March 9.
You are required to typeset your answers. Not only will this make your
answers easier to read, but it will make your work easier since you can
use an editor to cut/paste/modify
parts of different problems. We strongly recommend using LaTeX since it
is superior for layout of mathematical material. If you choose to use
some other word processing application, please be sure that it produces
equally high quality output.
Do Exercise 1 in Section 9.3 (p. 78) of Harper's book.
Do Exercise 1 in Section 10.4 (p. 87) of Harper's book.
Do Exercise 2 in Section 10.4 (p. 87) of Harper's book.
Consider the evaluation sequence near the middle of page 81 in Harper's book.
Use the static semantics from Chapter 9 in Harper's book to derive a type for the
initial expression (the first line of the sequence) and a type for the final expression
(the last line of the sequence). How do your results relate to type safety?
Consider the evaluation sequence near the middle of page 81 in Harper's book.
Give the corresponding evaluation sequence resulting from using the contextual semantics
variant of structural semantics to justify each transition step.
Give the corresponding evaluation sequence resulting from using evaluation semantics
to justify each transition step.
Give the corresponding evaluation sequence resulting from using environment semantics,
starting with an empty environment, to justify each transition step.
Give the parts of the proof of Theorem 10.2 (page 83 in Harper's book) related to
the let operation (let(e1;x.e2)).
Give the parts of the proof of Theorem 11.2 (page 90 in Harper's book) related to
the length of string operation (len(e)).
Give the parts of the proof of Theorem 11.4 (page 91 in Harper's book) related to
the let operation (let(e1;x.e2)).
Give the parts of the proofs of Lemmas 12.3 and 12.4 (page 97 in Harper's book) related to
the let operation (let(e1;x.e2)).
Give all the rules necessary to define the "goes wrong" judgement for the
the let operation (let(e1;x.e2)).
State and prove the canonical forms lemma for unit and product types
as they are defined in Chapter 16 in Harper's book.
Do Exercise 1 from Section 17.4 (p. 146) of Harper's book.
Consider the expression (18.1) on page 148 in Harper's book.
Use the static semantics from Chapters 16, 17 and 18 in Harper's book to derive a type for
this expression.
