Abstract:

The course aims at giving to the students not only a basic introduction to the Coq proof assistant, but also enough background to access the Mathematical Components library (https://math-comp.github.io/math-comp), which provides extensive coverage of a variety of subjects, from the theory of basic data structures (e.g., numbers, lists, finite sets) to the theory of widespread mathematical objects (eg., groups, matrices, polynomials).

In particular the course covers the basics of Coq (how to define data types, write programs, state and prove theorems) as well as the two key formalization techniques adopted in the Mathematical Components library:

- the pervasive use of boolean reflection and of the SSReflect proof language

- the systematic use of algebraic structures to organize and access the contents of the library

The course is based on the Mathematical Components book, draft available at https://math-comp.github.io/mcb/.

The slides can be downloaded from http://www-sop.inria.fr/teams/marelle/types18/.