Funktionale Programmierung und Typtheorie

Technische Universität Dresden Institut für Theoretische Informatik Lehrstuhl für Automatentheorie

Information zur Lehrveranstaltung
(Bachelor Informatik (INF-B-510, INF-B-520), Master Informatik, Diplom Informatik (INF-BAS6, INF-VERT6))

Die Lehrveranstaltung thematisiert die semantischen Grundkonzepte getypter funktionaler Programmiersprachen (z.B. Haskell). Das sind: der Lambda-Kalkül als Programmiersprache, der getypte Lambda-Kalkül (nach Church und Curry), der polymorphe Lambda-Kalkül zweiter Ordnung, der polymorphe Lambda-Kalkül dritter Ordnung, der Lambda-Würfel, polymorphe Datentypen und Funktionen, Typsysteme und Typklassen, verzögerte Auswertung, funktionale Parser, Verifikation und Programmtransformation sowie Monaden.

Informationen zum Beginn der Lehrveranstaltung im SS 2015 am 13.04.2015 APB/E010

Die Lehrveranstaltung beginnt mit der ersten Lehrveranstaltungswoche. Die erste Vorlesung findet am Montag, den 13.04.2015 in der 3. DS, (APB/E010) statt. Zu den Modalitäten des Übungsbetriebes (Freitags, 4.DS, APB/E007) wird in der ersten Lehrveranstaltung informiert.

Es besteht die Möglichkeit, inhaltliche und organisatorische Fragen zur Lehrveranstaltung innerhalb einer Mailingliste zu diskutieren.

Lehrmaterial

Vorlesungsunterlagen werden an dieser Stelle aktuell zur Verfügung gestellt.

• Vorlesung Kapitel 1, Folien (pdf)
• Vorlesung Kapitel 2 (Teil 1), Folien (pdf)
• Vorlesung Kapitel 2 (Teil 2), Folien (pdf) (Version 10.05.2015)
• Vorlesung Kapitel 2 (Teil 3), Folien (pdf) (Version 01.06.2015)
• Vorlesung Kapitel 3, Folien (pdf)
• Vorlesung Kapitel 4, Folien (pdf)
• Vorlesung Kapitel 5, Folien (pdf)
• Vorlesung Kapitel 6, Folien (pdf)
• Vorlesung Kapitel 7, Folien (pdf) (Version 13.07.2015)

Übungsaufgaben

Übungsaufgaben sind im Vorfeld der jeweiligen Übung auf dieser Seite zu finden und selbständig auszuarbeiten. In den Übungen erfolgt die Diskussion der studentischen Lösungen. Die erste Übung findet am 24.04.2015, 4.DS im Raum E007 statt.

1. Übungsblatt (24.04.2015, 08.05.2015)
2. Übungsblatt (08.05.2015, 15.05.2015)
3. Übungsblatt (22.05.2015)
4. Übungsblatt (05.06.2015) Übung findet im Raum E042 statt!
5. Übungsblatt (12.06.2015) Übung findet im Raum E042 statt!
6. Übungsblatt (19.06.2015) Übung findet im Raum E042 statt!
7. Übungsblatt (26.06.2015, 03.07.2015)
8. Übungsblatt (10.07.2015)
9. Übungsblatt (17.07.2015, 24.07.2015)

Zusätzliche Literatur

Die hier empfohlene zusätzliche Literatur kann über den WebOPAC der SLUB gefunden werden.

• H. P. Barendregt, The Lambda Calculus - Its Syntax and Semantics, Studies in logics and the foundations of mathematics, Vol. 103, Elsevier Science Publishers B.V., 1985
• H. P. Barendregt, Lambda Calculi with Types, in: S. Abramsky, Dov. M. Gabbay, T. S. E. Maibaum, Handbook of Logic in Computer Science, Vol. 2: Background - Computational Structures, 1992
• Anthony J. Field, Peter G. Harrison, Functional Programming, Addison-Wesley, 1988
• Paul Hudak, Conception, Evolution, and Application of Functional Programming Languages, ACM Computing Surveys, Vol. 21, No. 3, September 1989
• Peter Thiemann, Grundlagen der funktionalen Programmierung, B. G. Teubner, 1994
• Simon Thompson, Haskell - The Craft of Functional Programming, Addison-Wesley, 1999
• Peter Pepper, Funktionale Programmierung in OPAL, ML, HASKELL und GOFER, Springer, 1999
• Chris Reade: Elements of Functional Programming, Addison-Wesley, 1989
• M. Gordon, Programming Language - Theory and its Implementation, Prentice Hall, 1988