Introduction
This course provides an introduction to interactive theorem
proving.
The following topics will be discussed:
- design of an LCF prover
- structured and tactical proofs
- formal type theory and set theory
- Curry-Howard isomorphism and code extraction
- proof automation
Module
The courses "Interactive Theorem Proving" and "Interactive Theorem Proving
in Isabelle/HOL" are a part of the same Vertiefung/Module, and it is recommended
to attend the courses together.
Language
English
Prerequisites
Knowledge about functional programming and logic.