## CS430/530 Assignment 3

Last modified: September 29, 2013.

Solution posted: October 11, 2013.
**Due: Monday, October 7, 2013**

- 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 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.