|
Monday
13:15-15:00
Lecture |
Monday
15:15-17:00
Exercise session |
Thursday
10:00-11:45
Lecture |
1. W 36
31/8 - 4/9 |
no lecture
|
no exercise session
|
Introduction.
Simply typed programming in Agda. (PD)
Code:
Booleans,
Natural numbers.
Reading: LN 1 - 3, VFP 1, 3. DTW 1, 2.1 - 2.5.
|
2. W 37
7 - 11/9 |
Termination checking. Dependent types. Polymorphism. Propositions as
sets.
(PD)
Code:
Division,
Logical Framework,
Lists,
Pairs,
Vectors,
Identity set,
Proofs about booleans.
LN 4 - 5, VFP 2, DTW 2.6 - 2.7, 3, 5.1, 5.2.
|
Getting started with Agda. This is not a lecture but a 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.
(UN)
|
Proving in Agda. Inductive predicates. Propositional and predicate logic (PD)
Code:
Propositional logic.
Predicate logic,
Proofs about natural
numbers.
Even numbers,
LN 6 - 9, DTW 4.
|
3. W 38
14 - 18/9 |
Introduction to operational semantics and type systems. Summary (TC)
TPL 1-3.
|
More on Agda. (UN)
Homework 1 due.
|
Introduction to operational semantics and type
systems. Summary (TC)
TPL 3-4.
|
4. W 39
21 - 25/9 |
Introduction to operational semantics and type systems. Summary (TC)
TPL 5-10.
|
More on Agda (UN).
Homework 2 due.
|
Introduction to operational semantics and type systems. Summary (TC)
|
5. W 40
28/9 - 2/10 |
Records. Abstract data types. (PD)
Code:
A record for dates,
Products as records,
The Sigma-type as a dependent
record,
A parametrised module,
Counters as records.
|
More on Agda (UN).
Homework 3 due.
|
Boolean expressions and
arithmetic expressions in Agda. (PD)
Code:
Reflexive, transitive
closure of a relation,
Boolean expressions and their denotational semantics,
operational semantics of Boolean expressions,
Arithmetic expressions and their types,
operational semantics of
artihmetic expressions and the proof of the type preservation
theorem.
The Maybe-type,
Additive expressions,
Proof of the correctness of a small
compiler a la McCarthy and Painter.
|
6. W 41
5 - 9/10 |
Introduction to operational semantics and type systems. Summary (TC)
|
Exercises on operational semantics and type systems. (TC)
Homework 4 due.
|
Typed lambda calculus in Agda.
Code:
Typed lambda calculus (PD)
|
7. W 42
12 - 16/10 |
Student presentations.
|
no exercise session
|
Student presentations
|
8. W 43
19 - 23/10 |
Student presentations
|
no exercise session
|
Take home exam:
Tuesday 20/10 8:00
- Friday 23/10 12:00
|