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:1515:00 Lecture in FL71 
Monday
15:1517:00 Exercise session in FL71 
Thursday
10:0011: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 Sigmatype 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 13.

4. W 38 18/9  22/9 
Introduction to operational semantics and type
systems. (TC)
TPL 34.

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 510.

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

