Schedule

Lecture: TuTh 2:55–4:10 in Phillips 101, starting January 21, 2020.

This schedule is subject to change, except for the dates of holidays and exams.

Recordings of lecture after Spring Break are available in Panopto.

Date	Chapter(s)	Assignment
	Intro slides Preface [reading \| slides \| lecture], Basics [reading \| slides \| lecture]
	(Basics continued) Induction [reading \| slides \| lecture]	A1

	Lists [reading \| slides \| lecture]
	(Lists continued, start Poly)	A2

	Poly [reading \| slides \| lecture], Tactics [reading \| slides \| lecture]
	(Tactics continued)	A3

	Five Stages of Accepting Constructive Mathematics Logic [reading \| slides \| lecture]
	(Logic continued)	A4

	IndProp [reading \| slides \| lecture]
	(IndProp continued)	A5

	February Break
	ProofObjects [reading \| slides \| lecture]

	Prelim: March 2-5: take-home exam
	Class canceled for prelim
	IndPrinciples [reading \| slides \| lecture]	A6

	Maps [reading \| slides \| lecture], Imp [reading \| slides \| lecture]
	(Maps and Imp continued)	A7

	Classes suspended in response to Covid-19
	Classes resume virtually

	Auto [reading \| slides \| lecture]
	Hoare [reading \| slides \| lecture]	A8

	Hoare2 [reading \| slides \| lecture]
	(Hoare2 continued) HoareAsLogic [reading \| slides \| lecture]	A9

	Perm [reading \| slides \| lecture], Sort [reading \| slides \| lecture], Multiset [reading \| slides \| lecture]
	Selection [reading \| slides \| lecture]	A10

	Formal Verification of a Realistic Compiler
	SearchTree [reading \| slides \| lecture]	A11

	ADT [reading \| slides \| lecture]
	(ADT continued) Extract [reading \| slides \| lecture]

	Conclusion: slides Reading: [De Millo et al. 1979], [Asperti et al. 2009] Redblack [reading \| slides \| lecture]

	Final: Final exam due 4:30 pm