Seminar Curry-Howard Korrespondenz (SemCurry)5 ECTS
(englische Bezeichnung: Seminar Curry-Howard Correspondence)

Lehrveranstaltungen:

• • Seminar Curry-Howard Korrespondenz
    (Seminar, 2 SWS, Tadeusz Litak et al., Do, 18:00 - 20:00, Raum n.V.; ab 18.10.2013; Seminarraum LS INF8, Martensstr. 3, 11. OG; Vorbesprechung: 18.10.2013, 14:00 - 16:00 Uhr)

Inhalt:

As the name indicates, we will spend the semester reading papers on Curry-Howard correspondence, type systems and type theories. This should be of particular interest to students who completed the SemProg course or are otherwise familiar with proof assistants or dependent types. Students with knowledge of functional programming are also a natural audience.
We will learn what makes proof assistants work and what are superficial and deep differences between most famous ones like Coq and Agda. Depending on interests and competences of participants, we can also focus more on issues like metaprogramming, code generation, GADTs, programming semantics and computational effects.

Lernziele und Kompetenzen:

Wissen

The papers we are going to study will allow students to recognize and explain key features and differences between respective theoretical underpinnings of proof assistants like Coq or Agda.

Verstehen

The students will be able to explain why these systems (e.g., calculus of constructions, Martin-Löf type theory) are normalizing/terminating, compare the benefits and disadvantages of adding new constructs and give examples of safe and unsafe extensions of corresponding systems.

Weitere Informationen:

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 | Bachelorprüfung | Bachelor-Module Informatik | Seminar)
2. Informatik (Bachelor of Arts (2 Fächer))
   (Po-Vers. 2013 | Bachelorprüfung | Bachelor-Module Informatik | Seminar)
3. Informatik (Bachelor of Science)
   (Po-Vers. 2007 | Seminar)
4. Informatik (Bachelor of Science): 3-5. Semester
   (Po-Vers. 2009s | Pflichtmodule | Seminar)
5. Informatik (Bachelor of Science): 3-5. Semester
   (Po-Vers. 2009w | Pflichtmodule | Seminar)
6. Informatik (Master of Science)
   (Po-Vers. 2010 | Seminar)

Studien-/Prüfungsleistungen:

Seminar Curry-Howard Korrespondenz (Prüfungsnummer: 803808)

Prüfungsleistung, mehrteilige Prüfung, 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.

Erstablegung: WS 2013/2014, 1. Wdh.: SS 2014

1. Prüfer:

Lutz Schröder