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

#### Lecture 4: "Well-typed programs can't go wrong" (28/2)

- Proving properties of a programming language
- Type systems and type preservation
- Case study: Typed Arithmetic Language from Software Foundations
- Code