Interactive Theorem Proving Project

CS-642 / 4 crédits

Enseignant: Pit-Claudel Clément

Langue: Anglais

Remark: Next time: spring 2027

Frequency

Every year

Summary

A project-focused introduction to interactive theorem proving.

Content

Sample topics:

-    Intro to the interactive theorem proving (Rocq, logic, higher-order functions, tactics)
-    Functional programming (inductive types and fixpoints)
-    Structural induction (data structures and verified algorithms)
-    Interpreter-based program semantics (intro to compiler verification)
-    Inductive relations (predicates, rule induction)

Note

Assessments: Take-home assignments, in-class quizzes, formal verification project

Learning objectives: Plan and carry out mechanized proofs

Learning Prerequisites

Recommended courses

CS320, CS550

 

Resources

Moodle Link

Dans les plans d'études

  • Forme de l'examen: Multiple (session libre)
  • Matière examinée: Interactive Theorem Proving Project
  • Cours: 2 Heure(s)
  • Projet: 70 Heure(s)
  • TP: 40 Heure(s)
  • Type: optionnel

Semaine de référence

Cours connexes

Résultats de graphsearch.epfl.ch.