On this page:
The lectures are given by:
The Teaching Assistant (TA) is:
If you run into difficulties and are not making satisfactory progress then seek help. The earlier you ask for help the more likely it is that your problems can be solved without damaging your performance in the course. This is a challenging course, which introduces you to novel techniques and skills. You are expected to learn them over a short period of time.
To seek help
Various kinds of feedback are provided during the course.
Lectures are held at 15.10-16.00 in Semester 1. Details:
The first lecture is on Tuesday 20th September 2016.
Note that there are no lecture notes for the course. Instead, recommended reading is associated with each lecture. This reading is usually from:
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.
Please note: At any point of the course, the future schedule gives a strong indication of the topics to be covered. However, some details might change.
|1||Tue 20th Sep 2016||1. Introduction||Bundy, Ch. 1
[background] Formal Proof by Tom Hales.
|Fri 23rd Sep 2016||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||Tue 27th Sep 2016||3. Natural Deduction and Starting with Isabelle
— Isabelle Theory file for Lecture 3
|H&R Sec 1.2, 1.4
Sec 5.1-5.7 of Tutorial on Isabelle/HOL
Prop.thy Isabelle theory file
|Fri 30th Sep 2016||4. Propositional Reasoning in Isabelle
Sec 5.1-5.7 of Tutorial
[background] Pollack's How to Believe a Machine-Checked Proof
[background] How do they verify a verifier of formalized proofs?
|3||Tue 4th Oct 2016||5. First-order Logic
H&R Secs 2.1-2.4
FOL.thy Isabelle theory file
[background] Logitext - an interactive L-system FOL prover
|Fri 7th Oct 2016||6. Representation
||Bundy Ch. 4|
|4||Tue 11th Oct 2016||7. Introduction to Higher Order Logic in Isabelle||
Sec 1.1-1.4 of Tutorial
N&K Sec 2.1-2.2
|Fri 14th Oct 2016||8. Representation II: Locales in Isabelle/HOL
— Isabelle Theory file for Lecture 8
|Tutorial on Locales
[background] Interpretation of Locales in Isabelle
|5||Tue 18th Oct 2016||9. Coursework: Proving and Reasoning in Isabelle/HOL||See coursework files|
|Fri 21st Oct 2016||10. Isar — A Language for
— Isar Demo Theory
|The Isabelle/Isar Quick
N&K Ch. 5
|6||Tue 25th Oct 2016||11. Program Verification using Hoare Logic
— Lecture by Petros Papapanagiotou
— 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).
|Fri 29th Oct 2016||12. Write your own Theorem Prover
— Lecture by Phil Scott
|7||Tue 1st Nov 2016||13. Unification||Bundy, Sec 17.1-17.4|
|Fri 4th Nov 2016||14. Rewriting I||Bundy, Ch. 9
Sec 3.1 of Tutorial on Isabelle/HOL
|8||Tue 8th Nov 2016||15. Rewriting II||Bundy, Ch. 9
|Fri 11th Nov 2016||16.|
|9||Tue 15th Nov 2016||17.|
|Fri 18th Nov 2016||18.|
|10||Tue 22nd Nov 2016||19.|
|Fri 25th Nov 2016||20.
|3||Tutorial 1: Propositional logic and some Isabelle
|4||Tutorial 2: First order logic and more Isabelle
|5||Tutorial 3: Representation and reasoning in Isabelle using locales
|6||Tutorial 4: Structured proofs in Isabelle
|7||Tutorial 5: Reasoning about Hoare Logic in Isabelle [thy]
|A riddle: The rich grandfather||[pdf][thy]|
|A Bad Axiomatization||[pdf][thy]|
There will be one item of assessed coursework for this course, which will count for 40% of the overall mark (the other 60% is assessed by exam).
The dates for the coursework are as follows:
Informatics Forum, 10 Crichton Street, Edinburgh, EH8 9AB, Scotland, UK
Tel: +44 131 651 5661, Fax: +44 131 651 1426, E-mail: firstname.lastname@example.org
Please contact our webadmin with any comments or corrections. Logging and Cookies
Unless explicitly stated otherwise, all material is copyright © The University of Edinburgh