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

Schedule

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

Language

English

Prerequisites

Knowledge about functional programming and logic.