[Agda] Seeking Pointers for an Introductory Presentation

[Lyndon Maydwell]

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