CS430/530 Assignment 3

Last modified: September 29, 2013.
Solution posted: October 11, 2013.

Due: Monday, October 7, 2013

  1. Reynolds, Exercise 5.1(a, b).
  2. Reynolds, Exercise 5.3.
  3. Reynolds, Exercise 5.4(b).
  4. Show that either the direct or the continuation denotational semantics (of a language without fail) does not distinguish the following commands: if x=0 then ?y ; !y+1 else ?y ; !y+2 and ?y ; if x=0 then !y+1 else !y+2
  5. Reynolds, Exercise 6.1(a).
  6. Reynolds, Exercise 6.2.
  7. Reynolds, Exercise 6.4.
  8. SF Poly (Please directly modify the abridged Poly.v file; full version at Poly.v):

  9. SF MoreCoq (Please directly modify the abridged MoreCoq.v file; full version at MoreCoq.v):

Sample Solutions

For the writing part, sample solutions can be downloaded here. For the coq part, sample solutions are on the Zoo machine /c/cs430/as/as3/{Poly,MoreCoq}-sol.v.