|
Monday
13:15-15:00
Lecture |
Monday
15:15-17:00
Exercise session |
Thursday
10:00-11:45
Lecture |
1. W 36
28/8 - 1/9 |
no lecture
|
no exercise session
|
Introduction to Agda.
Simply typed programming in Agda. (UN)
Reading: LN 1 - 3, VFP 1, 3. DTW 1, 2.1 - 2.5.
|
2. W 37
4 - 8/9 |
Termination checking. Dependent types. Polymorphism. Propositions as
sets.
(TC)
|
Getting started with Agda. Help-session
where Ulf will help you get started with Agda programming. Before
this session you need to install Agda and try to write your first
Agda programs. Some simple exercises in Agda.
(UN)
|
Proving in Agda. Inductive predicates. Propositional and predicate logic (TC)
|
3. W 38
11 - 15/9 |
Introduction to operational semantics and type systems.
(TC)
TPL 1-3.
|
More on Agda. (TC)
Homework 1 due.
|
Introduction to operational semantics and type
systems. (TC)
TPL 3-4.
|
4. W 39
18 - 22/9 |
Introduction to operational semantics and type systems.
(TC)
TPL 5-10.
|
More on Agda (TC).
Homework 2 due.
|
Introduction to operational semantics and type systems.
(TC)
|
5. W 40
25/9 - 29/9 |
More on operational semantics and type systems in Agda.
(UN)
|
More on Agda (UN).
Homework 3 due.
|
Boolean expressions and
arithmetic expressions in Agda. (UN)
|
6. W 41
2 - 6/10 |
Records. Abstract data types. (UN)
|
Exercises on operational semantics and type systems. (UN)
Homework 4 due.
|
Typed lambda calculus in Agda.
(UN)
|
7. W 42
9 - 13/10 |
Student presentations.
|
no exercise session
|
Student presentations
|
8. W 43
16 - 20/10 |
Student presentations
|
no exercise session
|
Take home exam:
Tuesday 17/10 8:00
- Friday 20/10 12:00
|