|
Jan 7
|
course overview; Lean basics
|
Basic.lean
A0.lean
|
|
|
Jan 14
|
Curry–Howard correspondence; equality; induction
|
CurryHoward.lean
Induction.lean
Equality.lean
|
|
|
Jan 21
|
a verified compiler; denotational semantics
|
MiniCompiler.pdf
MiniCompiler.lean
|
Assignment 1
due Jan 23
|
|
Jan 28
|
operational semantics
|
IMP.pdf
IMP.lean
|
|
|
Feb 4
|
monads and effects
|
Monad.lean
ProbSTLC.pdf
ProbSTLC.lean
|
|
|
Feb 11
|
metaprogramming in Lean
|
Metaprogramming.lean
|
Assignment 2
due Feb 13
Project proposal
due Feb 13
|
|
Feb 18
|
Reading Week
|
|
|
Feb 25
|
well-founded recursion
|
WFRecursion.lean
|
|
|
Mar 4
|
certified and certifying decision procedures
|
DecProcedures.lean
|
|
|
Mar 11
|
|
|
Assignment 3
due Mar 13
|
|
Mar 18
|
Instructor away
|
|
|
Mar 25
|
project presentations
|
|
Presentation slides
due Mar 26 (noon)
|
|
Apr 1
|
project presentations
|
|
Presentation slides
due Apr 1 (noon)
|
|
|
|
|
Final project code and report
due Apr 23
|