Dependently Typed Programming (G54DTP)

Dependently Typed Programming teaches you advanced topics in functional programming. We will start with an introduction to pure lambda-calculus and simply typed lambda-calculus. Then we will go on to study type systems with dependent types and prove their mathematical properties. We will look at the correspondence between functional programming and formal logic. Finally we will learn about inductive and coinductive definitions. The module consists of two threads, a theoretical study of type systems and a practical activity in using the proof assistant Coq.

Module Resources

The theoretical part of the module is based on Lambda Calculi with Types by H.P. Barendregt, in the Handbook of Logic in Computer Science, Volume 2, Chapter 2. A more recent account of the same material is in the book Lecture Notes on the Curry-Howard Isomorphism by M.H. Sørensen and P. Urzyczyn.

For the practical part, we use the proof assistant Coq. We will learn it by following the on-line book Certified Programming with Dependent Types by Adam Chlipala. Another good introduction book to Coq is Interactive Theorem Proving and Program Development by Yves Bertot and Pierre Castéran. The code files for this book are availabe from the Coq'Art page.

Outline of lectures

In this section you will find, after each lecture, a list of topics that were taught.

Lecture	Topics	Coq Files
1. 24 Jan 2011	Introduction to the Module
2. 31 Jan 2011	Introduction Coq Chapter 1 of Bertot/Casteran	Insertion Sort from Bertot/Casteran
3. 4 Feb 2011	Simple recursion on inductive types Chapter 2 of Chlipala Chapter 6 of Bertot/Casteran	Simple recursive functions
4. 7 Feb 2011	Inductive types and recursive functions	Search trees
5. 11 Feb 2011	Propositional Logic The Curry-Howard Isomorphism Chapter 3 of Bertot/Casteran
6. 14 Feb 2011	Propositional connectives Chapter 5 (Sec. 5.2) of Bertot/Casteran	Example proofs
7. 18 Feb 2011	Type Universes Family of Finite Types
8. 25 Feb 2011	Dependent Types, Vectors Bertot/Casteran, Ch.4, Ch.6 Sec.6.5	Vector Types
9. 28 Feb 2011	Pattern Matching on Dependent Types
10. 7 March 2011	Inductive Predicates Bertot/Casteran, Ch.8	Even and Odd
11. 11 March 2011	Divisibility relation	Quotient and Remainder
12. 14 March 2011	General Recursion read Bertot/Casteran, Ch.5	Inductive Domain Predicate
13. 17 March 2011	Lab Session on Assignment 3
14. 21 March 2011	Minimization function Introduction to coinductive types
15. 25 March 2011	Lazy Lists read Bertot/Casteran, Ch.13	Lazy Lists
16. 28 March 2011	(Co)Inductive predicates on streams	Streams
17. 1 April 2011	Minimization for Streams	Minimization

Assessment

The final mark you get on this module is equally divided between coursework and final exam. The coursework will consist of four assignments that I will give you during the module: they are exercises in programming and proving using Coq. You must complete them and e-mail them to me by the specified date. The final exam consists in some problems on the theoretical part of the module.

Date	Assignment	Submit by	Solution
7 Feb 2011	Assignment 1: Recursive Functions	18 Feb 2011	Solutions
18 Feb 2011	Assignment 2: Propositional Logic	4 March 2011	Solutions
7 March 2011	Assignment 3: Dependent Types	21 March 2011	Solutions
25 March 2011	Assignment 4: Coinductive Types	8 April 2011	Solutions

Contacting the teacher

Please don't hesitate to ask me any question you may have about the module. After every lecture, I'm in my office (A07 in the Computer Science building) answering all your queries. You can also contact me by e-mail: put G54DPT in the subject line, so I know immediately that it is about this module.