Theory and Practice of Rocq
This is a slightly updated version of a lecture I gave at TU Dortmund in the years 2020 and 2021. Some of the tutorials and exercises require CoqHammer. The tutorial files have been tested with Coq 8.19.
Description
Since the beginning of the 21st century, formal proof methods have become standard in industrial hardware verification, particularly in CPU verification (Intel, AMD). During the past decade, the proof assistant technology has matured enough to also enable formal certification of substantial software systems. Major success stories include the seL4 operating system microkernel, the CompCert optimising C compiler, and the CakeML implementation of Standard ML. Recently, deductive program verification has attracted increasing attention in the software industry (Microsoft, Amazon, Facebook, Galois). To quote Nikhil Swamy from Microsoft Research:
Today, what seemed impossible just a few years ago is becoming a reality. We can, in certain domains, produce fully verified software at a nontrivial scale and with runtime performance that meets or exceeds the best unverified software.
This lecture is about writing functional programs in a dependently typed language and proving them correct.
Rocq (formerly Coq) - the 2013 ACM Software System Award winner - is an interactive proof assistant for the development of formally certified software and mathematical theories. Its underlying theory is the Calculus of Inductive Constructions - a variant of dependent type theory with inductive types. The lecture covers programming and proving in Rocq, dependent type theory, and applications to program verification. The focus is on dependently typed functional programming, verification of functional programs, proof automation, theoretical foundations of inductive and dependent types.
Prerequisites
Some experience with functional programming and formal logic. You should understand mathematical induction. If you liked the logic and/or the functional programming bachelor courses then this lecture is for you. If you’re interested in formal methods and security then this may also be for you. The lecture is reasonably self-contained - previous knowledge of type theory is not necessary.
Supplementary materials
- Certified Programming with Dependent Types and Formal Reasoning About Programs by Adam Chlipala.
- Software Foundations by Benjamin C. Pierce et. al.
- Interactive Theorem Proving and Program Development by Yves Bertot and Pierre Casteran.
- Inductive definitions in the system Coq: rules and properties by Christine Paulin-Mohring.
- History of Interactive Theorem Proving by John Harrison, Josef Urban and Freek Wiedijk.
Lectures (theory)
- Introduction
- The Curry-Howard isomorphism
- Higher-order logic
- Dependent types and the Calculus of Constructions
- Inductive types
- Equality
Rocq tutorials
- Functional programming in Rocq
- Basic logic and proofs
- Higher-order logic
- Equality
- Induction
- Inductive specifications
- Universes and axioms
- Sorting
- Executable specifications
- Strong automation with CoqHammer
- Proof automation with Ltac
- Dependent types
- Type classes, mergesort and the Function command
- Positivity, large elimination and induction schemes
- More dependent types
- Dependent pattern matching, the Program command and well-founded recursion
- Dependently typed expressions
- Dependent merge
- Equality reasoning with dependent types
- Equations package
- Program extraction
- Hoare logic
Exercises
- Functional programming I
- Functional programming II
- The Curry-Howard isomorphism
- Logic; Induction
- Induction; Higher-order logic
- More induction
- Inductive definitions
- Induction; Universes
- Sorting; Fibonacci
- Ltac; Arithmetic expressions; Dependent types
- Type classes; Recursors
- Search trees I; Dependent pattern matching; Termination
- Search trees II