[Agda] Seeking Pointers for an Introductory Presentation

[Joachim Breitner]

Hi,

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
https://entropia.de/wiki/images/c/cf/AgdaTalk.pdf
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:
http://stackoverflow.com/questions/10931316/real-programs-written-in-agda

Greetings,
Joachim

-- 
Dipl.-Math. Dipl.-Inform. Joachim Breitner
Wissenschaftlicher Mitarbeiter
http://pp.info.uni-karlsruhe.de/~breitner
-------------- 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