CS430/530 Assignment 3

Last modified: February 5, 2025.

Due: Tuesday, February 20, 2025

  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 Tactics (Please directly modify the abridged Tactics.v file; full version at Tactics.v):

Before working on Poly.v and Tactics.v in question 8 and 9, you have to place the Basics.vo file you used for assignment 2 in the same directory as the two files. You also have to compile your finished {Induction,Lists}.v files in assignment 2 and place the {Induction,Lists}.vo files in the same directory. You may have to add a line

at the end of Lists.v before compiling (my fault -- Longfei). Before working on Tactics.v you also have to execute Alternatively, you may download our sample solutions to {Basics,Induction,Lists}.v (available 3 days after AS2 is due) and compile them instead.