Erlernen abstrakter logischer Sprachen und Spezifikationen, sowie der Grundlagen funktionaler Sprachen, verstehen des Begriffs der Berechenbarkeit. Zusammenhang zwischen Algorithmen und Beweisen.

Syntax des Lambda-Kalk"uls, kombinatorische Logik, Lambda-Konversion, Reduktion, Normalform, Konfluenz, Termination, beta-Reduktion, eta-Reduktion, der Satz von Church-Rosser, Lambda-Theorien, Lambda-Definierbarkeit, Zahlensysteme, rekursive Funktionen, Unentscheidbarkeitsresultate. Typisierter Lambda-Kalkuel, Curry-Howard Isomorphismus.

Aufwandsabschaetzung

24 h: 12 Vorlesungseinheiten a 2 h

16 h: Loesen von 2 Uebungsblaettern a 7 Beispielen

4 h: tippen der Loesung in LaTeX

30 h: Vorbereitung auf abschliessende Pruefung

1 h: abschl. Pruefung

---------------------------------------------------

75 Std  = 3 ECTS