Program requirementsprojet
TeacherAlexis Saurin
Weekly hours 2.0 h CM , 2.0 h TP
Years Master Logique Mathématique et Fondements de l'Informatique M2 Logos

Syllabus

One half of this module will consist of course work, the other half will consist of practical work on a machine. The course will finish with a project to be carried out in Coq. The first part of this course is a prerequisite for the Homotopy Type Theory course.

Contents

Functional programming in Coq

  • Lambda-calculus, recursivity (and its limitations in Coq), ML style typing
  • Common data structures (Boolean, integers, lists, options, trees, etc.)
  • Generic programming: polymorphism, modules, type classes
  • Dependent types
  • Connections with other languages such as OCaml, presentation of the "absent" from Coq (exceptions, imperative traits, input-output,...), how to make the link between OCaml and Coq

Formal proofs in Coq

  • Specification language, basic logical rules
  • Arithmetic, calculation, rewriting, recurrence
  • Proof of properties of the usual data structures
  • Inductive predicates
  • Automation
  • Possibly: a quick overview of other proof assistants and comparison with Coq

Bibliography