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. (Stand 06.07.2012)
Mehr Informationen zu Agda:
Fahrplan ·
3D Printing - code, drucken, nerfgun · Agda - Mit starken Typen abhängen · Angriffe auf Wireless Local Area Networks · Arduino Selbsthilfegruppe · BubbleTea selber bauen · CMS4Nerds - Vermitteln von informationeller Selbstbestimmung im Alltag · Crash Course Lua · Crunchman's Memoirs · Die D Sprache für C++ Entwickler · Die neuen politischen Proteste und ihre Vernetzung · Die Werwölfe von Düsterwald · Eigentum, Sex und die Cloud · Emacs Org-mode · Evolution im täglichen Leben und warum "Intelligent Design" auf den Lehrplan gehört · Gamejam · Go – eine moderne Programmiersprache · Gulaschbytes · Häkeln · Hardware Design Patterns · Heterosexismus hacken · Homeautomationsplausch · HTML5 Security · Info Beamer Hacking · Informatik in der Schule · Introduction to Vorbis · Kinect-Touchpad · Klangsynthese und Live-Coding mit SuperCollider · Lightning Talks · Linux Networking - Ninja Style · Location Based Games - Spiele im Stadtraum · Lockpicking · Maintainern 101 · meillo's mail handler · Raumschiffe in Science und Fiction · Roboter in die Schule · Segelfliegen auch für Bastler · Steal This Talk · systemd · Tschunk-Workshop · Urban Hacking - Hacking the Public Space · What to hack · When biotech is outlawed, only outlaws will do biotech. · Wie man eine 64Kilobyte-Intro baut · Wunderwelt des SSH – mehr als nur Telnet mit Crypto · You are HERO - Questdesign im Real Life