Proof Assistants

Aims

This module introduces students to interactive theorem proving using Isabelle and Coq. It includes techniques for specifying formal models of software and hardware systems and for deriving properties of these models.

 

Syllabus

• Introduction to proof assistants and logic.
• Reasoning in predicate logic and typed set theory.
• Reasoning in dependent type theory.
• Inductive definitions and recursive functions: modelling them in logic, reasoning about them.
• Modelling operational semantics definitions and proving properties.

 

Objectives

On completion of this module, students should:

• possess good skills in the use of Isabelle and Coq;
• be able to specify inductive definitions and perform proofs by induction;
• be able to formalise and reason about a variety of specifications in a proof assistant.

Coursework

Practical sessions will allow students to develop skills. Some of the exercises will serve as the basis for assessment.

Assessment

Assessment will be based on two marked assignments (due in weeks 5 and 8) with students performing small formalisation and verification projects in a proof assistant together with a write-up explaining their work (word limit 2,500 per project for the write-up). Each of the assignments will be worth 100 marks, distributed as follows:

• 50 marks for completing basic formalisation and verification tasks assessing grasp of the material taught in the lecture. Students will submit their work as theory files for either the Isabelle or Coq proof assistant, and they will be assessed for correctness and completeness of the specifications and proofs.
• 20 marks for completing designated more challenging tasks, requiring the use of advanced techniques or creative proof strategies.
• 30 marks for a clear write-up explaining the design decisions made during the formalisation and the strategy used for the proofs, where 10 of these marks will be reserved for write-ups of exceptional quality, e.g. demonstrating particular insight.

The main tasks in the assignments will be designed to assess the student's proficiency with the basic material and techniques taught in the lectures and the practical sessions, while the more challenging tasks will give exceptional students the opportunity to earn distinction marks

Recommended reading

Nipkow, T., Klein, G. (2014). Concrete Semantics with Isabelle/HOL. (The first part of this book, “Programming and Proving in Isabelle/HOL”, comes with the Isabelle distribution.) 

Nipkow, T., Paulson, L.C. and Wenzel, M. (2002). A proof assistant for higher-order logic. Springer LNCS 2283. 

The Software Foundations series of books, in particular the first two:

• Pierce, B., Azevedo de Amorim, A., Casinghino, C., Gaboardi, M., Greenberg, M., Hriţcu, C., Sjöberg, V., Yorgey, B. (2023). Logical Foundations 
• Pierce, B., Azevedo de Amorim, A., Casinghino, C., Gaboardi, M., Greenberg, M., Hriţcu, C., Sjöberg, V., Tolmach, A., Yorgey, B. (2023). Programming Language Foundations 

Chlipala, A. (2022). Certified programming with dependent types: a pragmatic introduction to the Coq proof assistant. MIT Press. 

Sergey, I. (2014). Programs and Proofs: Mechanizing Mathematics with Dependent Types. 

All of these are freely available online.