← Fun in Oxford, November 2006 Fun in Cambridge, May 2007 →

At all costs, modesty

Our second meeting was held on Wednesday 21 February 2007, in various locations on the Jubilee Campus of the University of Nottingham. Despite some minor technical problems with a narcoleptic projector, we fed our heads acceptably, I think. A swift one or two in the Three Wheatsheaves, a curry at Taste of India, then next door to the Johnson Arms: Fun continues to be a valuable social occasion, as well as (despite?) its academic status. It seems that the substantial attendance at the inaugural meeting was not, after all, beginner's luck. Thank you all for coming!

Dinner

As promised, here's the receipt for dinner. Curry, as it happens, in the Taste of India, Abbey Street.

Graham and Conor Said

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!

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 here.

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.

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.

Schedule

12.00 - 14.00 Lunch (bring your own)
14.00 - 15.00 Matching Regular Expressions, Revisited, Revisited
James McKinna, University of St Andrews
James's slides
15.00 - 15.30 Coffee
15.30 - 16.00 Generic and Indexed Programming
Jeremy Gibbons, University of Oxford
Jeremy's slides
16.00 - 16.30 A Well-Typed Interpreter for a Dependently Typed Language
Nils Anders Danielsson, Chalmers University of Technology
Nisse's slides
16.30 - 17.00 Making Haskell even better for DSELs
Lennart Augustsson, Credit Suisse
Lennart's slides are unavailable (pat. pending)
17.00 - 19.00 Pub
19.00 - Dinner

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.

  • Making Haskell even better for DSELs
    Lennart Augustsson, Credit Suisse