Lambda Calculus

Worum geht's

Du lernst die Grundlagen des Lambda-Kalküls als Modell von Programmiersprachen. Zunächst behandelst Du ungetypten Lambda-Kalkül, seine Reduktionsregeln, Evaluationsstrategien (z. B. call-by-value, call-by-name) und seine Turing-Vollständigkeit. Im zweiten Teil lernst Du getypte Lambda-Kalküle, gängige Typensysteme in funktionalen Sprachen und die Verbindung zwischen Typen und Logik (Curry–Howard). Am Ende kannst Du Lambda-Terme nutzen, übersetzen und ihre Eigenschaften beweisen.

Was du danach kannst

• fundamentale Eigenschaften der Reduktion im Lambda-Kalkül beweisen
• übliche Datentypen und Kontrollstrukturen im Lambda-Kalkül modellieren
• Lambda-Terme und Kombinatoren ineinander übersetzen
• einen principal type für ungetypte Terme ableiten
• Übersetzung zwischen Lambda-Termen und Beweisen (Curry–Howard) durchführen

Aus was das Modul besteht

• VorlesungVermittlung des Lehrstoffs durch Dozent/in in Interaktion mit den Studierenden
• Übung/TutorialBearbeitung von Aufgaben einzeln oder in Kleingruppen mit Tutor-Unterstützung; Aufgaben können computerbasiert oder schriftlich sein

Lehrmethode

• Vortrag / dialogische VorlesungPräsentation des Materials und Austausch mit den Studierenden
• Tutorials mit AufgabenVertiefung des Stoffes durch Übungsaufgaben, praktische Anwendung und Tutorhilfe