Nach positiver Absolvierung der Lehrveranstaltung sind Studierende in der Lage neue Methoden der Typentheorie und der Beweistheorie zu erlernen und selbständig zu gebrauchen. Insbesondere können die Studierenden den Bezug zwischen computationaler Logik und funktionaler Programmierung herstellen.
Intuitionistische Logik, typisierter Lambda-Kalkül, Curry-Howard Isomorphismus, Arithmetik erster Stufe, System T, Logik zweiter Stufe, System F.
Selbstständige Erarbeitung von Kapiteln durch die Studierenden, Erarbeitung eines Vortrages gemeinsam mit dem Leiter der Lehrveranstaltung. Diskussion der Inhalte in der Gruppe.
Die Lehrveranstaltung basiert auf Sørensen, Urzyczyn: "Lectures on the Curry-Howard Isomorphism" (2006), das aus dem TU Netzwerk via https://www.sciencedirect.com/bookseries/studies-in-logic-and-the-foundations-of-mathematics/vol/149/suppl/C heruntergeladen werden kann.
Der Leistungsnachweis erfolgt durch die Abhaltung eines Vortrages im Seminar und durch die Mitarbeit.
Nicht erforderlich
Gute Kenntnisse in Mathematischer Logik.
