|
Jan 8
|
course overview; basic Rocq programming
|
Notes
SF: Basics
|
|
|
Jan 15
|
equality; inductive relations; interpreters and compilers
|
Notes
SF: Induction
CPDT: Stack Machine
|
|
|
Jan 22
|
Instructor away
|
|
|
Jan 29
|
operational semantics
|
Notes
|
|
|
Feb 5
|
algorithmic correctness; well-founded recursion
|
Notes
SF: Sort
SF: Merge
CPDT: General Recursion
|
|
|
Feb 12
|
well-founded induction; STLC; type safety
|
Notes
FRAP: §11
|
project proposal
due Feb 16
|
|
Feb 19
|
Reading Week
|
|
|
Feb 26
|
exceptions; mutable references
|
Notes
|
|
|
Mar 5
|
Hoare logic; shallow encoding
|
Notes
|
|
|
Mar 12
|
separation logic
|
Notes
|
|
|
Mar 19
|
proof search and proof by reflection
|
Notes
|
Presentation slides
due Mar 26 (noon)
|
|
Mar 26
|
project presentations
|
|
|
|
Apr 2
|
coinductive types; coinduction
|
Notes
|
|
|
|
|
|
final project
due Apr 19
|