| week |
date |
topics |
slides |
sources |
exercises |
|---|
| 01 |
09.03 |
Organization, Introduction, Higher-Order Logic |
pdf (x4) |
Demo.thy |
thy |
| 02 |
16.03 |
Pure Framework, Structured Proofs |
pdf (x4) |
Demo.thy Live.thy |
thy |
| 03 |
23.03 |
Structured Proofs Continued, Case Analysis and Induction |
pdf (x4) |
Demo.thy Live.thy |
thy |
| 04 |
30.03 |
Induction Revisited, Calculational Reasoning, Simplifier |
pdf (x4) |
Demo.thy Live.thy |
thy |
| 05 |
20.04 |
Function Definitions Revisited, Manual Termination Proofs, Attributes |
pdf (x4) |
Demo.thy Live.thy |
thy |
| 06 |
27.04 |
Projects, Proof Methods, Sledgehammer |
pdf (x4) |
Demo.thy Live.thy |
thy |
| 07 |
04.05 |
Inductive Definitions, Rule Inversion and Induction |
pdf (x4) |
Demo.thy Live.thy |
thy |
| 08 |
11.05 |
Sets and Lists in Isabelle, Case Study: Binary Search Trees |
pdf (x4) |
Demo.thy Live.thy |
thy |
| 09 |
25.05 |
Typedef, Lifting and Transfer |
pdf (x4) |
Demo.thy Live.thy |
thy |
| 10 |
01.06 |
Code Generation Part 1 |
pdf (x4) |
Demo.thy Live.thy |
thy |
| 11 |
15.06 |
Code Generation Part 2 |
pdf (x4) |
Demo.thy Live.thy |
thy |
| 12 |
22.06 |
Sessions, Document Preparation, Type Classes |
pdf (x4) |
Demo.thy Live.thy |
thy |
| 13 |
29.06 |
Further Topics, Master Projects |
pdf (x4) |
Demo.thy Live.thy |
|