Interactive Theorem Proving
This course is an introduction to interactive theorem proving and advanced functional programming, mostly using the Coq proof assistant.
This course is for students interested in:
- The foundational theories of mathematics, most notably type theory and logic
- Practical interactive theorem proving in a state-of-the-art proof assistant
- Advanced functional programming languages and their relation to constructive mathematics via the “Curry-Howard Isomorphism”
- Program verification and “certified programming”
- Programming Language Semantics
The course can be found on Alma
Dozenten
Forum
Participants should register in the forum ps-forum.cs.uni-tuebingen.de and send a message to user binderd in order to be admitted to the subforum.
Schedule
The lecture will take place on the following dates:
- Tuesday, 12 c.t. - 14 in room F122 on the Sand
- Friday, 14 c.t. - 16 in room F122 on the Sand
The tutorials will take place on the following dates:
- Friday, 12 c.t. - 14 in room F122 on the Sand.