Course on mechanization of proofs
Joëlle Despeyroux
Graduate course given at the
Dea in CS at the University of Nice SophiaAntipolis (UNSA),
with Yves Bertot and Laurent Théry; Spring 2000.
Instructor is Joëlle Despeyroux, except otherwise stated.
(Slides are only available in french.)
 Introduction:
Induction principles.
1st examples of proofs in the domain of certified software
(slides)
 Introduction to Type Theory:

Natural deduction, typed lambdacalculus, the CurryHoward isomorphism,
dependant types, the Calculus of Constructions
(slides)

Type Theory at work: the Coq system. Instructor: Yves Bertot.
(slides)

Further notes on the CurryHoward isomorphism
(slides)
The Calculus of Inductive Constructions
(slides)

Induction and inversion principles at work in the Coq system.
Instructor: Yves Bertot
(slides)

Some exercices on the computer.
Instructors: Laurent Théry and Loïc Pottier
 Certified software:

Informal proofs. MiniML: evaluation and compilation
(slides)

Formalization of functional languages
(slides)
MiniML: further evaluations and typing
(slides)
 Certified algorithms.
Instructor: Laurent Théry
(slides)
 Further topics:
Other proof assistants: Isabelle, HOL, PVS. Instructor: Laurent Théry
(slides)
Yves Bertot,
Joëlle Despeyroux,
Laurent Théry.