en | de

Interactive Theorem Proving in Isabelle/HOL

master program

VU3  SS 2024  703315


Content and Schedule

week date topics slides sources exercises
01 07.03 Organization, Introduction, Higher-Order Logic pdf (x4) Demo.thy Live.thy thy
02 14.03 Pure Framework, Structured Proofs pdf (x4) Demo.thy Live.thy thy
03 21.03 Structured Proofs Continued, Case Analysis and Induction pdf (x4) Demo.thy Live.thy thy
04 11.04 Induction Revisited, Calculational Reasoning, Simplifier pdf (x4) Demo.thy Live.thy thy
05 18.04 Function Definitions Revisited, Manual Termination Proofs, Attributes pdf (x4) Demo.thy Live.thy thy
06 25.04 Projects, Proof Methods, Sledgehammer pdf (x4) Demo.thy Live.thy thy
07 02.05 Inductive Definitions, Rule Inversion and Induction pdf (x4) Demo.thy Live.thy thy
08 16.05 Sets and Lists in Isabelle, Case Study: Binary Search Trees pdf (x4) Demo.thy Live.thy thy
09 23.05 Typedef, Lifting and Transfer pdf (x4) Demo.thy Live.thy thy
10 06.06 Code Generation Part 1 pdf (x4) Demo.thy Live.thy thy
11 13.06 Code Generation Part 2 pdf (x4) Demo.thy Live.thy thy
12 20.06 Sessions, Document Preparation, Type Classes pdf (x4) Demo.thy Live.thy thy
13 27.06 Further Topics, Master Projects pdf (x4) Demo.thy Live.thy