Viele Programmierer führen nur ungern Beweise: Agda verwendet das Curry-Howard-Prinzip “Beweise sind Programme”, so dass es ausreicht ein typkorrektes Programm zu schreiben um zu zeigen, dass ein Programm seine Spezifikation erfüllt.
Agda ist eine funktionale Programmiersprache mit abhängigen Typen und gleichzeitig ein interaktives Beweissystem. Das mächtige Typsystem erlaubt, auch substanzielle Eigenschaften direkt ins Programm zu schreiben.
Nach einer Einführung in die funktionale Programmierung mit Typen und das Curry-Howard-Prinzip führen wir anhand von Beispielen die wichtigsten Features von Agda vor. Zum Abschluss beleuchten wir einige Anwendungen von Agda und geben Hinweise auf Informationsquellen zum Thema.
Eine Installationsanleitung für Agda befindet sich hier.
Peter Thiemann ist Professor für Informatik an der Universität Freiburg und leitet dort den Arbeitsbereich Programmiersprachen. Er ist einer der führenden Experten zur funktionalen Programmierung, der partiellen Auswertung, domänenspezifischen Sprachen und zahlreichen anderen Themen der Softwaretechnik. Seine aktuelle Forschung beschäftigt sich mit statischen und dynamischen Analysemethoden für JavaScript.
