This course will cover a range of topics related to proof assistants based on dependent type theory, and more particularly the Rocq prover and Lean. The purpose of the course is to teach the foundations of dependently typed proof assistants, with their syntax and models. We then explain the intermediate layers sitting between the proof assistant and the users and how these can be extended. We finish the course with an overview of major mathematical libraries, both in Rocq and in Lean and on how to use them on examples.

We will thus cover the following topics:

• Syntax and models of the Caluclus of Inductive Constructions and Martin-Löf Type Theory.
• Overview of the Rocq system in practice: Gallina, vernacular, tactics, and meta-programming mechanisms.
• Metaprogramming in Rocq using Rocq-Elpi.
• The Rocq Mathematical Components library: structures and applications.
• An introduction to Lean and to the library Mathlib.

Organization

• 15 × 2h lectures/practical sessions
• 1 formalisation project
• 1 exam

Course Outline

1. General introduction to Rocq and the Calculus of Constructions (CC)
2. Syntax of the Calculus of Constructions and Categories with Families (CC)
3. Rocq tactics, SSReflect basics, and decision procedures (CC)
4. Inductive types, records, sigma types and subtypes (CC)
5. Inductive families, equality, setoids and dependent elmination (CC)
6. λ-prolog, Elpi, building a typechecker for STLC (ET)
7. Rocq-Elpi, representing Rocq terms, and a tour of Rocq API (ET)
8. Rocq-Elpi, meta-programming advanced tactics (ET)
9. The Mathcomp Library: Algebraic Hierarchies & Hierarchy Builder (ET)
10. The Mathcomp Library: Extensionality in an Intentional type theory (CC)
11. The Mathcomp-Analysis Library: topology and filters (CC)
12. An introduction to the Lean system and Mathlib (FN)
13. Functions, sets and quotients in Lean/Mathlib (FN)
14. Categories in Lean 1 (FN)
15. Categories in Lean 2 (FN)

Prerequisites

• Projet Fonctionel (L3 Info - ENS de Lyon) or any course in Functional Programming,
• Proofs and Programs (M1 ICA) or any course on System F or .