[Agda] Seeking Pointers for an Introductory Presentation

[Andreas Abel]

Looks like a very nice talk! --Andreas

On 21.09.2012 11:31, Joachim Breitner wrote:
> 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
>
>
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>


-- 
Andreas Abel  <><      Du bist der geliebte Mensch.

Theoretical Computer Science, University of Munich
Oettingenstr. 67, D-80538 Munich, GERMANY

andreas.abel at ifi.lmu.de
http://www2.tcs.ifi.lmu.de/~abel/