CS430/530 Assignment 3
Last modified: February 5, 2025.
Due: Thursday, 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.
Sample Solutions
For the writing part, sample solutions can be downloaded
here. For the coq part, sample solutions
can be downloaded here and here.
Solutions to the writing part were provided by Antonis Stampoulis.
Solutions to the coq part were prepared by Longfei Qiu.