4 Logistics

The textbook for CS 798 is "Software Foundations" by Benjamin Pierce and co-authors (available online). Local versions of the HTML files, as well as the Coq files from which they are derived (which you will need to do the assignments) will be made available on the Handouts page (terse versions of the Coq files used by the instructor in lecture will not be made available).

There will be frequent programming assignments, not on a regular schedule, but timed by when we have covered the relevant material in lecture. Assignment details will be posted on the Assignments page. We will use the Marmoset submission system, but the only "testing" it will do is to ensure that your files compile, so if you have used it in another course, this will be a much simpler process. Submission details are on the Marmoset page.

The software used in the course is Coq 8.8.1. You will need to download and install the right version of Coq on a machine of your choice (the Coq compiler is available on the CS General and CS Undergraduate Environments, but not the IDEs described next).

You can either use the CoqIDE application (available from the Coq page above) to work in Coq, or (as will be done in lecture) Proof General for Emacs. There is some overhead in installing Emacs and learning to use it, but you can use it for many other purposes. Power users may wish to investigate the Company-Coq extensions to Proof General.

Other resources that are not directly required for the course but may be of assistance are detailed on the Resources page.