en | de

Interaktives Beweisen in Isabelle/HOL

Masterstudium

VU3  SS 2024  703315


Content and Schedule

Woche Datum Themen Folien Quelltext Proseminar
01 07.03 Organization, Introduction, Higher-Order Logic
02 14.03 Pure Framework, Structured Proofs
03 21.03 Structured Proofs Continued, Case Analysis and Induction
04 11.04 Induction Revisited, Calculational Reasoning, Simplifier
05 18.04 Function Definitions Revisited, Manual Termination Proofs, Attributes
06 25.04 Projects, Proof Methods, Sledgehammer
07 02.05 Inductive Definitions, Rule Inversion and Induction
08 16.05 Sets and Lists in Isabelle, Case Study: Binary Search Trees
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