GPN12:Agda - Mit starken Typen abhängen: Unterschied zwischen den Versionen

aus dem Wiki des Entropia e.V., CCC Karlsruhe
Wechseln zu: Navigation, Suche
(Die Seite wurde neu angelegt: „{{#css:GPN12:Stylesheet}} Vortrag von nomeata auf der GPN12. <blockquote> Agda: is it a dependently-typed programming language? Is it a proof-assistant b…“)
 
(Post-Vortrags-Upload)
Zeile 16: Zeile 16:
 
  play n _ _ | n <= 0 = []
 
  play n _ _ | n <= 0 = []
 
  play n p1 p2 = let k = p1 n in n : play (n - k) p2 p1
 
  play n p1 p2 = let k = p1 n in n : play (n - k) p2 p1
 +
 +
Mehr Infos zum Vortrag:
 +
* [[Media:AgdaTalk.pdf|Transskript]] (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://git.nomeata.de/?p=darcs-mirror-gpn12-agda-talk.git;a=summary Git-Mirror] obiges Repository.
  
 
Mehr Informationen zu Agda:
 
Mehr Informationen zu Agda:
 
* Die [http://wiki.portal.chalmers.se/agda/pmwiki.php offizielle Homepage]
 
* Die [http://wiki.portal.chalmers.se/agda/pmwiki.php offizielle Homepage]
 +
* [http://stackoverflow.com/questions/10931316/real-programs-written-in-agda Gibt es echte Programme in Agda?]
  
 
[[Kategorie:GPN12]]
 
[[Kategorie:GPN12]]
 
[[Kategorie:Vorträge]]
 
[[Kategorie:Vorträge]]
 
{{Navigationsleiste GPN12}}
 
{{Navigationsleiste GPN12}}

Version vom 7. Juni 2012, 23:51 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:

Mehr Informationen zu Agda: