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