### 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.