One half of this module will consist of course work, the other half will consist of practical work on a machine. The course will finish with a project to be carried out in Coq. The first part of this course is a prerequisite for the Homotopy Type Theory course.
Functional programming in Coq
- Lambda-calculus, recursivity (and its limitations in Coq), ML style typing
- Common data structures (Boolean, integers, lists, options, trees, etc.)
- Generic programming: polymorphism, modules, type classes
- Dependent types
- Connections with other languages such as OCaml, presentation of the "absent" from Coq
(exceptions, imperative traits, input-output,...), how to make the link between OCaml and Coq
Formal proofs in Coq
- Specification language, basic logical rules
- Arithmetic, calculation, rewriting, recurrence
- Proof of properties of the usual data structures
- Inductive predicates
- Possibly: a quick overview of other proof assistants and comparison with Coq
- R. David, K. Nour et C. Raffalli, Introduction à la logique : théorie de la démonstration, Dunod, Paris, 2001.
- Y. Bertot et P. Castéran, Interactive Theorem Proving and Program Development. Coq'Art : The Calculus of Inductive Constructions. Springer Verlag, 2004.
- F. Wiedijk ed., The Seventeen Provers of the World, LNCS vol. 3600, Springer Verlag, 2006. http://www.cs.ru.nl/~freek/comparison/comparison.pdf