CS-628 / 4 credits

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

Language: English

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 by crafting simple


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

Learning Prerequisites

Required courses

-    Formal Verification (CS-550)
-    Computer language processing (CS-320)

Recommended courses

-    Formal Verification (CS-550)
-    Computer language processing (CS-320)



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

Moodle Link

In the programs

  • Number of places: 30
  • Exam form: During the semester (session free)
  • Subject examined: Interactive Theorem Proving CS
  • Lecture: 2 Hour(s)
  • Exercises: 1 Hour(s)
  • Practical work: 3 Hour(s)

Reference week