The dates and events shown here are dynamically displayed from Stud.IP.
Therefore, if you have any questions, please contact the person listed under the item Lehrende/DozentIn (Lecturers) directly.
Lecture: 2.01.803 Interactive Theorem Proving
Semester:
Winter term
2025
2.01.803 Interactive Theorem Proving -
Event date(s) | room
- Dienstag, 14.10.2025 10:00 - 12:00 | A02 3-334
- Donnerstag, 16.10.2025 14:00 - 16:00 | A04 2-201 (Rechnerraum)
- Dienstag, 21.10.2025 10:00 - 12:00 | A02 3-334
- Donnerstag, 23.10.2025 14:00 - 16:00 | A04 2-201 (Rechnerraum)
- Dienstag, 28.10.2025 10:00 - 12:00 | A02 3-334
- Donnerstag, 30.10.2025 14:00 - 16:00 | A04 2-201 (Rechnerraum)
- Dienstag, 4.11.2025 10:00 - 12:00 | A02 3-334
- Donnerstag, 6.11.2025 14:00 - 16:00 | A04 2-201 (Rechnerraum)
- Dienstag, 11.11.2025 10:00 - 12:00 | A02 3-334
- Donnerstag, 13.11.2025 14:00 - 16:00 | A04 2-201 (Rechnerraum)
- Dienstag, 18.11.2025 10:00 - 12:00 | A02 3-334
- Donnerstag, 20.11.2025 14:00 - 16:00 | A04 2-201 (Rechnerraum)
- Dienstag, 25.11.2025 10:00 - 12:00 | A02 3-334
- Donnerstag, 27.11.2025 14:00 - 16:00 | A04 2-201 (Rechnerraum)
- Dienstag, 2.12.2025 10:00 - 12:00 | A02 3-334
- Donnerstag, 4.12.2025 14:00 - 16:00 | A04 2-201 (Rechnerraum)
- Dienstag, 9.12.2025 10:00 - 12:00 | A02 3-334
- Donnerstag, 11.12.2025 14:00 - 16:00 | A04 2-201 (Rechnerraum)
- Dienstag, 16.12.2025 10:00 - 12:00 | A02 3-334
- Donnerstag, 18.12.2025 14:00 - 16:00 | A04 2-201 (Rechnerraum)
- Dienstag, 6.1.2026 10:00 - 12:00 | A04 2-201 (Rechnerraum)
- Donnerstag, 8.1.2026 14:00 - 16:00 | A04 2-201 (Rechnerraum)
- Dienstag, 13.1.2026 10:00 - 12:00 | A04 2-201 (Rechnerraum)
- Donnerstag, 15.1.2026 14:00 - 16:00 | A04 2-201 (Rechnerraum)
- Dienstag, 20.1.2026 10:00 - 12:00 | A04 2-201 (Rechnerraum)
- Donnerstag, 22.1.2026 14:00 - 16:00 | A04 2-201 (Rechnerraum)
- Dienstag, 27.1.2026 10:00 - 12:00 | A04 2-201 (Rechnerraum)
- Donnerstag, 29.1.2026 14:00 - 16:00 | A04 2-201 (Rechnerraum)
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.
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.
Lecturers
SWS
4
Lehrsprache
deutsch und englisch