|
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; operational semantics
|
|
Assignment 1
due Jan 23
|
|
Jan 28
|
|
|
|
|
Feb 4
|
|
|
Assignment 2
due Feb 6
|
|
Feb 11
|
|
|
Project proposal
due Feb 13
|
|
Feb 18
|
Reading Week
|
|
|
Feb 25
|
|
|
Assignment 3
due Feb 27
|
|
Mar 4
|
|
|
|
|
Mar 11
|
|
|
|
|
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
|