Hauptseminar Mathematische Logik (S2A2)/ Graduate seminar on Logic (S4A4)
Dozenten
- Prof. Dr. Peter Koepke
- Dr. Philipp Schlicht
Zeit und Ort
- Dienstag, 16.15-18.00 Uhr, Seminarraum 1.007.
- Beginn: 18.04.2017
Inhalt
We will study type theory and lambda calculus, following the notes on Type Theory and Functional Programming by Simon Thompson, available on his webpage.
Programm
- 1. Untyped lambda-calculus [30] - Flock/Ranosch
- 2. Expressiveness [41] - Baker/Tepavcevic
- 3. Typed lambda-calculus [42] - Hamm/Slot
- 4. Propositional logic [67] - Barisic/Kraasch
- 5. Curry-Howard isomorphism [78] - Jakobs/Yalcinoglu
- 6. Quantifiers [88] - Troebst/Weigt
- 7. Natural numbers [100] - Campigotto
- 8. Equality [106] - Stassen/Ribelles
- 9. Girard's paradox - Henke/Vicari
- 10. Homotopy - Frerix
- 11. Homotopy type theory - Chen/Zaiser