Types for Programs and Proofs

Types for Programs and Proofs

DAT140/DIT232, study period 1, 2009

"Types are the leaven of programming; they make it digestible"
(R. Milner, winner of the Turing award 1991)

News

The take home exam has now been corrected.

Bonus points for homework and presentations. Please check! People who have not sent their slides to Peter should do so immmediately!

Aim

The development of ever more 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.

Literature

Types and Programming Languages by Benjamin Pierce, MIT Press.

Course notes on dependent types:

Course notes on PCF:

Prerequisites

Functional programming. Some knowledge of logic and programming languages.

Schedule

Lectures (and tutorials) are in ML 3 on The first lecture is on Wednesday 2 September.

Preliminary plan

Date Chapters Topics
We 2 Sep Part 1 Introduction. Untyped systems. Lecture. Homework due 21 Sep
Mo 7 Sep Dependently typed programming in Agda.
We 9 Sep Dependently typed programming in Agda.
Mo 14 Sep -
We 16 Sep Dependently typed programming in Agda. Homework due 5 Oct
Code: Adder.agda, Bool.agda, Arith.agda
Mo 21 Sep Part 1 Untyped systems. Tutorial. Homework due.
Lecture notes on the Church-Rosser theorem.
We 23 Sep 8,9,10 Simple types. Type soundness. Homework due 5 Oct
Mo 28 Sep 8,9,10 Simple types. Type soundness. Homework due 12 Oct
We 30 Sep 11,12 Records, variants, datatypes. Normalization.
Mo 5 Oct 23,24,25 Polymorphism and system F. Abstract data types and existential types. Homework due.
Student presentations.
We 7 Oct Type reconstruction, Chapter 22 (Dan Rosen)
Subtyping, Chapter 15 (Mike Blaguszewski and Karin Keijzer)
John Launchbury, A natural semantics for lazy evaluation (Simon Edwardsson and Daniel Gustafsson)
Mo 12 Oct Homework due.
Exceptions, Chapter 14 (Joakim Lind-Hasselskog and Tobias Vehkajarvi)
Kinds and higher order polymorphism, Chapter 29-30 (Daniel Gustafsson and Anders Mortberg)
John Reynolds, Towards a theory of type structure (Alexandre Agular and Bassel Mannaa).
We 14 Oct References, Chapter 13 (Bartolomeus Jankowski and Tobias Olausson)
Recursive types, Chapter 20 (Alexander Edsmyr and Linus Ek)
Rod Burstall, Proving properties of programs by structural induction (Stevan Andjelkovic and Ola Holmstrom)
Jean-Louis Krivine, Call-by-name lambda-calculus machine (Arnar Birgisson and Willard Rafnsson)
Gilles Kahn, Natural semantics (Tuve Nordius)
John Reynolds, Types, abstraction, and parametric polymorphism (Saleem Fayyaz)

Examination

Take home exam (60 pts, due Friday 30 October 16.00). Presentation of advanced topic (proposals).

Bonus points will be given to students who have handed in homework and been prepared to present it in class (max 4 x 4 pts). Bonus points will also be given for good presentations (max 5pts) and for attendance at the presentations (max 3 x 1 pts).

Interesting links

The history of operational semantics by G. Plotkin.

Papers on parametric polymorphism by J. Reynolds.

Lecturers

Thierry Coquand
Peter Dybjer
Ulf Norell