CS430/530 Assignment 3

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):
   • split
   • map_rev
   • fold_length
   • fold_map
9. SF MoreCoq (Please directly modify the abridged MoreCoq.v file; full version at MoreCoq.v):
   • silly_ex
   • practice: just beq_nat_0_l
   • plus_n_n_injective
   • beq_nat_true
   • combine_split

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.