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