Teachers
Objectives
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.
Summary
-
8 lectures covering the detailed program below.
With each course, there will be a practical session on computers.
- Exam.
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.
Program
Lectures:
-
[12/08, BB]
Introduction to lambda-calculus, Curry-Howard isomorphism and
dependent types.
(slides, TP1
, template and solution)
-
[12/15, BB]
Caluclus of Constructions, Metatheory.
(slides, TP2
and solution)
-
[1/5, BB]
Introduction to Inductive Types.
(slides, TP3
and solution)
-
[1/12, BB]
Theory of Inductive Types.
(slides, TP4
and solution)
Exams:
Course notes
Archives
Archive of projects
Archive of
exams
This document was translated from LATEX by
HEVEA.