Interactive Theorem Proving Project

CS-642 / 4 credits

Teacher: Pit-Claudel Clément

Language: English

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

In the programs

  • Exam form: Multiple (session free)
  • Subject examined: Interactive Theorem Proving Project
  • Courses: 2 Hour(s)
  • Project: 70 Hour(s)
  • TP: 40 Hour(s)
  • Type: optional

Reference week

Related courses

Results from graphsearch.epfl.ch.