Lectures

Slides and Isabelle files will be made available online as the lectures progress.
  • Isabelle hints
  • Week 1, Mon: intro
    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]
  • Week 2, Mon: typed lambda calculus
    slides 1-per-page [pdf], slides 4-per-page [pdf], demo [thy]
  • Week 2, Thu: 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, 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, Mon: 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, more confluence
    slides 1-per-page [pdf], slides 4-per-page [pdf], demo [thy]
  • Week 5, Mon: sets, type definitions, inductive predicates
    slides 1-per-page [pdf], slides 4-per-page [pdf], demo [thy]
  • Week 5, Thu: inductive predicates, rule induction formally
    slides 1-per-page [pdf], slides 4-per-page [pdf], demo [thy], solution [thy]
  • Week 6, Mon: datatypes, datatype induction, primitive recursion
    slides 1-per-page [pdf], slides 4-per-page [pdf], demo [thy], solution [thy]
  • Week 6, Thu: regular expressions
    demo (done during lecture)[thy], solution[thy]
  • Week 7, Mon: general recursive functions
    slides 1-per-page [pdf], slides 4-per-page [pdf], demo [thy], solution [thy]
  • Week 7, Thu: automatic proof and disproof
    slides 1-per-page [pdf], slides 4-per-page [pdf], demo [thy]
  • Week 8, Mon: Semantics and Hoare logic
    slides 1-per-page [pdf], slides 4-per-page [pdf], demo [thy]
  • Week 8, Thu: Weakest precondition, verification condition
    slides 1-per-page [pdf], slides 4-per-page [pdf] , demo [thy]
  • Week 9, Mon: Shallow Embedding, State Monads
    slides 1-per-page [pdf], slides 4-per-page [pdf], records demo [thy], monad demo [thy]
  • Week 9, Thu: C verification, AutoCorres
    slides 1-per-page [pdf], slides 4-per-page [pdf], demo [thy], C file [c], C-Parser and AutoCorres [tar.gz] (from AutoCorres website)
  • Week 10, Mon: Public Holiday
  • Week 10, Thu: Eisbach, proof method language (guest lecture)
  • Week 11, Mon: Isar
    slides 1-per-page [pdf], slides 4-per-page [pdf], demo [thy], solution [thy]
  • Week 11, Thu: more Isar (datatypes, calculational reasoning) and code generation
    slides 1-per-page [pdf], slides 4-per-page [pdf], demo [thy]
  • Week 12, Mon: Type classes, Locales
    slides 1-per-page [pdf], slides 4-per-page [pdf], demo [thy]
  • Week 13, Thu: AutoCorres demos
    plus demo [c] [thy], fib demo [c] [thy], mult by add demo [c] [thy]