Lectures

Slides and Isabelle files will be made available online as the lecture progresses.
  • Isabelle hints
  • Week 1, Mon: intro, installing Isabelle
    slides 1-per-page [pdf], slides 4-per-page [pdf], demo [thy]
  • Week 1, Wed: untyped lambda calculus
    slides 1-per-page [pdf], slides 4-per-page [pdf], demo [thy]
  • Week 2, Mon: typed lambda calculus
    slides 1-per-page [pdf] slides 4-per-page [pdf]
  • Week 2, Wed: HOL, natural deduction for propositional logic
    slides 1-per-page [pdf], slides 4-per-page [pdf], demo [thy]
  • Week 3, Mon: HOL, quantifiers, automation
    slides 1-per-page [pdf], slides 4-per-page [pdf], demo [thy]
  • Week 3, Wed: defining HOL from scratch, more automation
    slides 1-per-page [pdf], slides 4-per-page [pdf], HOL demo [thy] automation demo [thy]
  • Week 4, Mon: term rewriting, confluence, termination
    slides 1-per-page [pdf], slides 4-per-page [pdf], introductory demo [thy] simp demo [thy]
  • Week 4, Wed: conditional term rewriting, congruence rules, more confluence
    slides 1-per-page [pdf], slides 4-per-page [pdf], demo [thy]
  • Week 5, Mon: Isar, readable proofs
    slides 1-per-page [pdf], slides 4-per-page [pdf], demo [thy]
  • Week 5, Wed: assignment 1 feedback
  • Week 6, Mon: sets, type definitions, inductive predicates
    slides 1-per-page [pdf], slides 4-per-page [pdf], demo [thy]
  • Week 6, Wed: inductive predicates, rule induction formally
    slides 1-per-page [pdf], slides 4-per-page [pdf], demo [thy]
  • Week 7, Mon: datatypes, datatype induction, primitive recursion
    slides 1-per-page [pdf], slides 4-per-page [pdf], demo [thy] solution [thy]
  • Week 7, Wed: datatype methods in Isar, regular expressions (part 1)
    slides 1-per-page [pdf], slides 4-per-page [pdf], demo [thy], RegExp (incomplete) [thy]
  • Week 8, Mon: regular expressions (part 2), feedback assignment 2
    RegExp [thy]
  • Week 8, Wed: general recursive functions
    slides 1-per-page [pdf], slides 4-per-page [pdf], demo [thy]
  • Week 9, Mon: calculational reasoning and code generation
    slides 1-per-page [pdf], slides 4-per-page [pdf], demo [thy].
    Also: question for previous year's assignement 3: [pdf], [thy]
  • Week 9, Wed: Automatic Proof and Disproof in Isabelle/HOL guest lecture by Tobias Nipkow from TU Munich
    slides 1-per-page [pdf] demo [thy] Aux [thy]. You will also need to install a copy of the AFP for the Demo to work on red-black trees.
  • Week 10, Mon: semantics, Hoare logic
    slides 1-per-page [pdf], slides 4-per-page [pdf], demo [thy]
  • Week 10, Wed: Weakest precondition, verification condition
    slides 1-per-page [pdf], slides 4-per-page [pdf], demo [thy]
  • Week 11, Mon: public holiday
  • Week 11, Wed: C verification, SIMPL
    slides 1-per-page [pdf], slides 4-per-page [pdf], demo [thy], Simpl [zip] (from afp.sf.net)
  • Week 12, Mon: C verification, memory model
    slides 1-per-page [pdf], slides 4-per-page [pdf], demo [thy]
  • Week 12, Wed: exam preparations
    demo [thy]