[Agda] Seeking Pointers for an Introductory Presentation

Joachim Breitner breitner at kit.edu
Fri Sep 21 11:31:29 CEST 2012


Am Freitag, den 21.09.2012, 15:27 +0800 schrieb Lyndon Maydwell:
> If anyone has any links to recommended introductory presentations,
> examples of use of Agda outside of academia, or tips in general, let
> me know!

recently, I held an Agda course to a non-academic audience. My approach
was a bit different: I did a live hacking session developing a game
simulator, taking the players as arguments and returning who wins.
During the talk I pointed out way in which the players could cheat (and
where a “normal” programming language would have to resort to runtime
checks) and enhanced the types to reflect that. Then I also implemented
a strategy where the first player will always win, and proved that
within Agda.

I did not expect anyone in the audience to be able to do anything in
Agda after the talk; my aim was to show them _why_ they might want to
learn how to, though.

If you happen to know German (or fine with just reading the code), you
can browse through
and the code is at http://darcs.nomeata.de/gpn12-agda-talk/

I also wanted to point out “real world” uses of Agda, but I could not
find any:


Dipl.-Math. Dipl.-Inform. Joachim Breitner
Wissenschaftlicher Mitarbeiter
-------------- next part --------------
A non-text attachment was scrubbed...
Name: not available
Type: application/pgp-signature
Size: 198 bytes
Desc: This is a digitally signed message part
Url : http://lists.chalmers.se/pipermail/agda/attachments/20120921/0da386d6/attachment.bin

More information about the Agda mailing list