| week |
date |
topics |
slides |
sources |
exercises |
|---|
| 01 |
07.03 |
Organization, Introduction, Higher-Order Logic |
pdf (x4) |
Demo.thy Live.thy |
thy |
| 02 |
14.03 |
Pure Framework, Structured Proofs |
pdf (x4) |
Demo.thy Live.thy |
thy |
| 03 |
21.03 |
Structured Proofs Continued, Case Analysis and Induction |
pdf (x4) |
Demo.thy Live.thy |
thy |
| 04 |
11.04 |
Induction Revisited, Calculational Reasoning, Simplifier |
pdf (x4) |
Demo.thy Live.thy |
thy |
| 05 |
18.04 |
Function Definitions Revisited, Manual Termination Proofs, Attributes |
pdf (x4) |
Demo.thy Live.thy |
thy |
| 06 |
25.04 |
Projects, Proof Methods, Sledgehammer |
pdf (x4) |
Demo.thy Live.thy |
thy |
| 07 |
02.05 |
Inductive Definitions, Rule Inversion and Induction |
pdf (x4) |
Demo.thy Live.thy |
thy |
| 08 |
16.05 |
Sets and Lists in Isabelle, Case Study: Binary Search Trees |
pdf (x4) |
Demo.thy Live.thy |
thy |
| 09 |
23.05 |
Typedef, Lifting and Transfer |
|
|
|
| 10 |
06.06 |
Code Generation Part 1 |
|
|
|
| 11 |
13.06 |
Code Generation Part 2 |
|
|
|
| 12 |
20.06 |
Sessions, Document Preparation, Type Classes |
|
|
|
| 13 |
27.06 |
Further Topics, Master Projects |
|
|
|