[Agda] Seeking Pointers for an Introductory Presentation

[Andreas Abel]

I have collected my Agda teaching material at

   http://www2.tcs.ifi.lmu.de/~abel/projects.html

Cheers,
Andreas

On 21.09.2012 09:27, Lyndon Maydwell wrote:
> Hi Agda-List.
>
>
> I've volunteered to give a talk about Agda to the Perth Functional
> Programmers group in Perth in about a month's time.
>
> I was wondering if anyone had any pointers on what would be useful to
> include in an introductory presentation.
>
> The level of familiarity with these sorts of languages within the
> group is limited to Haskell use and a couple of people with strong
> knowledge of Refinement Types at the moment, so rather than delve into
> anything overly technical or baroque I'd like to cover what might make
> dependently-typed programming a useful skill to know, with examples in
> Agda.
>
> I've broken the talk down into the following sections so far:
>
> * Philosophy
> * Syntax / Emacs
> * Basic Types
> * Inductive Types
> * --- Break ---
> * Dependent Types
> * Types and Values :: Theorems and Proofs
> * Conclusion
> * --- Questions ---
>
> I'm feeling under-qualified at this point as I've been exploring the
> language slowly on my own time over the past year, but don't yet have
> much confidence in my own abilities - However, there are some smart
> people in PerthFP and if I can get some of them interested, then it
> will serve me well with respect to having people around locally to
> bounce ideas off ;-)
>
> I don't want to make Agda seem like something that it's not since that
> would only lead to unrealistic expectations, but I do want to show off
> the power of dependent types.
>
> If anyone has any links to recommended introductory presentations,
> examples of use of Agda outside of academia, or tips in general, let
> me know!
>
>
>   - Lyndon
> _______________________________________________
> 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/