From the course catalog:

A combined course on functional programming and formal proof. Students write programs over a variety of data structures, proving their programs correct with respect to precise logical specifications. Programming topics (and proof topics) range over: recursion (induction); combinatorics; algebraic data types, from lists to trees to abstract syntax trees (structural induction); parsers and interpreters (soundness properties); regular expressions (set theory and language theory).

Prerequisites: CSCI051 PO or equivalent (e.g., 4 or 5 on AP CS exam). Please see the syllabus for more information.


We’ll be using an experimental new volume of Software Foundations, which we're calling for now Discrete Math in Coq. Name suggestions are welcome!

Office hours and mentor sessions

Day Time Location
Prof. Michael Greenberg Tuesday 4–5pm (right after class) Seaver 104 (our classroom)
Prof. Michael Greenberg Wednesday 2–5pm Edmunds 225
Prof. Joseph C. Osborn Monday 1-3pm Edmunds 113
Prof. Joseph C. Osborn Thursday 10-12am Edmunds 113
Mentor sessions Friday (Iren) 6-8pm Edmunds 1st Floor Common Area
Mentor sessions Saturday (Mui) 1-3pm Edmunds 1st Floor Common Area
Mentor sessions Sunday (Ethan) 6-8pm Edmunds 1st Floor Common Area


Date Lecture Notes
1 Jan. 21 Basics (Formal) (.v file) (Informal)
2 Jan. 23 Basics Truth tables practice sheet
3 Jan. 28 Basics Basics (Formal) and (Informal) due Thursday at 1 PM
4 Jan. 30 Induction (Formal) (HTML) (.v file) (Informal) You can create a _CoqProject file with no file extension (in emacs might be easiest) with the contents -Q . DMFP, then automatic compilation should work next time you open Induction.v. If it doesn't, go ahead and open up Induction.v in Emacs. Now type M-! coqc -Q . DMFP Basics.v RET, i.e. use the M-! keyboard shortcut, then type coqc -Q . DMFP Basics.v and hit return.
5 Feb. 4 Induction
6 Feb. 6 Induction
7 Feb. 11 Induction
8 Feb. 13 Lists (Formal) (HTML) (.v file) (Informal .tex file) Induction (Formal) and (Informal) due at 1 PM.
9 Feb. 18 Lists
10 Feb. 20 Poly (Formal) (HTML) (.v file) (Informal .tex file)
11 Feb. 25 Poly Lists (Formal) and (Informal) due at 1 PM.
12 Feb. 27 Poly
13 Mar. 3 Tactics
14 Mar. 5 Tactics Poly (Formal) and (Informal) due at 1 PM.
15 Mar. 10 Review
16 Mar. 12 Midterm
Mar. 17 Spring break
Mar. 19 Spring break
17 Mar. 24 Logic how to prove it sheet
18 Mar. 26 Logic Tactics (Formal) and (Informal) due at 1 PM.
19 Mar. 31 Logic
20 Apr. 2 IndProp
21 Apr. 7 IndProp
22 Apr. 9 IndProp2 Logic (Formal) and (Informal) due at 1 PM.
23 Apr. 14 IndProp2
24 Apr. 16 Sort IndProp (Formal) and (Informal) due at 1 PM.
25 Apr. 21 Combinatorics
26 Apr. 23 Combinatorics IndProp2 (Formal) and (Informal) due at 1 PM.
27 Apr. 28 Countability
28 Apr. 30 Graphs Sort (Formal) and (Informal) due at 1 PM, Combo (Informal) due at 1 PM.
29 May 5 Trees Final Informal due at 1 PM Thursday 5/7.
Final May 11, 7–10pm Final Exam If you need an alternative to this time (e.g. for religious observation), talk to a professor promptly.