Functional Programming and Proofs

For this course I was assisted by Grégory Lafitte the first year, and then by Jean Duprat for three years. Some of the first year courses were recorded by Marc Daumas, but not all of them are available.

In this course, I show how algorithms and proofs can be described in the calculus of inductive constructions as it is implemented in the Coq system. The lectures are organized as follows.

1. Dependent types and their use in performing proofs
2. Inductive type, recursive programming, and proofs by induction
3. Adding dependency to inductive types, inductive properties
4. Strong specifications
5. Modelling general recursion, well-founded recursion
6. Reflective tactics
7. Extraction, models of imperative programs, Co-Inductive types (if we have enough time)

The course is supported with a collection of on-machine exercises, which we only distribute for each session, and a collection of homework assignments. The topics of these exercises cover varied aspects of mathematics and algorithms: proving that the square root of 2 is non rational, verifying the correctness of parsing and sorting algorithms, verifying algorithms in arithmetics, compilation, proving that some typed calculus is strongly normalizing, etc...

References

• Yves Bertot, Pierre Castéran
  Interactive Theorem Proving and Program Development: Coq'Art: The Calculus of Inductive Constructions, Springer Verlag, EATCS Texts in Theoretical Computer Science, ISBN 3-540-20854-2 (associated internet site).