Lectures

Slides and Isabelle files will be made available online as the lectures progress.
  • Isabelle hints
  • Week 1, Tue: intro
    slides [pdf], slides with animations [pdf], demo [thy]
  • Week 1, Wed: untyped lambda calculus
    slides [pdf], slides with animations [pdf], demo [thy]
  • Week 2, Tue: typed lambda calculus
    slides [pdf], slides with animations [pdf], demo [thy]
  • Week 2, Wed: HOL, natural deduction for propositional logic
    slides [pdf], slides with animations [pdf], demo [thy] demo solution [thy]
  • Week 3, Tue: HOL, quantifiers, automation, Isar (part 1)
    slides [pdf], slides with animations [pdf], demo [thy], demo solution [thy], Isar demo [thy], Isar demo solution [thy]
  • Week 3, Wed: defining HOL from scratch, more automation
    slides [pdf], slides with animations [pdf], HOL demo [thy] automation demo [thy]
  • Week 4, Tue: term rewriting, confluence, termination
    slides [pdf], slides with animations [pdf], introductory demo [thy] simp demo [thy]
  • Week 4, Wed: conditional term rewriting, congruence rules, more confluence
    slides [pdf], slides with animations [pdf], demo [thy]
  • Week 5, Tue: sets, type definitions, inductive predicates
    slides [pdf], slides with animations [pdf], demo [thy], demo solutions [thy]
  • Week 5, Wed: inductive predicates, rule induction formally
    slides [pdf], slides with animations [pdf], demo [thy], solution [thy]
  • Week 6, Tue: datatypes, datatype induction, primitive recursion
    slides [pdf], slides with animations [pdf], demo [thy], solution [thy]
  • Week 6, Wed: automatic proof and disproof, Isar (part 2)
    slides [pdf], slides with animations [pdf], demo [thy], Isar demo [thy]
  • Week 7, Tue: rule induction tutorual
    demo [thy] (as developed in the lecture)
  • Week 7, Wed: general recursive functions
    slides [pdf], slides with animations [pdf], demo [thy]
  • Week 8, Tue: Semantics and Hoare logic
    slides [pdf], slides with animations [pdf], demo [thy], demo solutions[thy]
  • Week 8, Wed: Weakest precondition, verification condition
    slides [pdf], slides with animations [pdf], demo [thy], demo solutions[thy]
  • Week 9, Tue: Shallow Embedding, State Monads
    slides [pdf], slides with animations [pdf], records demo [thy], monad demo (Monads) [thy] monad demo (Monads solution) [thy] monad demo (GCD) [thy] monad demo (GCD solution) [thy] monad demo (While) [thy]
  • Week 9, Wed: C verification, AutoCorres
    slides [pdf], slides with animations [pdf], demo [thy], C file [c], C-Parser and AutoCorres [tar.gz]
  • Week 10, Tue: Invariant practice
    slides [pdf], slides with animations [pdf], demo [thy], demo solutions[thy]
  • Week 10, Wed: exam preparations
    2014 exam papers: exam [pdf], C file [c], Isabelle template [thy] (with bonus question).
    2014 exam solution: [pdf, thy].