Aktuelles

Unsere fleißigen Tutoren im Sommersemester 2010 Sascha, Benny, Peter, Dominik und Bianca.

 
 

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

3. Workshop "Deklarative Modellierung und effiziente Optimierung - dank Constraint-Technologie (MOC 2010)"

40. Jahrestagung der Gesellschaft für Informatik, Leipzig

 

14. -16. September 2010

WLP 2010

24th Workshop on Constraint Logic Programming
Cairo

Mitarbeit

an aktuellen Forschungsprojekten möglich. Themenvorschläge für Studien-, Diplom-, Bachelor- und Masterarbeiten hier. 

Vorschau Wintersemester 2010/11

Im Wintersemester 2010/11 bieten wir folgende Lehrveranstaltungen an:

12-3-49 :
Moderne Funktionale Programmierung
12-4-72 :
Einführung in die Constraint-Programmierung
12-1-02 :
Programmierpraktikum
12-1-11 :
Proseminar "Maschinelles Lernen"
12-4-61 :
Seminar "Formale Methoden der Software-Sicherheit"