This course study interactive proof assistants based on higher-order
type theory, and more specifically the Coq system. It studies
generalised inductive definitions and program extraction (theory and
practice). It presents application of the Coq proof assistant to
formal modelisation of mathematical concepts.
8 lectures covering the detailed program below.
With each course, there will be a practical session on computers.
The evaluation is done with a written exam and 2
exercices. The final score is the average of the written exam and
the average of the exercices.
Introduction to lambda-calculus, Curry-Howard isomorphism and
, template and solution)
Caluclus of Constructions, Metatheory.
Introduction to Inductive Types.
Theory of Inductive Types.
Archive of projects
This document was translated from LATEX by