|
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
|
data abstraction; well-founded recursion
|
|
|
|
Feb 5
|
operational semantics
|
|
Assignment 2
due Feb 9
|
|
Feb 12
|
STLC; type safety
|
|
project proposal
due Feb 16
|
|
Feb 19
|
Reading Week
|
|
|
Feb 26
|
exceptions; mutable references
|
|
Assignment 3
due Mar 2
|
|
Mar 5
|
termination; simulation
|
|
|
|
Mar 12
|
Hoare logic; shallow encoding
|
|
Assignment 4
due Mar 16
|
|
Mar 19
|
separation logic
|
|
Presentation slides
due Mar 26 (noon)
|
|
Mar 26
|
project presentations
|
|
Assignment 5
due Mar 30
|
|
Apr 2
|
advanced topics
|
|
|
|
|
|
|
final project
due Apr 18
|