Introduction
This course provides knowledge about interactive theorem proving with a focus on the Isabelle proof assistant using higher-order logic (HOL). The following topics will be discussed:- higher-order logic
- Isabelle's proof language Isar
- natural deduction in Isabelle
- functional programming in Isabelle
- inductive definitions
- code generation
- selection of advanced topics