Interactive Theorem Proving

Motivation

Interactive theorem proving is used by several research groups at the Department of Information Technology, including the Algorithmic Program Verification group, the Concurrency group, and the Programming Languages group. It is also employed at the Department of Mathematics, e.g., in the context of the CAPA (Computer-Aided Proofs in Analysis) project.

More generally, interactive theorem proving is a well-known formal verification technique, is widely used in the programming languages community, and has gained traction also with mathematicians, since it allows to prove highly non-trivial theorems with utmost rigor.

Course Contents

This course is aimed at PhD students. It will give a hands-on introduction to interactive theorem proving, using the proof assistant Isabelle/HOL. The following topics will be covered:

Introduction to higher-order logic and Isabelle/HOL
Reasoning in predicate logic and typed set theory
Recursive datatypes and functions: modeling and reasoning about them
Inductive definitions
Modeling operational semantics and proving properties of programs
Declarative proofs
Automated and semi-automated theorem proving

On completion, students should be proficient in the use of Isabelle/HOL for formal modeling and verification.

Course Structure

The course will consist of approx. 11 lectures and 4 labs, where students will use Isabelle/HOL to solve exercises and carry out a small theorem proving project. Student work will be assessed. PhD students who successfully complete the course will receive 5 credits (provided their supervisor agrees).

Schedule

Date	Time	Room	Topic
Thursday, May 4	13:15 - 15:00	1345	Introduction
Tuesday, May 9	15:15 - 17:00	1345	Isabelle Theories
Wednesday, May 10	15:15 - 17:00	1345	Elementary Proof
Friday, May 12	13:15 - 15:00	1406	Lab 1: Replace, Reverse and Delete (.thy)
Tuesday, May 16	15:15 - 17:00	1345	Advanced Recursion, Induction and Simplification
Wednesday, May 17	15:15 - 17:00	1345	Logic in Isabelle
Friday, May 19	13:15 - 15:00	2415b	Lab 2: Power, Sum (.thy)
Tuesday, May 23	15:15 - 17:00	2415b	Structured Proofs
Wednesday, May 24	10:15 - 12:00	1345	Sets
Wednesday, May 24	15:15 - 17:00	1345	Lab 3: Euler's Totient Function (.thy) [assessed]
			Deadline: Friday, June 9 at 12:00
Tuesday, May 30	15:15 - 17:00	1345	Inductive Definitions
Wednesday, May 31	10:15 - 12:00	1345	Structured Induction Proofs
Wednesday, June 7	15:15 - 17:00	1345	Operational Semantics
Thursday, June 8	15:15 - 17:00	1345	Modelling Hardware
Friday, June 9	13:15 - 15:00	1345	Lab 4: The Binary Euclidean Algorithm (.thy) [assessed]
			Deadline: Friday, June 30 at 12:00

For the assessed exercises, please submit your solution—a working Isabelle theory file including brief informal explanations—by email before the respective deadline.

Course Materials

Most course material is taken (with permission) from Prof. Larry Paulson's course Interactive Formal Verification at the University of Cambridge.

Slides

Please install Isabelle on your own laptop before the first lecture. Extensive Isabelle documentation is available, both on-line and as part of the Isabelle distribution. In particular, you may want to read Programming and Proving in Isabelle/HOL by Tobias Nipkow.

You are strongly encouraged to attempt additional exercises beyond those handed out for the labs. To become proficient with Isabelle, you should attempt a variety of exercises, and perhaps even develop your own.

Feel free to contact me by email (tjark.weber@it.uu.se) or in person if you have any questions about this course.

Last modified: 2017-06-07