Week |
Date |
Topics |
Material |
Deadlines |
1(17) |
26/4 |
Introduction |
slides and code |
|
|
28/4 |
Agda - introduction (WS) |
slides and code |
|
2(18) |
3/5 |
Agda - pattern matching dependent types (WS) |
code |
|
|
5/5 |
Classes cancelled |
|
|
3(19) |
10/5 |
Agda - universes & lambda calculus (WS) |
code |
|
|
12/5 |
Semantics I - denotational, small step and big step (WS) |
slides and code |
Hand in first exercise set |
4(20) |
17/5 |
Semantics II - types (WS) |
code |
|
|
19/5 |
Semantics III - logical relations |
|
|
5(21) |
24/5 |
Intro and Control Flow Analysis (part 1) |
slides |
|
|
26/5 |
Control Flow Analysis (part 2) |
|
Hand in second exercise set before 28/5 |
6(23) |
31/5 |
Tracking Effects in Type Systems/Usage Analysis (pt 1) |
slides1
slides2 |
|
|
2/6 |
Usage Analysis (part 2)/Abstract Interpretation (part 1) |
slides |
|
7(24) |
7/6 |
Abstract Interpretation (part 2) |
|
|
|
9/6 |
No class |
|
|
8(25) |
14/6 |
9.00: Robin & Frank; 10.00: Ferdinand & Matthew |
|
|
|
16/6 |
|
|
Hand in Assignment 3 before or on 18/6 |
9(25) |
21/6 |
9.00: Fabian & Carlos; 10.00: Ruud |
|
|
|
23/6 |
13.15: Giovanni & Sije; 14.15: Marinus |
|
|