| session |
date |
topics |
slides |
thys |
solutions |
|---|
| 1 |
06.03 |
history and motivation, first steps, functional programming in HOL |
pdf (x1, x4) |
zip |
thy |
| 2 |
13.03 |
Isabelle basics, higher-order logic, structured proof |
pdf (x1, x4) |
zip |
thy |
| 3 |
20.03 |
finding theorems, natural deduction, case analysis, structural induction |
pdf (x1, x4) |
zip |
thy |
| 4 |
27.03 |
type definitions, simplification, calculational reasoning |
pdf (x1, x4) |
zip |
thy |
| 5 |
03.04 |
PSL - A high-level proof strategy language, Isabelle/ML |
pdf |
|
|
| 6 |
10.04 |
sledgehammer, inductive definitions, rule inversion, rule induction |
pdf (x1, x4) |
zip |
thy |
| 7 |
08.05 |
code generation, computation induction, multisets |
pdf (x1, x4) |
zip |
thy |
| 8 |
15.05 |
session management, document preparation, sets |
pdf (x1, x4) |
zip |
thy |
| 9 |
22.05 |
proof methods, well-foundedness, manual termination proofs |
pdf (x1, x4) |
zip |
thy |
| 10 |
29.05 |
notation, type classes |
pdf (x1, x4) |
zip |
thy |
| 11 |
05.06 |
locales, data type invariants |
pdf (x1, x4) |
zip |
thy |
| 12 |
12.06 |
semester projects |
pdf (x1, x4) |
|
|
| 13 |
19.06 |
the archieve of formal proofs, the certification approach, IsaFoR/CeTA |
pdf (x1, x4) |
zip |
|