Course on mechanization of proofs

Joëlle Despeyroux

Graduate course given at the Dea in CS at the University of Nice Sophia-Antipolis (UNSA), with Yves Bertot and Laurent Théry; Spring 2000.
Instructor is Joëlle Despeyroux, except otherwise stated. (Slides are only available in french.)
  1. Introduction:
    Induction principles. 1st examples of proofs in the domain of certified software (slides)
  2. Introduction to Type Theory:
    1. Natural deduction, typed lambda-calculus, the Curry-Howard isomorphism, dependant types, the Calculus of Constructions (slides)
    2. Type Theory at work: the Coq system. Instructor: Yves Bertot. (slides)
    3. Further notes on the Curry-Howard isomorphism (slides)
      The Calculus of Inductive Constructions (slides)
    4. Induction and inversion principles at work in the Coq system. Instructor: Yves Bertot (slides)
    5. Some exercices on the computer. Instructors: Laurent Théry and Loïc Pottier
  3. Certified software:
    1. Informal proofs. MiniML: evaluation and compilation (slides)
    2. Formalization of functional languages (slides)
      MiniML: further evaluations and typing (slides)
  4. Certified algorithms.
    Instructor: Laurent Théry (slides)
  5. Further topics:
    Other proof assistants: Isabelle, HOL, PVS. Instructor: Laurent Théry (slides)
Yves Bertot, Joëlle Despeyroux, Laurent Théry.