Skip to main content
BOB Konferenz 2018

Logo of BOB Konferenz 2018 BOB Konferenz 2018

23rd February 2018

Berlin, Germany

Part of the BOB series

Einführung in Agda

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.

This session is held on in Main Room

Speaker