Types for Programs and Proofs

Types for Programs and Proofs

DAT140/DIT232, study period 1, 2016

News

The take home exam will be available at 800 on Tuesday 18 October. Here is last year's exam.

Here are some more exercises in propositional logic.

Since ML1 is too small for the course, we have been assigned new lecture rooms. Unfortunately, this means that we will have different rooms on different occasions. Please consult TimeEdit.

Aim

The development of powerful type systems is an important aspect of modern programming language design. This course provides an introduction to this area. In particular it introduces the notion of dependent type, a type which can depend on (is indexed by) values of another type, for example, the type of vectors indexed by its length. Dependent types are versatile. Through the Curry-Howard identification of proposition and types virtually any property of a program can be expressed using dependent types. The student will learn how to use an interactive programming system for a language with dependent types. The course is thus simultaneously an introduction to
  • functional programming with dependent types;
  • computer-assisted interactive proving in logical systems, including predicate logic;
  • proving the correctness of functional programs;
  • type systems and operational semantics for programming languages.
Each of these topics is supported by experimenting with the interactive proof system.

Teachers

Literature

Books: Agda: PCF: There is also a Google group.

Prerequisites

Lectures

We will be in different rooms on different occasions. Please consult TimeEdit.

Exercise sessions

This will include Agda supervision and discussion of homework (AV). These exercise sessions are for everyone, but in order to get credit for homework you must be prepared to present your solutions in class.

Plan for lectures and homework

DTW means suggested reading in Dependent Types at Work. TPL means suggested reading in Types and Programming Languages.
Th 1 Sep (PD) Introduction. Simply typed programming in Agda. Code: Booleans, Natural numbers. Reading: DTW 1, 2.1 - 2.5.
Mo 5 Sep (PD) Termination checking. Dependent types. Polymorphism. Propositions as sets. Code: Division, Logical Framework, Lists, Pairs, Vectors, Propositional logic. Identity set, Proofs about booleans. DTW 2.6 - 2.7, 3, 4.1, 4.3, 5.1, 5.2.
Th 8 Sep (PD) Predicate logic. Proving in Agda. Code: Predicate logic, Proofs about natural numbers. DTW 4.2, 4.4.
Mo 12 Sep (PD) Inductive Predicates. Records. Abstract data types. Code: Even numbers, A record for dates, Products as records, The Sigma-type as a dependent record, Counters as records. Homework 1 due.
Th 15 Sep (TC) Introduction to operational semantics and type systems.
Mo 19 Sep (TC) Introduction to operational semantics and type systems. Homework 2 due.
Th 22 Sep (PD) Boolean expressions and arithmetic expressions in Agda. Code: Boolean expressions, Operational semantics of Boolean expressions, Reflexive, transitive closure of a relation, Arithmetic expressions and their types, Operational semantics of artihmetic expressions and the proof of the type preservation theorem.
Mo 26 Sep (TC) Introduction to operational semantics and type systems. Homework 3 due.
Th 29 Sep (TC) Introduction to operational semantics and type systems.
Mo 3 Oct (TC) Introduction to operational semantics and type systems.
Th 6 Oct (UN) Guest lecture on Agda. Code: Typed lambda calculus.
Mo 10 Oct Student presentations. Homework 4 due.
Th 13 Oct Student presentations.
Mo 17 Oct Student presentations.

Examination

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.

Links

Course evaluators