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 (theory and practice). It presents
application of the Coq proof assistant to proof of programs and covers
both functional and imperative programs.
Summary
-
07/12 - CP - Introduction to Coq theory, Inductive Definitions 1.
Slides 1&2, TD 1, Coq solution for TD 1.
- 14/12 - CP - Inductive Definitions 2.
Slides 1&2, TD 2, Coq solution for TD 2.
- 04/01 - BB - Functional Programming 1, structural versus well-founded induction, partial function, coinductive definitions.
Slides 3, TD 3, Coq solution for TD 3.
- 11/01 - BB - Functional Programming 2, monadic constructions, modules.
Models, realisability, extraction. Slides 4, TD 4, Coq solution for TD 4.
- 18/01 - BB - Architecture of a proof assistant, automated versus interactive proofs, tactic language. TD 5.
- 25/01 - GM - Proofs by reflection. Slides 6, TD 6, Coq solution for TD 6.
- 01/02 - GM - Proof of imperative programs. Slides 7, TD 7.
- 08/02 - Support for project.
- 15/02 - GM - Floating-point arithmetic. Automated proofs. Slides 8.1, Slides 8.2, TD 8, ACSL solution for TD 8.
- 01/03 - Exam.
- 08/03 - Project defense.
Course notes
Project
-
With each course, there will be a practical session on computers.
- 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.
- Subject of the project 2010/11 (pdf)
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.