Types for Programs and Proofs

DAT140/DIT232, study period 1, 2013

News

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.

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 ML1.
Thursdays 10.00 - 11.45 in ML1.

Agda supervision (GM)

Thursday 5 Sep 13-15 in 5128
Friday 6,13,20 Sep and 4,11 Oct, 10-12 in 5128
Tuesday 17 Sep and 1,8,15 Oct, 13-15 in 6128

There is also a mailing list for the course.

Plan

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.

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 19 September 13.15. Here are some talk proposals. Register your topic on this wiki. Write your names after the chapter or paper. Note that it is "first come first serve". You may not choose a topic which is already taken.
Bonus points will also be given for good presentations (max 5 pts) and for attendance at the presentations (max 4 x 1 pts).
Take home exam: Friday 25 October 1200 - Friday 1 November 1200.
Both presentation and take home exam are obligatory. Homework is not.

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.

Teachers

Thierry Coquand, (TC), course responsible
Peter Dybjer (PD), course responsible
Ulf Norell (UN), guest lecturer
Guilhem Moulin (GM), course assistant

Course evaluators

Jesper Lloyd: lioyd@student.chalmers.se
Alesandro Sanchez: alesan@student.chalmers.se
Niklas Ulvinge: ulvinge@student.chalmers.se
Jakob Rippe: rippe@student.chalmers.se

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