Lectures
Slides and Isabelle files will be made available online as the lecture progresses.- Isabelle hints
- 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] - 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, more confluence
slides 1-per-page [pdf], slides 4-per-page [pdf], demo [thy] - Week 5, Tue: 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, Tue: 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 (incomplete)[thy] - Week 7, Tue: regular expressions (part 2), general recursive functions
Reg Exp solution [thy], 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], solution [thy] - Week 8, Tue: Semantics and Hoare logic
slides 1-per-page [pdf], slides 4-per-page [pdf], demo [thy], solution [thy] - Week 8, Thu: Weakest precondition, verification condition
slides 1-per-page [pdf], slides 4-per-page [pdf], demo [thy], solution [thy] - Week 9, Mon: C verification, SIMPL
slides 1-per-page [pdf], slides 4-per-page [pdf], demo [thy], Simpl [zip] (from afp.sf.net) - Week 9, Thu: C verification, memory model
slides 1-per-page [pdf], slides 4-per-page [pdf], demo [thy], C-Parser and autocorres [tar.gz] (from autocorres website), list_reverse [thy], list_reverse [C], selection_sort [thy], selection_sort [C], - Week 10, Tue: Autocorres and monads
slides 1-per-page [pdf], demo [thy], union.c [c], C-Parser and autocorres [tar.gz] (from autocorres website) - Week 10, Thu: Autocorres and monads background
slides 1-per-page [pdf] - Week 11, Tue: 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], solution [thy] - Week 12, Tue: Type classes, Locales
slides 1-per-page [pdf], slides 4-per-page [pdf], demo [thy] - Week 12, Thu: exam preparations
demo [thy], C file written during lecture [c], Isabelle proof for C file, written during lecture [thy].