Homework is generally due at 11pm PT on Sundays.

Due dateFiles
09-05Day01_intro.v and Day02_types.v due at 11pm PT
09-12Day03_recursion.v and Day04_structures.v due at 11pm PT
09-19Day05_lists.v and Day06_sorting.v due at 11pm PT
09-26Day07_trees.v and Day08_sets.v due at 11pm PT
10-03Day09_levenshtein.v and Day10_expressions.v due at 11pm PT. First exam due 10-08 at 11:59pm PT.
10-10Day11_propositions.v and Day12_cases.v due at 11pm PT
10-17Day13_induction.v and Day14_exists.v due at 11pm PT
10-24Day15_induction2.v due at 11pm PT
10-31Day16_indprop.v and Day17_indprop2.v due at 11pm PT
11-07Day18_sorting.v and Day19_levenshtein.v at 11pm PT
11-14Day20_latex.tex and Day21_translating.tex and second exam due at 11pm PT
11-21Day22_sorting.tex and Day23_combo.tex due at 11pm PT
12-05 (!)Day24_sets.tex due at 11pm PT. Any submissions before 11/29 will be graded before 12/02.
12-05Day25_relations.tex and Day26_countability.tex due at 11pm PT
12-12Day27_graphs.tex and third exam due at 11pm PT
12-14Final exam slot, retakes

Feel free to look at various chapters ahead of time, but know that we may change assignments up until a week before the due date!

Worksheets are not for credit; they are excellent practice, though, and they resemble the kinds of problems we like to set on exams.

Guides are meant to give you an overview of proof techniques or how to prepare for an upcoming test.

Office hours and mentor sessions

Office hours and mentor sessions are in the same Zoom room. The password is available on Slack.

All times are in Pacific Time. Look in #csci-054-po on Slack for Zoom info. Look for more times to be announced after Tuesday 09/07.

Summer 07:30pm--09:30pmProf Osborn 02:00pm--04:00pmProf Osborn 09:00--11:00Guy 09:00--11:00
LC 1 (Summer) 09:00--11:00LC 4 (Guy) 05:30pm--07:30pmChloe 11:00--1:00Lucas & David 06:00pm--08:00pm
LC 2 (Eryn) 11:00-01:00pmEryn 05:00pm--07:00pmLC 5 (Lucas) 03:00pm--05:00pm
LC 3 (Chloe) 01:00pm--02:00pmLC 6 (David) 03:00pm--05:00pm

Lecture Schedule

Please see the syllabus for general course information. The course has three parts: programming, formal proof, and paper proof.

0108-31Day01_introCoq, Emacs, how to read the book; boolean operations, truth tables, and DNA bases
0209-02Day02_typesnumbers and recursive functions
0309-07Day03_recursionmore recursive functions
0409-09Day04_structurespairs, options, lists, and trees
0509-14Day05_listslist processing
0609-16Day06_sortinginsertion sort
0709-21Day07_treesbinary search trees
0809-23Day08_setslist and tree representations of sets
0909-28Day09_levenshteinthe Levenshtein algorithm for edit distance
1009-30Day10_expressionsexpressions and interpreters

At this point, we'll have our first exam on gradescope, about programming.

1110-05Day11_propositionsbasic formal proof; Coq tactics; equality and logical propositions
1210-07Day12_casesproofs by case analysis
1410-14Day14_existsexistential quantification
1510-21Day15_induction2induction on other structures
1610-26Day16_indpropinductive propositions
1710-28Day17_indprop2inductive propositions, continued
1811-02Day18_sortingpermutations and sorting
1911-04Day19_levenshteinproving the Levenshtein algorithm correct and optimal

At this point, we'll have our second exam on gradescope, about formal proof.

2011-09Day20_latexmathematical typesetting in LaTeX
2111-11Day21_translatingtranslating formal proofs to paper
2211-16Day22_sortingsort, informally
2311-18Day23_combinatoricscounting; sum rule, product rule, division rule, permutation, choose
2411-23Day24_setsset theory
2511-30Day25_relationsrelations and functions
2612-02Day26_countabilitycardinality and (un)countability
2712-07Day27_graphsgraphs and paths and trees

The third exam (on informal proof) is due the Sunday after the last week of classes (12/12). Grades will be distributed by the morning of 12/14.

Retakes of exam sections will take place during our final exam slot (14:00--17:00 PT, Tuesday December 14th), in-person but laptops allowed.


We're using Coq 8.12.2, Emacs 27.2 (macOS, Windows, on Linux see your package manager), and Proof General.

To configure your emacs, you'll want to download our init.el and install it to the appropriate location:


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!