Lecture: 2.01.803 Interactive Theorem Proving - Details

Lecture: 2.01.803 Interactive Theorem Proving - Details

General information

Course name Lecture: 2.01.803 Interactive Theorem Proving
Subtitle inf803
Course number 2.01.803
Semester WiSe25/26
Current number of participants 5
expected number of participants 15
Home institute Department of Computing Science
Courses type Lecture in category Teaching
First date Tuesday, 14.10.25, 10:00 - 12:00 o'clock A02 3-334
Type/Form V+Ü
Lehrsprache deutsch und englisch

Rooms and times

A02 3-334

  • Tuesday, 10:00 - 12:00, Weekly (from 14.10.25)
  • Thursday, 14:00 - 16:00, Weekly (from 16.10.25)

Module assignments

Comment/Description

In this course, we will delve into the exciting field of interactive theorem proving, an area central to both formal methods in computer science and mathematical logic. Proof assistants help users construct and verify mathematical proofs interactively. They check each step of your reasoning for correctness, provide powerful automation to support proof development, and flag errors that might be difficult to spot manually. These tools are widely employed in both academic research and industry to verify critical software, hardware designs, and complex mathematical theorems where absolute certainty is needed.

We will begin by revisiting the foundations and consider different logics and reasoning systems. We will work with various proof techniques and apply them in the proof assistant Isabelle. Thereby, learning not just how to construct proofs, but also how to verify their correctness using the powerful interactive prover Isabelle/HOL.

A large part of the course will be dedicated to practical exercises. Along the way, we will also learn fundamentals of functional programming (used in Isabelle). Finally, we plan a multi-week project formalizing and verifying the classic result connecting deterministic and nondeterministic finite automata - a result you may recognize from GTI.

Join us to discover how computer-assisted proving opens new possibilities for mathematicians and computer scientists, and gain practical skills. Any questions regarding the course can be directed to Caroline Lemke.

Admission settings

The course is part of admission "Anmeldung gesperrt (global)".
Erzeugt durch den Stud.IP-Support
The following rules apply for the admission:
  • Admission locked.