Lectures

Slides and Isabelle files will be made available online as the lecture progresses.
  • ProofGeneral/XEmacs reference card [pdf]
  • Isabelle Cheat Sheet by Jeremy Avigad [pdf]
  • Week 1, Tue: intro, installing Isabelle
    slides 1-per-page [pdf], slides 4-per-page [pdf], demo [thy]
  • Week 1, Thu: untyped lambda calculus
    slides 1-per-page [pdf], slides 4-per-page [pdf], demo [thy], list exercise [pdf]
  • Week 2, Tue: typed lambda calculus
    slides 1-per-page [pdf] slides 4-per-page [pdf]
  • Week 2, Thu: HOL, natural deduction for propositional logic
    slides 1-per-page [pdf], slides 4-per-page [pdf], demo [thy]
  • Week 3, Tue: HOL, quantifiers, automation
    slides 1-per-page [pdf], slides 4-per-page [pdf], demo [thy]
  • Week 3, Thu: defining HOL from scratch, more automation
    slides 1-per-page [pdf], slides 4-per-page [pdf], HOL demo [thy] automation demo [thy]
  • Week 4, Tue: term rewriting, confluence, termination
    slides 1-per-page [pdf], slides 4-per-page [pdf], introductory demo [thy] simp demo [thy]
  • Week 4, Thu: conditional term rewriting, congruence rules
    slides 1-per-page [pdf], slides 4-per-page [pdf], demo [thy]
  • Week 5, Tue: Isar, readable proofs
    slides 1-per-page [pdf], slides 4-per-page [pdf], demo [thy]
  • Week 5, Thu: assignment 1 feedback
  • Week 6, Tue: sets, type definitions, inductive predicates
    slides 1-per-page [pdf], slides 4-per-page [pdf], demo [thy]
  • Week 6, Thu: inductive predicates, rule induction formally
    slides 1-per-page [pdf], slides 4-per-page [pdf], demo [thy]
  • Week 7, Tue: datatypes, datatype induction, primitive recursion
    slides 1-per-page [pdf], slides 4-per-page [pdf], demo [thy]
  • Week 7, Thu: 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, Tue: regular expressions (part 2), feedback assignment 2
    RegExp [thy]
  • Week 8, Thu: general recursive functions
    slides 1-per-page [pdf], slides 4-per-page [pdf], demo [thy]
  • Week 9, Tue: calculational reasoning and code generation
    slides 1-per-page [pdf], slides 4-per-page [pdf], demo [thy]
  • Week 9, Thu: semantics, Hoare logic
    slides 1-per-page [pdf], slides 4-per-page [pdf], demo [thy]
  • Week 10, Tue: Automatic Proof and Disproof in Isabelle/HOL guest lecture by Tobias Nipkow from TU Munich
    slides 1-per-page [pdf] demo [thy] Aux [thy] Red-Black Trees [thy] (the demo will only work with a current (Sep'11) development version of Isabelle and a matching version of the AFP)
  • Week 10, Thu: Weakest precondition, verification condition
    slides 1-per-page [pdf], slides 4-per-page [pdf], demo [thy], demo with solution[thy]
  • Week 11, Tue: C verification, SIMPL
    slides 1-per-page [pdf], slides 4-per-page [pdf], demo [thy], Simpl [zip] (from afp.sf.net)
  • Week 11, Thu: C verification, memory model
    slides 1-per-page [pdf], slides 4-per-page [pdf], demo [thy]
  • Week 12, Tue: Type classes and Locales
    slides 1-per-page [pdf], slides 4-per-page [pdf], demo [thy]