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

Lectures (theory)

  1. Introduction
  2. The Curry-Howard isomorphism
  3. Higher-order logic
  4. Dependent types and the Calculus of Constructions
  5. Inductive types
  6. Equality

Rocq tutorials

  1. Functional programming in Rocq
  2. Basic logic and proofs
  3. Higher-order logic
  4. Equality
  5. Induction
  6. Inductive specifications
  7. Universes and axioms
  8. Sorting
  9. Executable specifications
  10. Strong automation with CoqHammer
  11. Proof automation with Ltac
  12. Dependent types
  13. Type classes, mergesort and the Function command
  14. Positivity, large elimination and induction schemes
  15. More dependent types
  16. Dependent pattern matching, the Program command and well-founded recursion
  17. Dependently typed expressions
  18. Dependent merge
  19. Equality reasoning with dependent types
  20. Equations package
  21. Program extraction
  22. Hoare logic

Exercises

  1. Functional programming I
  2. Functional programming II
  3. The Curry-Howard isomorphism
  4. Logic; Induction
  5. Induction; Higher-order logic
  6. More induction
  7. Inductive definitions
  8. Induction; Universes
  9. Sorting; Fibonacci
  10. Ltac; Arithmetic expressions; Dependent types
  11. Type classes; Recursors
  12. Search trees I; Dependent pattern matching; Termination
  13. Search trees II