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: 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.

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 Home Valid HTML 4.01 Transitional Valid CSS