[Haskell] ANNOUNCE: Fun in the Afternoon II

[Graham Hutton]

Dear all,

     *** FUN IN THE AFTERNOON, WED 21 FEB, NOTTINGHAM ***

The second Fun in the Afternoon will take place in Nottingham 
next week, on the afternoon of Wednesday 21st February.  This
time around, James McKinna will be giving an invited talk to
start the event off, and we'll then have three half-hour talks
by Jeremy Gibbons, Nils Anders Danielsson, and Lennart Augustsson.
We hope it will be as much fun as the first event in Oxford, but
for this to be the case we need as many people as possible to
come along and join in.  Please spread the word!

Background
----------

Fun in the Afternoon is a termly seminar on functional programming
and related topics.  The inaugural meeting was held in Oxford in
November last year, and was a great success, with four excellent
talks and a large number of participants from across the UK and 
further afield.  For more info, and to join the mailing list:

   http://sneezy.cs.nott.ac.uk/fun

Location
--------

The second Fun in the Afternoon will be held on the Jubilee Campus
of the University of Nottingham on Wednesday 21st February 2007.
Nottingham is centrally located in the UK, and is easily reachable
by all forms of transport.  Travel info and maps are available from:

   http://www.nottingham.ac.uk/cs/general/school_directions.php

Before the talks start at 2pm, you are welcome to bring your own
sandwiches and have lunch with us in the Atrium of the Computer
Science building (labelled 4 on the campus map available above).
There are two places to buy sandwiches on the campus, either from
the cafe on the top floor of the New Business School (labelled 7
on the campus map), or from The Exchange (labelled 2.)

The talks will take place in seminar room A32 of the Education
(not Computer Science) building on the Jubilee Campus, which is
the building labelled 6 on the map.  We will put up some signs
on the day to help make sure no-one gets lost.

We'll retire afterwards to a local pub for further discussion
and heated debate, and then to dinner for those interested.

Schedule
--------

12.00 - 14.00 : Lunch (bring your own)

14.00 - 15.00 : Matching Regular Expressions, Revisited, Revisited
                James McKinna, University of St Andrews

15.00 - 15.30 : Coffee

15.30 - 16.00 : Generic and Indexed Programming
                Jeremy Gibbons, University of Oxford

16.00 - 16.30 : A Well-Typed Interpreter for a Dependently Typed Language
                Nils Anders Danielsson, Chalmers University of Technology

16.30 - 17.00 : Lennart Augustsson, Credit Suisse
                Title to be announced

17.00 - 19.00 : Pub

19.00 -       : Dinner

Titles and abstracts
--------------------

Matching Regular Expressions, Revisited, Revisited 
James McKinna, University of St Andrews

We revisit regular expression matching, following Harper's 1999
JFP treatment, recently revisited by Yi, in the context of
dependently-typed functional programming.  The correctness of
matching is delegated to the (self-evident) correctness of the
rendering function, to which the recogniser provides an inverse.
The use of dependent types to organise the development permits us
to develop, in a uniform setting, the intricate mix of operations
on regular languages on the one hand, and on the other, their algebraic
theory, together with the constructions which relate the two.

Generic and Indexed Programming
Jeremy Gibbons, University of Oxford

The Generic and Indexed Programming project at Oxford started in  
November 2006, and is funded by EPSRC for three and a half years.
The "generic" bit is about programs parametrized by datatypes,
and builds on our work on the Datatype-Generic Programming project.
This talk is about the "indexed" bit, which concerns lightweight
techniques for dependently-typed programming, for example using
generalized algebraic datatypes.  Specifically, values are reflected
at the type level, and can then be used as "phantom type" indices
to other types, expressing certain kinds of constraints; the
relationship between type representations and values, important
in datatype-generic programming, is one application.  We will
explain our motivation, show some cool examples, and say a little
about where we see the project going.

A Well-Typed Interpreter for a Dependently Typed Language
Nils Anders Danielsson, Chalmers University of Technology

GADTs are often introduced with the "well-typed interpreter"
example.  A simple programming language is encoded as a GADT in
such a way that only well-typed terms can be defined, and then
an interpreter which cannot get stuck is implemented.  I'll show
how to do this for a dependently typed lambda calculus, in the
dependently typed meta-language AgdaLight.  To accomplish this
I'll use inductive-recursive families, a generalisation of GADTs.

Lennart Augustsson, Credit Suisse
Title/abstract to be announced

We look forward to seeing you in Nottingham next week!  If you
are planning to come, it would be useful if you can drop us a
line and also say if you are likely to come for dinner, in order
that we can estimate numbers for coffee and dinner.

Best wishes,

Graham and Conor

+---------------------------------------------------------------------+
| Dr Graham Hutton                     Email : gmh at cs.nott.ac.uk      |
| School of Computer Science and IT                                   |
| University of Nottingham             Web   : www.cs.nott.ac.uk/~gmh |
| Jubilee Campus, Wollaton Road                                       |
| Nottingham NG8 1BB, UK               Phone : +44 (0)115 951 4220    |
+---------------------------------------------------------------------+

This message has been checked for viruses but the contents of an attachment
may still contain software viruses, which could damage your computer system:
you are advised to perform your own checks. Email communications with the
University of Nottingham may be monitored as permitted by UK legislation.