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 | Exercises: 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 | Exercises: 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 | Exercises: 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 | Exercises: 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 | Exercises: 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). [Related material] Lecture 14 of Formal Verification course. | ||||
6 | 21 Oct 2024 | 11. Program Verification using Hoare Logic (II) — Isabelle Theory file | H&R Sec 4.1-4.3 N&K Sec 12.2.1 [background] Reading on Hoare Logic (especially pages 1-27, 37-48). [Related material] Lecture 14 of Formal Verification course. | None | Exercises: 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. Linear Temporal Logic I | H&R Sec 3.2 [Related material] Lecture 2 of Formal Verification course. | None | Exercises: Reasoning about Hoare Logic, Induction
Lab: Coursework | |
31 Oct 2024 | 14. No Lecture | |||||
8 | 4 Nov 2024 | Coursework Q&A with Teaching Assistant | None | Exercises: H&R 3.2 (3-7, page 246)
Lab: Coursework | ||
7 Nov 2024 | 15. Linear Temporal Logic II | H&R Sec 3.2 [background] De Giacommo and Vardi's Linear Temporal Logic and Linear Dynamic Logic on Finite Traces [background] Constrained Training of Neural Networks via Theorem Proving ( arXiv). | ||||
9 | 11 Nov 2024 | 16. A Verified Neurosymbolic Pipeline for Learning Linear Temporal Behaviour — Guest Lecture by Mark Chevallier | None | Exercise: H&R 3.2 (3-7, page 246)
Lab: Coursework | ||
14 Nov 2024 | Exam Review | None | Past papers (Note: Some of the questions cover topics that are 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 |