| September | ||||
| Monday | Tuesday | Wednesday | Thursday | Friday |
| 28 | 29 |
30
Coq Tutorial
|
01
HW1 Posted
|
02 |
| October | ||||
| Monday | Tuesday | Wednesday | Thursday | Friday |
|
05
Lists, Inductiion
|
06 |
07
Syntax, Relations, Tactics
|
08 |
09
HW1 Due
|
|
12
Expression Semantics, Relations vs. Functions
HW2 Posted
|
13 |
14
Logic vs. Biology
Statement Semantics, Big vs. Small Step
|
15 | 16 |
|
19
Analysis, Termination
|
20 |
21
Pseudo Denotational Semantics
|
22 |
23
HW2 Due
|
|
26
Lambda Calculus, Reduction Strategies
|
27 |
28
Church Encodings, Y
Proof of a Program: FIND
|
29 | 30 |
| November | ||||
| Monday | Tuesday | Wednesday | Thursday | Friday |
|
02
STLC
Midterm Posted
|
03 |
04
Progress and Preservation
|
05 | 06 |
|
09
Midterm Due
Extending STLC
|
10 |
11
Veteran's Day
|
12
HW3 Posted
|
13 |
|
16
Extending STLC
|
17 |
18
Extending STLC
Social Processes and Proofs of Theorems
|
19 | 20 |
|
23
Records and Subtyping
HW3 Due
|
24 |
25
Thanksgiving
|
26 | 27 |
|
30
Parametric Polymorphism
|
01 |
02
Parametric Polymorphism
|
03 |
04
Final Posted
|
| December | ||||
| Monday | Tuesday | Wednesday | Thursday | Friday |
|
07
16: Recursive Types
|
08 |
09
17: Curry-Howard
CompCert
|
10 | 11 |
| 14 |
15
Final Due
|
16 | 17 | 18 |