CS-628 / 6 crédits

Enseignant(s): Barrière Aurèle Aimé Aubin, Pit-Claudel Clément

Langue: Anglais

Remark: Spring 2024


Every year


A hands-on introduction to interactive theorem proving, proofs as programs, dependent types, and to the Coq proof assistant. Come learn how to write bug-free code!



Learning outcomes:

Implement purely-functional algorithms in the Gallina language; Translate informal requirements about software into precise mathematical properties; Plan and carry out mechanized proofs in Coq (e g maths algorithms compilers type systems); Automate repetitive proof tasks


Interactive theorem proving, verification, intuitionistic logic, program proofs, functional programming

Learning Prerequisites

Recommended courses

-    Formal Verification (CS-550)
-    Computer language processing (CS-320)
-    Foundations of software (CS-452)



-    https://softwarefoundations.cis.upenn.edu/
-    http://adam.chlipala.net/frap/
-    https://coq.inria.fr/distrib/current/refman/

Moodle Link

Dans les plans d'études

  • Forme de l'examen: Pendant le semestre (session libre)
  • Matière examinée: Interactive Theorem Proving CS
  • Cours: 2 Heure(s)
  • Exercices: 1 Heure(s)
  • TP: 3 Heure(s)

Semaine de référence

Cours connexes

Résultats de graphsearch.epfl.ch.