Types for Programs and Proofs (preliminary page)

Types for Programs and Proofs

DAT140/DIT232, study period 1, 2012

"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 and reported.

Aim

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.

Literature

Types and Programming Languages by Benjamin Pierce, MIT Press.

Course notes on dependent types:

Dependent Types at Work by Ana Bove and Peter Dybjer
Dependently Typed Programming in Agda by Ulf Norell
Agda wiki
Benjamin Pierce's course

Course notes on PCF:

Computability via PCF by Peter Dybjer.

Prerequisites

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

Lectures

Mondays 13.15 - 15.00 in ML16
Thursdays 10.00 - 11.45 in ML4

Agda supervision (GM)

Thursday 6 Sep 14-16 in 6128
Every Friday 7 Sep - 28 Sep, 10-12 in 5128
Monday 10 Sep, 15-16 in 6128
Every Tuesday 11 Sep - 18 Sep, 14 - 16 in 5128 and on 25 Sep - 2 Oct 13 - 15 in 6128. Note the change!

There is also a mailing list for the course.

Plan

Date	Chapters	Topics	Homework
Th 6 Sep	1-2	Introduction. Dependently typed programming. (PD) Code: TruthValues, NaturalNumbers, LambdaNotation, Lists	Homework due 20 Sep 13.15
Mo 10 Sep	3-4	Untyped Arithmetic expressions. Dependently typed programming. (PD) Code: Product, Vectors, PropositionalLogic.
Th 13 Sep		Agda programming session. (GM) Code: PredicateLogic, Equality
Mo 17 Sep		Dependently typed programming. (NAD) Code: Boolean-Expressions, Unit	Homework due 27 Sep 13.15
Th 20 Sep	5-10	Untyped lambda calculus. Simple types. Type soundness. (PD)
Mo 24 Sep		Dependently typed programming. (NAD) Code: Prelude, untyped lambda calculus, typed lambda calculus, well-typed terms, parametric higher order abstract syntax.	Homework due 4 Oct 13.15
Th 27 Sep	8-10	Simple types. Type soundness. (PD)
Mo 1 Oct	11-12	Records, variants, datatypes. Normalization. (PD)	Homework due 11 Oct 13.15
Th 4 Oct	23-25	Polymorphism and system F. Abstract data types and existential types. (PD) Code: local definitions, products and records, sums and variants, an abstract data type using a record
Mo 8 Oct		Student presentations. Schedule on wiki
Th 11 Oct		Student presentations. Schedule on wiki
Mo 15 Oct		Student presentations. Schedule on wiki
Th 18 Oct		Student presentations. Schedule on wiki.

Examination

Homework. 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). The Fire system should be used for submitting your homework. Handwritten homework can also be handed in in class. Do not submit homework by email.
Presentation of advanced topic. You should work in pairs and choose a topic no later than on Thursday 20 September 13.15. After that your talk will be scheduled during the last two weeks of the course. Schedule and talk proposals. Bonus points will also be given for good presentations (max 5pts) and for attendance at the presentations (max 4 x 1 pts).
Take home exam Friday 26 October 1600 - Friday 2 November 1600.

Teachers

Peter Dybjer (PD), course responsible
Nils Anders Danielsson (NAD), guest lecturer
Guilhem Moulin (GM), course assistant

Course evaluation

Course representatives:

Viktor Holmqvist, vikhol@student.chalmers,
Jonatan Pålsson, jonpal@student.chalmers,
Thomas Bååth Sjöblom, thobaa@student.chalmers.

Registration

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