[Agda] Seeking Pointers for an Introductory Presentation

Lyndon Maydwell maydwell at gmail.com
Fri Sep 21 09:27:07 CEST 2012

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

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

More information about the Agda mailing list