CS-628 / 6 credits

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

Language: English

Remark: Spring 2024


Frequency

Every year

Summary

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!

Content

Note

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

Keywords

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)

Resources

Bibliography

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

Moodle Link

In the programs

  • 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

Related courses

Results from graphsearch.epfl.ch.