GPN12:Agda - Mit starken Typen abhängen: Unterschied zwischen den Versionen
(Post-Vortrags-Upload) |
Keine Bearbeitungszusammenfassung |
||
Zeile 19: | Zeile 19: | ||
Mehr Infos zum Vortrag: | Mehr Infos zum Vortrag: | ||
* [[Media:AgdaTalk.pdf|Transskript]] (PDF-Datei) | * [[Media:AgdaTalk.pdf|Transskript]] (PDF-Datei) | ||
* [http://darcs.nomeata.de/gpn12-agda-talk/AgdaTalk-Slides.svg Die Folien der Einführung] (interaktives SVG, erstellt mit [http://sozi.baierouge.fr/wiki/en:welcome Sozi]) | |||
* [[Media:AgdaTalk-Slides.pdf|Die Folien der Einführung]] (PDF-Datei) | * [[Media:AgdaTalk-Slides.pdf|Die Folien der Einführung]] (PDF-Datei) | ||
* [http://darcs.nomeata.de/gpn12-agda-talk/ Darcs-Repository] mit den Quellen von Programm, Vortragstext und Präsentation | * [http://darcs.nomeata.de/gpn12-agda-talk/ Darcs-Repository] mit den Quellen von Programm, Vortragstext und Präsentation |
Version vom 8. Juni 2012, 10:33 Uhr
Vortrag von nomeata auf der GPN12.
Agda: is it a dependently-typed programming language? Is it a proof-assistant based on intuitionistic type theory? ¯\(°_0)/¯ Dunno, lol.
Programmiersprachen gibt es wie Sand am Meer; wir wollen hier an Stränden sandeln die etwas weiter weg der üblichen touristischen Hochburgen wie C, Java oder PHP sind. Genau gesagt geht es um Agda, was gleichzeitig eine funktionale Programmiersprache (wie Haskell) und ein Theorembeweiser (wie Coq) ist. Der Vortrag ist kein Tutorial, sondern eine Demonstration: nomeata wird einfach den Editor starten und ein kleines Problem live bearbeiten. Dabei wird man sehen wie man mit einem abhängigen Typsystem sich Datentypen definiert, die exakt das darstellen, was man braucht, und wie man damit Ausnahmebehandlungen ersetzt und wie man in Agda selbst die Korrektheit des Programms beweist.
Die Syntax von Agda ist sehr ähnlich der von Haskell und wird nicht besonders ausführlich erklärt. Es ist also nützlich, schon mal Haskell-Code gesehen zu haben. Wer versteht (oder erahnen kann) was dieser Code macht sollte keine Schwierigkeiten haben:
play :: Int -> (Int -> Int) -> (Int -> Int) -> [Int] play n _ _ | n <= 0 = [] play n p1 p2 = let k = p1 n in n : play (n - k) p2 p1
Mehr Infos zum Vortrag:
- Transskript (PDF-Datei)
- Die Folien der Einführung (interaktives SVG, erstellt mit Sozi)
- Die Folien der Einführung (PDF-Datei)
- Darcs-Repository mit den Quellen von Programm, Vortragstext und Präsentation
- Git-Mirror obiges Repository.
Mehr Informationen zu Agda: