- Isabelle tutorial slides for Part I
- Isabelle tutorial for Part I
- Demo theories for Part I
- Slides for Part II
- Book for Part II
Until we can all meet safely in the classroom again, all lectures are will be replaced by video recordings of the same. We will use a mixture of TTT recordings from previous years and new recordings and live sessions. For each Friday (when the lecture would take place) we list which recordings to watch and what to read up to that date:
Part I, Introduction to Isabelle:
- 16.4. Watch #01 from 2018, read up to/incl 2.2.5 in prog-prove.pdf.
Note: at the very end of the lecture I could not demo the last proof (because of a problem with the projector). Do look at the full proof in Demos/List_Demo.thy.
- 23.4. Watch #02 from 2019, read up to/incl 2.5.3 in prog-prove.pdf.
- 30.4. Watch #03 from 2019, read up to/incl 3.3 in prog-prove.pdf.
- 07.5. Watch #04 from 2019, read up to/incl 4.1 (but without 3.5) in prog-prove.pdf.
- 14.5. Watch #05 from 2019, read up to the end of prog-prove.pdf.
Part II, Functional Data Structures:
- 21.5. Live session, read Chapters 1 and 2 from the book (up to but excl. 2.6)
- 28.5. Live session, read Chapters 4 - 6 from the book
- 04.6. Recording 31.5., read Chapters 7 and 8 from the book
- 11.6. Live session, read Chapters 10 and 12 from the book
- 18.6. Live session, read Chapters 14, 15 and 16 from the book
- 25.6. Live session, read Chapters 17 and 19 from the book
- 2.7. Live session, read Chapters 20 and 22 from the book
- 9.7. Live session, read Chapters 21 and 23 from the book
- 16.7. No lecture