Lectures

Slides and Isabelle files will be made available online as the lectures progress. Lecture recordings are available this semester starting from week 3.
  • Isabelle hints
  • Week 1, Tue: intro
    slides [pdf], slides with animations [pdf], demo [thy]
  • Week 1, Fri: 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, Fri: HOL, natural deduction for propositional logic
    slides [pdf], slides with animations [pdf], demo [thy] demo solution [thy]
  • Week 3, Tue: HOL, quantifiers, automation
    slides [pdf], slides with animations [pdf], demo [thy], demo solution [thy]
  • Week 3, Fri: 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, Fri: 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]