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.
- Support for project.
- Exam.
- Project defense.
The evaluation is done with a written exam and optionally a
project. The final score is the max of the exam score and the
average of the exam and project.
Program
Lectures:
-
[07/12, BB]
Introduction to Coq theory, Calculus of Constructions.
(slides)
- [14/12 and 04/01, BB]
Inductive Definitions.
(slides 14/12
04/01,
TD2 (solution),
TD3 (solution))
- [11/01, AM]
Functional Programming: structural versus well-founded
induction, partial function, monadic constructions, coinductive
definitions. (slides,
TD4 solution)
- [18/01, AM]
Modelisation: modules, structures, type classes. Examples:
algebra, finite sets
(slides,
TD5 solution)
- [18/01 and 25/01, AM]
Small Scale Reflection (slides,
TD6 solution).
- [25/01, AM]
Modelisation of real numbers allowing efficient computations.
- [01/02, BB]
Models: consistency, strong normalisation, realizability.
(no slides, TD7 insertion.v
solution)
- [08/02, BB]
Extraction of pure functional programs.
Support for project: 15/02
Exams:
-
[29/02] Written exam.
- [04/03] Project submission deadline. New!
- [07/03] Project defense.
Course notes
Project
-
This year’s project: Deciding
Presburger arithmetic
- The project should be done individually using the Coq proof
assistant. We request the Coq source file with comments and a small
report (max 5 pages). There will be a defense.
Archive of projects
Archive of exams
This document was translated from LATEX by
HEVEA.