Cancelled Interactive Proof Assistants (IPA)

Interactive theorem proving is concerned with carrying out machine-checked proofs and developing the systems that check these proofs—proof assistants. Proof assistants, like Coq, Lean, and Isabelle, are used today to build highly critical systems and verify deep mathematical results. Landmark achievements in this area include formally verified compilers, operating system kernels, and distributed systems, as well as formal proofs of deep mathematical results, such as the four-colour, the Feit–Thompson, and Gödel's incompleteness theorems, and the Kepler conjecture.

The IPA course is a hands-on course about using a proof assistant to construct formal models of algorithms, protocols, and programming languages and to reason about their properties. The focus is on applying logical methods to concrete problems. The course will demonstrate the challenges of formal rigour and the benefits of machine support in modeling, proving and validating.

In the course, we will use the Isabelle proof assistant. The course is structured in two parts: The first part introduces basic and advanced modeling techniques (functional programs, inductive definitions, modules), the associated proof techniques (term rewriting, resolution, induction, proof automation), and compilation of the models to certified executable code. In the second part, the students work in groups on a project assignment in which they apply these techniques: they build a formal model and prove its desired properties. The project lies in the area of programming languages, model checking, and information security.