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 readingQuizzes
(auto-marked, anonymous)
Exercises + Labs
 
116 Sep 20241. IntroductionPDF[background] Bundy, Ch. 1 
[background] Formal Proof by Tom Hales. 
[background] Logicomix
Quiz 1Exercise: Propositional logic and some Isabelle
19 Sep 20242. Propositional Logic and Natural DeductionPDF 
H&R Sec 1.1, 1.2, 1.3, start of 1.4 
[background] Wadler's Propositions as Types
223 Sep 20243. Natural Deduction and Starting with Isabelle
Isabelle Theory file
Isabelle Theory file
PDF
H&R Sec 1.2, 1.4 
Sec 5.1-5.7 of Tutorial on Isabelle/HOL
Quiz 2Exercise: Propositional logic and some Isabelle
26 Sep 20244. Propositional Reasoning in IsabellePDF
[Quick Guide] Isabelle Cheat Sheet
330 Sep 20245. First-order Logic
Isabelle Theory file
PDF
H&R Secs 2.1-2.4  
[background] Logitext - an interactive L-system FOL prover
Quiz 3

Exercise: First order logic and more Isabelle

 

Lab: Additional Isabelle exercises

3 Oct 20246. Introduction to Higher Order Logic in IsabellePDFSec 1.1-1.4 of Tutorial on Isabelle/HOL
N&K Sec 2.1-2.2
47 Oct 20247. Locales in Isabelle/HOL
Isabelle Theory file
PDFTutorial 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 20248. Isar — A Language for Structured Proofs
Isar Demo Theory
PDF[Quick Guide] The Isabelle/Isar Quick Reference Manual
N&K Ch. 5
514 Oct 20249. Inductive Proof (in Isabelle)
Isabelle Theory file
PDFH&R Sec 1.4.2 
[background] The Automation of Mathematical Induction
Quiz 5Exercise: Structured proofs in Isabelle
17 Oct 202410. Program Verification using Hoare Logic (I)
Isabelle's Hoare Logic library
PDFH&R Sec 4.1-4.3 
N&K Sec 12.2.1 
[background] Reading on Hoare Logic (especially pages 1-27, 37-48).
621 Oct 202411. Program Verification using Hoare Logic (II) 
Isabelle Theory file
PDF TBC

Exercise: Reasoning about Hoare Logic, Induction [thy]

 

Lab: Coursework

24 Oct 202412. Coursework: Proving and Reasoning in Isabelle/HOLPDFSee coursework files on Assessment page.
728 Oct 202413. TBCPDF TBC

Exercise: Reasoning about Hoare Logic, Induction

 

Lab: Coursework

31 Oct 202414. TBCPDF 
84 Nov 2024Coursework Q&A with Teaching AssistantPDF None

Exercise: TBC

 

Lab: Coursework

7 Nov 202415. TBCPDF 
     911 Nov 202416. TBCPDF None

Exercise: TBC

 

Lab: Coursework

14 Nov 2024Exam ReviewNone

Past papers (Note: Papers before 2016-17 also contain material not in the current course):

A comprehensive selection is available here.

1018 Nov 2024No lecture
 
  

Exercise: None

Lab: None

Coursework deadline: 18 Nov 2024 at 12:00
 

21 Nov 2024No lecture   
License
All rights reserved The University of Edinburgh