CS430/530 Assignment 2

Last modified: September 17, 2013.
Solution posted: September 29, 2013.

Due: Wednesday, September 25, 2013

  1. Reynolds, Exercise 2.2.
  2. Reynolds, Exercise 2.3.
  3. Reynolds, Exercise 2.4.
  4. Reynolds, Exercise 2.9.
  5. SF Induction (Please directly modify the abridged Induction.v file; full version at Induction.v):

  6. SF Lists (Please directly modify the abridged Lists.v file; full version at Lists.v):

For any tool to accept Induction.v and Lists.v in question 5 and 6, you have to compile the Basics.v you finished in assignment 1 to Basics.vo using

Or download the file here or copy /c/cs430/as/as2/Basics.vo (both available three days after assignment 1 due).

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/as2/{Induction,Lists}-sol.v.