Types for Programs and Proofs DAT350/DIT232, LP1, HT2017


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