1 For Prospective Students
In this course, we will will work through the online textbook Software Foundations by Benjamin Pierce and co-authors (available in full online, though there is a local version linked on the Handouts page that you should use during the course). The goal of this book, and our goal, is to study topics in functional programming, logic, semantics, and type theory using the proof assistant Coq. The Preface of the textbook gives an excellent overview of the topics covered and the reasons to study them; if you are reading this sentence, you should click through and read the preface. In addition to what is written there, I can add that working in Coq is an interesting change from conventional (even functional) programming, and will appeal to those who like solving puzzles. This is the third offering of this course; the earlier ones were in fall 2014 and fall 2016.
Lectures: The HTML version of the book is generated from a set of source files that are Coq scripts, which you will be using for assignments. Local "full" versions of these files are available on the Handouts page. Lectures will consist of my loading a terse version of one of these files into my browser to project as "slides". At the same time, I will load the corresponding full version into Emacs, and work through some of the proof scripts interactively, while providing relevant commentary and some whiteboard explanations. How far we will get depends on many factors, but we will follow the core chapter path (with a few omissions and additions). We should be able to complete Volume I and get about halfway through Volume II, roughly to the discussion of the properties of the simply-typed lambda calculus (StlcProp).
Workload: The files include exercises, some of which will be assigned (when we have gone through the material in lecture) for you to complete and submit to have grades recorded. These exercises nearly all consist of you interactively writing proof scripts for Coq. These scripts are for the most part short, but it may take you some time to get them right. The advantage of using Coq is that you will know immediately whether they are correct or not. I have personally completed all exercises I will ask you to do, and I will have some additional comments and hints to offer. A few exercises may involve short exposition or informal mathematical proofs which will require hand-marking by me. These assignments will be the only basis for your final grade. There are no exams, presentations, or projects.
Necessary background: I will expect only some familiarity with some form of programming (such as might be obtained from a first course), exposure to university-level mathematics (including the brief look at discrete mathematics and logic that is found in the typical undergraduate CS curriculum), and the ability to install and work with new software (on which the Logistics page has more details). Exposure to functional programming will help, but if you have none, just be prepared to think about programs differently.