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.
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.
Lecture | Topics | Coq Files |
---|---|---|
Introduction to the Module | ||
Introduction Coq Chapter 1 of Bertot/Casteran |
Insertion Sort from Bertot/Casteran | |
Simple recursion on inductive types Chapter 2 of Chlipala Chapter 6 of Bertot/Casteran |
Simple recursive functions | |
Inductive types and recursive functions | Search trees | |
Propositional Logic The Curry-Howard Isomorphism Chapter 3 of Bertot/Casteran |
||
Propositional connectives Chapter 5 (Sec. 5.2) of Bertot/Casteran |
Example proofs | |
Type Universes Family of Finite Types |
||
Dependent Types, Vectors Bertot/Casteran, Ch.4, Ch.6 Sec.6.5 |
Vector Types | |
Pattern Matching on Dependent Types | ||
Inductive Predicates Bertot/Casteran, Ch.8 |
Even and Odd | |
Divisibility relation | Quotient and Remainder | |
General Recursion read Bertot/Casteran, Ch.5 |
Inductive Domain Predicate | |
Lab Session on Assignment 3 | ||
Minimization function Introduction to coinductive types |
||
Lazy Lists read Bertot/Casteran, Ch.13 |
Lazy Lists | |
(Co)Inductive predicates on streams | Streams | |
Minimization for Streams | Minimization |
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 |