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