Schedule

Date	Topic	Code	Reading	Homework
01/24	Course overview
01/26	Coq Programming	lec01.v	SF Basics, Lists, Poly	HW0 out
01/31	Induction and equality	lec02.v	SF Induction
02/02	Tactics	lec03.v	SF Tactics	HW0 due; HW1 out
02/07	Paper discussion: "Social Processes" (Ariel and Joshua)		CACM 1979
02/09	Paper discussion: "CompCert" (Priya and Charles)		CACM 2009	HW1 due; HW2 out
02/14	Logic	lec04.v	SF Logic	Project Proposal due
02/16	Paper Discussion: "CakeML" (Benjamin and Priya)		PLDI 2019	HW2 due
02/21	Inductively-Defined Propositions	lec05.v	SF IndProp, Maps, Imp
02/23	Paper discussion: "Closure Conversion" (Zach and Andrey)		ICFP 2019	HW3 out
02/28	No Class (February Break)
03/02	Defining tactics	lec06.v		HW3 due; HW4 out;
03/07	General recursion, fuel, and type classes	lec07.v
03/09	Paper discussion: "Verdi" (Amanda)		PLDI 2015	HW4 due; HW 5 out
03/14	No Class (Snow Day)
03/16	Regular expressions	lec08.v		HW 5 due
3/21	Paper discussion: "RockSalt" (Charles and Amanda)		PLDI 2012
03/23	Coq in industry (guest lecture by Satnam Singh)
03/28	Hoare Logic as Monad	lec09.v
03/30	No Class (Foster away)			Project Check-in due
04/04	No Class (Spring Break)
04/06	No Class (Spring Break)
04/11	More dependent types (guest lecture by Ryan Doenges)	lec10.v
04/13	Paper discussion: "FSCQ" (Mia and Ariel)		SOSP 2015
04/18	Simply-Typed Lambda Calculus	lec11.v
04/20	Paper discussion: "Interaction Trees" (Calvin and Zach)		POPL 2020
04/25	No Class (Foster away)
04/27	Abstraction and Parametricity	lec12.v
05/02	Unification and Type Inference	lec13.v
05/04	Paper discussion: "Mechanizing WebAssembly" (Nate)		CPP 2018
05/09	Project presentations			Final Project due