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