Lectures
Slides and Isabelle files will be made available online as the lectures progress.- Isabelle hints
- Week 1, Tue: intro
slides [pdf], demo [thy] - Week 1, Thu: untyped lambda calculus
slides [pdf], demo [thy] - Week 2, Tue: typed lambda calculus
slides [pdf], demo [thy] - Week 2, Thu: HOL, natural deduction for propositional logic
slides [pdf], demo [thy] - Week 3, Tue: HOL, quantifiers, automation
slides [pdf], demo [thy] - Week 3, Thu: defining HOL from scratch, more automation
slides [pdf], HOL demo [thy] automation demo [thy] - Week 4, Tue: term rewriting, confluence, termination
slides [pdf], introductory demo [thy] simp demo [thy] - Week 4, Thu: conditional term rewriting, congruence rules, more confluence
slides [pdf], demo [thy] - Week 5, Tue: sets, type definitions, inductive predicates
slides [pdf], demo [thy], demo solutions [thy] - Week 5, Thu: inductive predicates, rule induction formally
slides [pdf], demo [thy], solution [thy] - Week 6, Tue: datatypes, datatype induction, primitive recursion
slides [pdf], demo [thy], solution [thy] - Week 6, Thu: regular expressions
demo [thy], solution[thy] - Week 7, Tue: general recursive functions
slides [pdf], demo [thy] - Week 7, Thu: automatic proof and disproof
slides [pdf], demo [thy] - Week 8, Tue: Semantics and Hoare logic
slides [pdf], demo [thy] - Week 8, Thu: Weakest precondition, verification condition
slides [pdf], demo [thy] - Week 9, Tue: Shallow Embedding, State Monads
slides [pdf], records demo [thy], monad demo [thy] - Week 9, Thu: C verification, AutoCorres
slides [pdf], demo [thy], C file [c], C-Parser and AutoCorres [tar.gz] - Week 10, Tue: AutoCorres worked examples
plus demo [thy], C file [c];
mult by add demo [thy], C file [c];
fib demo [thy], C file [c] - Week 10, Thu: Eisbach, proof method language (guest lecture)
slides [pdf], demo [thy] - Week 11, Tue: Isar
slides [pdf], demo [thy] - Week 11, Thu: Type classes, Locales
slides [pdf], demo [thy] - Week 12, Tue: CakeML (guest lecture)
slides [pdf] - Week 12, Thu: exam preparations
2014 exam papers: exam [pdf], Isabelle template [thy], to be used with C-Parser and AutoCorres [tar.gz].
2014 exam solution: [pdf, thy].