Types for Programs and Proofs

Types for Programs and Proofs

DAT140/DIT232, study period 1, 2013


The take home exam is now corrected. Unfortunately, we have not been able to do the official reporting of the course because of illness at the student administration office.


The development of powerful type systems is one of the most dynamic aspects of modern programming language design. The aim of this course is to provide a solid and broad foundation in type systems for programming languages. The student will be exposed to applications of type-based technology in computer science and learn to use an interactive programming and proof system using dependent types.


Types and Programming Languages by Benjamin Pierce, MIT Press.

Course notes on dependent types:

Course notes on PCF:


Functional programming (essential). Some knowledge of logic and programming languages.


Agda supervision (GM)

There is also a mailing list for the course.


Date Chapters Topics Homework
Th 5 Sep 1-2 Introduction. Dependently typed programming in Agda. (PD) Homework due 19 Sep 13.15
Mo 9 Sep Dependently typed programming in Agda. (PD) Code: Truth values, Natural numbers, Lambda notation, Lists, Pairs, Unit, Vectors.
Th 12 Sep The Curry-Howard isomorphism. (PD) Code: Propositional logic. Predicate logic, Equality
Mo 16 Sep 3-4 Proving in Agda. Boolean expressions and untyped lambda expressions in Agda (PD) Code: Proofs about booleans, Proofs about natural numbers, Boolean expressions, Untyped lambda expressions Homework due 26 Sep 13.15
Th 19 Sep 5-10 Dependently typed programming. (UN) Code: Proofs about Boolean expressions.
Mo 23 Sep 8-10 Untyped lambda calculus, Simple types. Type soundness. (TC)
Th 26 Sep 8-10 Simple types. Type soundness. (TC) Here is a description of simply typed lambda-calculus using de Bruijn notations and the notion of closures. Homework due 10 Oct 13.15
Mo 30 Sep 11-12 Polymorphism and system F. Abstract data types and existential types. Normalization. (TC)
Th 3 Oct 23-25 Introduction to univalent foundations. (TC)
Mo 7 Oct Student presentations. Schedule on wiki
Th 10 Oct Student presentations. Schedule on wiki
Mo 14 Oct Student presentations. Schedule on wiki
Th 17 Oct Student presentations. Schedule on wiki.


Note that both homework and take home exam should be done individually. If we find out that people have helped each other or copied solutions, we will fail the whole course both for the helper and the helped.



Course evaluators


For GU-students admitted to the course. This semester you have to register online in LPW at the Student portal. The registration is compulsory and you need to register the same day as the first lecture otherwise you will lose your place in the course. Further information about registration and how to activate your student account