Aktuelles
Vortrag und Hands-On im Rahmen von Haskell in Leipzig 5
Dependent Types mit Agda
Vortragender: Wolfgang Jeltsch
am 04.06.2010, 15:45 Uhr (Vortrag) und 17.00 Uhr (Hands-On) auf dem Leipziger Mediencampus
Mit abhängigen Typen (dependent types) können nicht nur Typen, sondern auch Werte als Parameter von Typen fungieren. Dadurch kann man z.B. die Längen von Listen in deren Typen angeben. Damit wird es möglich, fehlerhafte Indizierungen zur Compilierzeit statt zur Laufzeit zu erkennen.
Die Möglichkeiten reichen aber noch viel weiter. Eine Programmiersprache mit abhängigen Typen ist nämlich automatisch eine Beweissprache für eine Prädikatenlogik. Daher kann man nahezu beliebige Spezifikationen als Typen darstellen und deren Einhaltung vom Typprüfer sicher stellen lassen.
In dem Vortrag und dem anschließenden praktischen Teil werden folgende Themen behandelt:
- Grundlagen zu Dependent Types
- Grundlagen zu induktiven Familien (GADTs)
- die Grundidee des Curry-Howard-Isomorphismus
- ein kleiner Beweis in Agda
Folgende Beispiele werden gezeigt:
- statische Bereichsprüfung für Listenindizes
- take mit Bereichsprüfung für die Resultatlänge
27.09. bis 02.10.2010
40. Jahrestagung der Gesellschaft für Informatik, Leipzig


