Einführung

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. The content is independent, but it may be easier to attend the courses together.

Zeitplan

The course will include several longer slots in order to end before the end of the semester.

Sprache

Englisch

Voraussetzungen

Knowledge about functional programming and logic.