|
The first lecture is on Thursday, 31/8, at 10:00 in room MC.
Teachers:
TC = Thierry
Coquand,
PD = Peter
Dybjer,
UN = Ulf
Norell,
FR = Fabian Ruch,
AV = Andrea Vezzosi.
Reading: DTW = Dependent
Types at Work. VFP = Verified
Functional Programming in Agda. TPL =
Types and Programming Languages.
|
Monday
13:15-15:00
Lecture in FL71 |
Monday
15:15-17:00
Exercise session in FL71 |
Thursday
10:00-11:45
Lecture in MC |
1. W 35
28/8 - 1/9 |
no lecture
|
no exercise session
|
Introduction.
Simply typed programming in Agda. (PD)
Code:
Booleans,
Natural numbers.
Reading: VFP 1, 3. DTW 1, 2.1 - 2.5.
|
2. W 36
4/9 - 8/9 |
Termination checking. Dependent types. Polymorphism. Propositions as
sets.
(PD)
Code:
Division,
Logical Framework,
Lists,
Pairs,
Vectors,
Identity set,
Proofs about booleans.
VFP 2, DTW 2.6 - 2.7, 3, 5.1, 5.2.
|
Getting started with Agda.
(FR)
List of Exercises 1: agda file, pdf.
|
Proving in Agda. Inductive Predicates. Propositional and predicate logic (PD)
Code:
Propositional logic.
Predicate logic,
Proofs about natural
numbers.
Even numbers,
DTW 4.
|
3. W 37
11/9 - 15/9 |
Records. Abstract data types. (PD)
Code:
A record for dates,
Products as records,
The Sigma-type as a dependent record,
Counters as records.
|
More on Agda. (FR)
List of Exercises 2: agda file, pdf.
|
Introduction to operational semantics and type systems. (TC)
TPL 1-3.
|
4. W 38
18/9 - 22/9 |
Introduction to operational semantics and type
systems. (TC)
TPL 3-4.
|
More on Agda.
Homework 1 due. (AV)
|
Introduction to operational semantics and type systems. (TC)
|
5. W 39
25/9 - 29/9 |
Boolean expressions and
arithmetic expressions in Agda. (PD)
Code:
Boolean expressions,
Operational semantics of
Boolean expressions,
Reflexive, transitive
closure of a relation,
Arithmetic expressions and their types,
Operational semantics of
artihmetic expressions and the proof of the type preservation
theorem.
Proof of the correctness of a small
compiler a la McCarthy and Painter.
TPL 5-10.
|
More on Agda.
Homework 2 due. (AV)
|
Introduction to operational semantics and type systems. (TC)
|
6. W 40
2/10 - 6/10 |
Introduction to operational semantics and type systems. (TC)
|
Exercises on operational semantics and type systems. (AV)
|
Guest lecture on Agda.
Code:
Typed lambda calculus (UN)
|
7. W 41
9/10 - 13/10 |
Student presentations.
|
no exercise session
|
Student presentations
|
8. W 42
16/10 - 20/10 |
Student presentations
|
no exercise session
|
Take home exam:
Tuesday 17/10 8:00
- Friday 20/10 12:00
|
|