This page contains my current plan for the tutorial I will be giving in Vienna.
Block 1
| Day 1 | Day 2 | Day 3 | |
|---|---|---|---|
| 9:30–10:30 | General introduction on ITPs (optional) | Code generation (optional) | The rules of the game (optional) |
| ACL2, Coq, Lean, Isabelle, HOL, … | Theory | Low level Isabelle | |
| 10:45–11:45 | Isabelle as programming language | Isar language (light version) | Exercises |
| (definition, fun, and value) | |||
| (Lunch break) | |||
| 13:30–14:30 | First theorems | Exercises | |
| LRAT? | |||
| 15:00–16:00 | Exercises | Exercises continued |
Block 2: Advanced Isabelle
| Day 4 | Day 5 | Day 6 | |
|---|---|---|---|
| 9:30–10:30 | Sledgehammer and encoding (optional) | Refinement (optional) | IsaSAT |
| Theory | |||
| 10:45–11:45 | Proof reconstruction (optional) | Exercises | Discussion |
| Resolving two clauses without duplicate | |||
| 13:00-14:00 | Eisbach and automation (optional) | Imperative code (depends on refinement | |
| Official tutorial | session) Theory | ||
| 14:15-15:15 | Exercises | Exercises | |
| Resolution continued |