Links und Funktionen
Sprachumschaltung

Navigationspfad
Sie sind hier: Startseite / Lehre / Bachelor- und Masterarbeiten / Projektbeschreibungen / Verifizierte Standardbibliothek für die funktionale Sprache Agda


Inhaltsbereich

Verifizierte Standardbibliothek für die funktionale Sprache Agda

Fortgeschrittenenpraktikum


Aufgabenstellung:

Agda ist eine neue, abhängig getypte Programmiersprache, vergleichbar mit Haskell. In Agda kann man nicht nur programmieren, sondern auch Programme als korrekt beweisen. Die nötigen Beweise werden dabei in derselben Sprache abgefasst wie die Programme.
Agda befindet sich noch in der heißen Phase der Entwicklung, die Standardbiliothek ist noch nicht vollständig. Im dem Projekt sollen Teile der Standardbiliothek entwickelt werden, z.B. eine Implementierung von Rot-Schwarz-Bäumen (balancierte Suchbäme). Dabei stellt die Implementierung nicht nur die Funktionalität zur Verfügung, sondern stellt auch sicher, dass die Invarianten (Balance, Sortierung) zu jedem Zeitpunkt erfüllt sind.

Referenzen:

Chris Okasaki, Red-black trees in a functional setting
Stefan Kahrs' Verbesserungen 

Kontakt:

Dr. Andreas Abel

Artikelaktionen


Funktionsleiste