Typ-basiertes Programmieren und Schließen in Funktionalen Sprachen, Wintersemester 2009/10

Jun.-Prof. Dr. Janis Voigtländer / Dipl.-Math. Daniel Seidel

Einträge im Vorlesungsverzeichnis:

Inhaltliche Zusammenfassung:

Stark getypte Programmiersprachen spielen eine zunehmend wichtige Rolle in der Praxis, unter Anderem da Typen schon bei der Konstruktion von Programmen bestimmte Arten von Fehlern ausschließen können. Typen dienen der Dokumentation und partiellen Spezifikation von Funktionalität und ermöglichen die sichere Wiederverwendung von Programmkomponenten. Darüber hinaus können mittels eines hinreichend ausdrucksstarken Typsystems Aussagen zum Programmverhalten jenseits der bloßen Passfähigkeit von Daten getroffen werden.

Ziel der Vorlesung ist es, solche Techniken an Hand der funktionalen Sprache Haskell zu beleuchten. Es wird darum gehen, geeignete Abstraktionsmechanismen (die mittlerweile auch Eingang in Mainstream-Sprachen wie Java finden) vorzustellen, teilweise formal zu untersuchen und auf konkrete Problemstellungen anzuwenden. Beispielanwendungen werden automatische Programmtransformationen sowie Korrektheitsbeweise für Algorithmen sein.

Voraussetzung:

Organisation:

Folien:

Übungsblätter:

"Skript":

Referenzen:

Online-Ressourcen:

Zuletzt geändert: Februar 2010, Janis Voigtlaender.