CS430/530 Assignment 3
Last modified: February 5, 2025.
Due: Tuesday, February 20, 2025
- Reynolds, Exercise 5.1(a, b).
- Reynolds, Exercise 5.3.
- Reynolds, Exercise 5.4(b).
- 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
- Reynolds, Exercise 6.1(a).
- Reynolds, Exercise 6.2.
- Reynolds, Exercise 6.4.
- SF Poly
(Please directly modify the abridged Poly.v file;
full version at Poly.v):
- split
- map_rev
- fold_length
- fold_map
- SF Tactics
(Please directly modify the abridged Tactics.v file;
full version at Tactics.v):
- silly_ex
- injection_ex3
- eqb_true
- plus_n_n_injective
- combine_split
- split_combine
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.