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