en | de

Interaktives Beweisen in Isabelle/HOL

Masterstudium

VU3  SS 2026  703315


Content and Schedule

Woche Datum Themen Folien Quelltext Proseminar
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