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 
InductivelyDefined 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 Checkin 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 
SimplyTyped 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 