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

Draft syllabus

-    Intro to the Coq proof assistant (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)
-    Automation and tactics I (bottom-up reasoning and logic programming)
-    Operational program semantics (small- and big-step semantics)
-    Program logics (hoare triples)
-    Automation and tactics II (top-down reasoning)
-    Type systems (Simply-typed lambda calculus)
-    Dependent types and equality proofs
-    Automation and tactics III (proofs by reflection)
-    Real-world interactive theorem proving (guest lecture)


Teaching methods: (e.g., ex cathedra, in-lab project, field trip)
-    Lectures

-   Live-coding sessions

Expected student activities:
-    Weekly programming and verification assignments

Assessment methods:
-    Take-home programming and verification assignments

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)
  • Type: optional

Reference week

Related courses

Results from graphsearch.epfl.ch.