Event
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.
Event
2.01.489 Formal Foundations of Programming Languages -
Event date(s) | room
- Dienstag, 13.10.2026 14:00 - 16:00 | A03 2-214
- Donnerstag, 15.10.2026 14:00 - 16:00 | A03 2-214
- Dienstag, 20.10.2026 14:00 - 16:00 | A03 2-214
- Donnerstag, 22.10.2026 14:00 - 16:00 | A03 2-214
- Dienstag, 27.10.2026 14:00 - 16:00 | A03 2-214
- Donnerstag, 29.10.2026 14:00 - 16:00 | A03 2-214
- Dienstag, 3.11.2026 14:00 - 16:00 | A03 2-214
- Donnerstag, 5.11.2026 14:00 - 16:00 | A03 2-214
- Dienstag, 10.11.2026 14:00 - 16:00 | A03 2-214
- Donnerstag, 12.11.2026 14:00 - 16:00 | A03 2-214
- Dienstag, 17.11.2026 14:00 - 16:00 | A03 2-214
- Donnerstag, 19.11.2026 14:00 - 16:00 | A03 2-214
- Dienstag, 24.11.2026 14:00 - 16:00 | A03 2-214
- Donnerstag, 26.11.2026 14:00 - 16:00 | A03 2-214
- Dienstag, 1.12.2026 14:00 - 16:00 | A03 2-214
- Donnerstag, 3.12.2026 14:00 - 16:00 | A03 2-214
- Dienstag, 8.12.2026 14:00 - 16:00 | A03 2-214
- Donnerstag, 10.12.2026 14:00 - 16:00 | A03 2-214
- Dienstag, 15.12.2026 14:00 - 16:00 | A03 2-214
- Donnerstag, 17.12.2026 14:00 - 16:00 | A03 2-214
- Dienstag, 5.1.2027 14:00 - 16:00 | A03 2-214
- Donnerstag, 7.1.2027 14:00 - 16:00 | A03 2-214
- Dienstag, 12.1.2027 14:00 - 16:00 | A03 2-214
- Donnerstag, 14.1.2027 14:00 - 16:00 | A03 2-214
- Dienstag, 19.1.2027 14:00 - 16:00 | A03 2-214
- Donnerstag, 21.1.2027 14:00 - 16:00 | A03 2-214
- Dienstag, 26.1.2027 14:00 - 16:00 | A03 2-214
- Donnerstag, 28.1.2027 14:00 - 16:00 | A03 2-214
Description
Type theory lies at the foundations of programming languages: Every time a compiler accepts a well-typed program, it proves basic correctness properties. The same theory is at work when proof assistants certify a mathematical theorem. This course offers an introduction to the theory of type systems from simply-typed lambda calculus to recursive types, linear types, and dependent types. Proofs will be carried out in the interactive theorem prover Lean and on the board.
Lecturers
SWS
4
Lehrsprache
englisch