Types for Programs and Proofs

Types for Programs and Proofs

DAT140/DIT232, study period 1, 2011

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

News

The take home exam is now corrected. The results will soon be available.

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 ML16 on

Preliminary plan

Date Chapters Topics
We 31 Sep Part 1 Introduction. Arithmetic expressions. (TC) Homework due 19 Sep 13.15
Mo 5 Sep Part 1 Untyped systems. Arithmetic expressions. Types and computation rules. (TC)
We 7 Sep 8,9,10 Simple types. Type soundness. (TC) Homework due 26 Sep 13.15
Mo 12 Sep 8,9,10 Simple types. Type soundness. (TC)
We 14 Sep 11,12 Records, variants, datatypes. Normalization. (TC)
Mo 19 Sep Dependently typed programming in Agda. (UN) Code: html, agda
We 21 Sep Dependently typed programming in Agda. (UN) Code: html, agda Homework due 5 Okt 13.15
Deadline for scheduling student presentations.
Mo 26 Sep 23,24,25 Polymorphism and system F. Abstract data types and existential types. (PD)
We 28 Sep Dependently typed programming in Agda. (UN) Code: html, agda
Mo 3 Oct Student presentations.
References, chapter 13 (Christian Isaksson, Andreas Wagner)
Subtyping, chapter 15, (Jens Lidestršm, Bart van Delft)
John McCarthy, Recursive functions of symbolic expressions and their computation by machine (Jonatan Bengtsson, Albin LindbŠck)
We 5 Oct
Featherweight Java, Chapter 19 (Hannes Sšrensson, Vijayakumar Raju)
Rod Burstall, Proving properties of programs by structural induction (Daniel Andren, Christoffer Skeppstedt)
Tim Griffin, The Formulae-as-Types Notion of Control for Curry-Howard and classical logic (Johan Grafstršm, Rodolphe Lepigre)
Types, abstraction, and parametric polymorphism (se Fahlander, Joacim Kosonen)
Mo 10 Oct
Jean-Louis Krivine, Call-by-name lambda-calculus machine (Johan Elvek, David SpŒngberg)
John Launchbury, A Natural Semantics for Lazy Evaluation (Qiuchi Jian, Gabriel Rizopulos)
Phil Wadler and Robby Findler, Well-typed programs cannot be blamed, (Jonas Karlsson, Mattis Jeppsson)
We 12 Oct
Exceptions, chapter 14, (Erik Flood, Joel Svensson)
Recursive types, chapter 20 (Andreas Granstršm, Daniel Mauritzson)
Peter Landin, On the Mechanical evaluation of Expressions (Ingemar dal, Alexandiar Marschanka)
John Reynolds, Towards a Theory of Type Structure (Adam Bengtsson, Mikael Bung)

Examination

The take home exam is now available. The deadline is on Tuesday 1 November at 1600.

Presentation of advanced topic (proposals). This topic should be chosen and the talk should be scheduled no later than on Wednesday 21 September 13.15.

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 4 x 1 pts).

Interesting links

The history of operational semantics by G. Plotkin.

Papers on parametric polymorphism by J. Reynolds.

Lecturers

Thierry Coquand (TC)
Peter Dybjer (PD)
Ulf Norell (UN)