Homotopy Type Theory (HoTT)5 ECTS
(englische Bezeichnung: Homotopy Type Theory)

Lehrveranstaltungen:

• • Homotopy Type Theory
    (Seminar, 2 SWS, Sergey Goncharov et al., Mi, 14:15 - 15:45, Übung 3 / 01.252-128)

Inhalt:

Homotopy Type Theory (HoTT) is a new approach to foundations of logic, programming and mathematics. It has an increasingly powerful impact on the development of the modern type-theory based tools for programming and verification, such as Coq proof assistant and Agda programming language.
The idea of the seminar is to provide a primer in HoTT and use the corresponding material to practice and improve research skills, such as being able to work with the literature, comprehend scientific texts, summarise and explain the material studied in front of an audience.
We plan to use the material from the HoTT book (https://homotopytypetheory.org/book ) as a basis for the seminar. The actual topics will be discussed and distributed between students depending on their background and interests.
Please see https://www8.cs.fau.de/ss17:hott for more.

Lernziele und Kompetenzen:

Wissen

Students explain the role of type theory in computer science, especially in modern tools for programming and verification like Coq and Agda.

Verstehen

Student understand the practical impact of foundational developments.

Anwenden

Students apply the concepts and apparatus of Homotopy Type Theory (HoTT), critically comparing it with previously existing type-theoretical frameworks for programming and verification like the Martin-Loef type theory or the Calculus of Inductive Constructions.

Analysieren

Students read scientific publications and analyse their contents. Students select material suitable for 90-minute oral presentations. They prepare presentations and deliver the presentations to other seminar participants.

Literatur:

The HoTT Book: https://homotopytypetheory.org/book

Verwendbarkeit des Moduls / Einpassung in den Musterstudienplan:
Das Modul ist im Kontext der folgenden Studienfächer/Vertiefungsrichtungen verwendbar:

1. Informatik (Bachelor of Arts (2 Fächer))
   (Po-Vers. 2010 | TechFak | Informatik (Bachelor of Arts (2 Fächer)) | Seminar | Seminar)
2. Informatik (Bachelor of Arts (2 Fächer))
   (Po-Vers. 2013 | TechFak | Informatik (Bachelor of Arts (2 Fächer)) | Seminar | Seminar)
3. Informatik (Bachelor of Science)
   (Po-Vers. 2007 | TechFak | Informatik (Bachelor of Science) | Seminar)
4. Informatik (Bachelor of Science): 3-5. Semester
   (Po-Vers. 2009s | TechFak | Informatik (Bachelor of Science) | Seminare, Praktika, Bachelorarbeit | Seminar)
5. Informatik (Bachelor of Science): 3-5. Semester
   (Po-Vers. 2009w | TechFak | Informatik (Bachelor of Science) | Seminare, Praktika, Bachelorarbeit | Seminar)
6. Informatik (Master of Science)
   (Po-Vers. 2010 | TechFak | Informatik (Master of Science) | Seminar, Projekt, Masterarbeit | Seminar)

Studien-/Prüfungsleistungen:

Homotopy Type Theory (Prüfungsnummer: 974785)

(englischer Titel: Homotopy Type Theory)

Prüfungsleistung, Seminarleistung, Dauer (in Minuten): 90, benotet

Anteil an der Berechnung der Modulnote: 100.0 %

weitere Erläuterungen:
Die Prüfungsleistung besteht in einer Ausarbeitung und einem 90-minütigen erfolgreichen Vortrag.

Prüfungssprache: Englisch

Erstablegung: SS 2017, 1. Wdh.: WS 2017/2018

1. Prüfer:

Lutz Schröder