Functional programming and formal proofs in Coq
8 ECTS, semester 1, 12 weeks
|Weekly hours||2 h CM , 2 h TP|
|Years||M2 Logos Master Logique Mathématique et Fondements de l'Informatique|
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.