AR: Lecture Schedule
Lecture times and place:
- Mondays, 13.10-14.00, AT 2.04.
- Thursdays, 13.10-14.00, AT 2.11.
There will be one lecture on the coursework assignment to provide some general information and background.
Note:
- These lectures do not necessarily coincide with the hand-out dates for the assignment sheet. Students should start work on their coursework as soon as they are handed out rather than wait for the lectures, if these come later on.
- The links to the quizzes will appear here when available.
Note also:
- CAUTION: These slides are being updated for the AY 2024/25, with some topics still to be confirmed (TBC).
- At any point of the course, the future schedule gives a strong indication of the topics to be covered. However, some details may still change.
Week | Date | Topic | Slides | Recommended reading | Quizzes (auto-marked, anonymous) | Exercises + Labs |
1 | 16 Sep 2024 | 1. Introduction | [background] Bundy, Ch. 1 [background] Formal Proof by Tom Hales. [background] Logicomix | Quiz 1 | Exercise: Propositional logic and some Isabelle | |
19 Sep 2024 | 2. Propositional Logic and Natural Deduction | H&R Sec 1.1, 1.2, 1.3, start of 1.4 [background] Wadler's Propositions as Types | ||||
2 | 23 Sep 2024 | 3. Natural Deduction and Starting with Isabelle — Isabelle Theory file — Isabelle Theory file | H&R Sec 1.2, 1.4 Sec 5.1-5.7 of Tutorial on Isabelle/HOL | Quiz 2 | Exercise: Propositional logic and some Isabelle | |
26 Sep 2024 | 4. Propositional Reasoning in Isabelle | Sec 5.1-5.7 of Tutorial on Isabelle/HOL [background] Pollack's How to Believe a Machine-Checked Proof [background] How do they verify a verifier of formalized proofs? [Quick Guide] Isabelle Cheat Sheet | ||||
3 | 30 Sep 2024 | 5. First-order Logic — Isabelle Theory file | H&R Secs 2.1-2.4 [background] Logitext - an interactive L-system FOL prover | Quiz 3 | Exercise: First order logic and more Isabelle
| |
3 Oct 2024 | 6. Introduction to Higher Order Logic in Isabelle | Sec 1.1-1.4 of Tutorial on Isabelle/HOL N&K Sec 2.1-2.2 | ||||
4 | 7 Oct 2024 | 7. Locales in Isabelle/HOL — Isabelle Theory file | Tutorial on Locales [background] Interpretation of Locales in Isabelle | Quiz 4 | Exercise: Representation and reasoning in Isabelle using locales Lab: Additional Isabelle exercises Coursework released: 11 Oct 2024 | |
10 Oct 2024 | 8. Isar — A Language for Structured Proofs — Isar Demo Theory | [Quick Guide] The Isabelle/Isar Quick Reference Manual N&K Ch. 5 | ||||
5 | 14 Oct 2024 | 9. Inductive Proof (in Isabelle) — Isabelle Theory file | H&R Sec 1.4.2 [background] The Automation of Mathematical Induction | Quiz 5 | Exercise: Structured proofs in Isabelle | |
17 Oct 2024 | 10. Program Verification using Hoare Logic (I) — Isabelle's Hoare Logic library | H&R Sec 4.1-4.3 N&K Sec 12.2.1 [background] Reading on Hoare Logic (especially pages 1-27, 37-48). | ||||
6 | 21 Oct 2024 | 11. Program Verification using Hoare Logic (II) — Isabelle Theory file | TBC | Exercise: Reasoning about Hoare Logic, Induction [thy]
Lab: Coursework | ||
24 Oct 2024 | 12. Coursework: Proving and Reasoning in Isabelle/HOL | See coursework files on Assessment page. | ||||
7 | 28 Oct 2024 | 13. TBC | TBC | Exercise: Reasoning about Hoare Logic, Induction
Lab: Coursework | ||
31 Oct 2024 | 14. TBC | |||||
8 | 4 Nov 2024 | Coursework Q&A with Teaching Assistant | None | Exercise: TBC
Lab: Coursework | ||
7 Nov 2024 | 15. TBC | |||||
9 | 11 Nov 2024 | 16. TBC | None | Exercise: TBC
Lab: Coursework | ||
14 Nov 2024 | Exam Review | None | Past papers (Note: Papers before 2016-17 also contain material not in the current course): — A comprehensive selection is available here. | |||
10 | 18 Nov 2024 | No lecture | Exercise: None Lab: None Coursework deadline: 18 Nov 2024 at 12:00 | |||
21 Nov 2024 | No lecture |
License
All rights reserved The University of Edinburgh