Introduction to Interactive Theorem Proving with Coq

This page covers the PhD course on "Introduction to Interactive Theorem Proving with Coq" at the University of Milan, offered in Feb 2022.

Course Overview

We give an overview of interactive theorem proving with the Coq proof assistant, applied to the verification of software correctness. We will also touch upon the integration of testing and proving. Our main examples are drawn from the theory of programming languages; mechanizing the specification of programming languages and their semantics, and reasoning over individual programs as well as over generic program transformations, as typically found in compilers. Some possible topics:

Operational semantics: small-step, big-step, definitional interpreters.
Hoare logic.
Compilation to virtual machine code and its proof of correctness.
Type systems and proof of soundness.

Doing proofs in a system such as Coq usually requires months to master. In these lectures we will instead use Coq mostly as a specification language and exploit some recent advances in machine-learning driven automation to delegate to the system most of the proofs

These lectures are based on Xavier Leroy's course "Mechanized semantics with applications to program proof and compiler verification", held at the Verification Technology, Systems & Applications summer school 2013. We are very grateful to Xavier for granting permission to use his materials.

Prerequisites

familiarity with functional programming (Ocaml, Haskell, but Python may suffice)
basic knowledge of first-order logic
interest (if not competence) in the semantics of programming languages (interpreters, type systems, compilers)

Outcome

You will have an appreciation of the role of formal methods and ITP in writing correct programs and designing correct PL artifacts. You will not become a Coq wizard, but you'll be able to read and write simple specifications and hopefully have them proved by the automation.

Examination

Some simple exercises in Coq for the bravest or a presentation of a paper/system to be agreed.

Enrollment and practicalities

The course has been offered in hybrid modality.

Learning Material

Coq in a hurry by Yves Bertot
Course notes by Xavier Leroy
More on the Teams channel

Course Structure

Lecture 1: Introduction (21/2)

Formal verification and program correctness
Famous bugs in software history
The role of logic: a brief history of theorem proving and its application to software correctness

Lecture 2: Coq Boot-camp (23/2)

Logic in Coq
functions and datatypes
inductive definitions
tactics vs. automation

Lecture 3: Program Correctness (25/2)

Operational semantics of IMP
Hoare logics
Proving a program correct
An overview of applications and systems
Code