Num |
Day |
Date |
Topics Covered |
Materials |
0 |
Th |
21 Jan |
Proof Assistants |
TA notes
|
|
1 |
Tu |
26 Jan |
Propositions as types |
TA notes,
code
|
2 |
Th |
28 Jan |
Propositions as types |
TA notes
|
|
3 |
Tu |
2 Feb |
Agda basics |
Agda code ,
TA notes
|
4 |
Th |
4 Feb |
Induction; Agda installation |
handout,
solution
|
|
5 |
Tu |
9 Feb |
Agda Basics lab |
|
6 |
Th |
11 Feb |
Lists |
handout,
solution
|
|
7 |
Tu |
16 Feb |
With |
handout,
solution
|
8 |
Th |
18 Feb |
Equality Type |
code
|
|
9 |
Tu |
23 Feb |
Magic With; Inductive Families; Implicit Arguments |
handout,
solution
|
10 |
Th |
25 Feb |
Inductive Families Lab |
handout,
solution
|
|
11 |
Tu |
1 Mar |
Red-black Trees |
reading,
code
|
12 |
Th |
3 Mar |
Red-black Trees |
|
|
13 |
Tu |
22 Mar |
Regexp |
reading,
see HW6 for code
|
14 |
Th |
24 Mar |
Regexp |
|
|
15 |
Tu |
29 Mar |
Regexp |
|
16 |
Th |
31 Mar |
Regexp lab |
|
|
17 |
Tu |
5 Apr |
Universes |
code,
library code
|
18 |
Th |
7 Apr |
Printf |
code
|
|
19 |
Tu |
12 Apr |
Explicit Termination Metrics |
code
|
20 |
Th |
14 Apr |
Serialization |
see HW7
|
|
21 |
Tu |
19 Apr |
Circuits |
See HW8
|
22 |
Th |
21 Apr |
HW7 Review |
|
|
23 |
Tu |
26 Apr |
Imperative Programming |
See HW8 |
24 |
Th |
28 Apr |
Compiling to Circuits |
See HW8 |
|
25 |
Tu |
3 May |
Homotopy type theory |
|