Fun in Birmingham, March 2011

← Fun in Glasgow, November 2010 Fun in Oxford, February 2012 →

Martin Says

Dear Fun fans,
I remind you that we are going to have a Fun meeting here in Birmingham, Wed 16 March, in the Afternoon. It promises to be very exciting. Here is an update:

  1. We have a few offers for contributed talks that we will confirm soon.
  2. Thorsten Altenkirch will talk about dependent types (he is making up his mind about two possible talks).
  3. Dan Ghica will talk about compilation of functional programs into hardware, and if we manage to set-up the equipment in the lecture theatre, he will give a demo using an FPGA.
  4. I will talk about exact real-number computation, using infinite lists of digits, including theory, programs in Haskell and demo.

But we need more talks! Please send proposals. If you would like to offer a talk, we probably have space in the programme (please specify the required time (e.g. 15, 30, 45 minutes)).

Please don't forget to let me know if you intend to attend. Thanks to those who have already told me.

Registration is not required. But please send me a message if you intend to come, so that we can organize various things.


University of Birmingham
Learning Centre, LG33


Wednesday 16 March. Arrival 1.45, talks start at 2.00.

How to get there

By train: you need to go to the station called "University". Believe it or not, it is the only station in the country called that. You probably go via New Street station, which is about 7min from this (usually stops at Five Ways first, and the next stop is University).

Once you are at University station, exit and turn left. You will see two red-brick, twin buildings opposite to each other, 1 minute walking, with a sculpture of Faraday (looking like he is going to be executed in an electric chair) between the buildings.

The building on the right is the Computer Science one. The building on the left is the Learning Centre, which is the one you want. It is called "R28 Learning Centre and Primary Care" on the Edgbaston map. The lecture theatre is in the Lower Ground floor, which means you have to go one floor down. There are stairs in the four corners of the building, and there is a lift (press buttons "-" and "1" to get to floor -1; the lift program was written in Haskell, and proved correct using denotational semantics, but hardware failures are not ruled out).

See also this link, where you can find directions for coming by car (probably not recommended).

We are looking forward to seeing you.


2.00Thorsten Altenkirch
3.00Philippa Cowderoy
3.15Coffee Break (Computer Science foyer)
3.40Dan Ghica
4.40Stretch your legs
4.45Martin Escardo
5.45Discussion and closing
6.00Pub followed by dinner


A Short History of Equality

Thorsten Altenkirch

University of Nottingham

Equality types are a unique feature of languages with dependent types (like Agda, Epigram or Coq's CIC). They are key to dissect inductive families (like Vec or Fin) and to understand dependently typed pattern matching. I will discuss some key issues with equality types: the question of extensionality (can we prove that two functions which are pointwise equal are equal ?) and the question of proof-irrelevance (are any two equality proofs equal ?). These issues have recently been reopened due to a proposal by Vladimir Voevodsky based on Homotopy Theory which gives a new answer to the question: when are two types equal?

Visibly Powerful Parsing

Philippa Cowderoy

Visibly Pushdown Languages are a relatively newly-discovered subset of Context-Free Languages with a wide range of useful properties. They also tie in neatly with a range of functional techniques and structures, offering a range of capabilities. I will sketch the case that there's room for yet another parsing library, that most of us want to use it for programming languages and that we may have a new flavour of applicative functor to play with.

Geometry of Synthesis:

Compiling higher order functions into hardware

Dan Ghica

University of Birmingham

Abramsky's Geometry of Interaction interpretation is a logical-directed way to reconcile the process and and functional views of computation, and can lead to a dataflow-style semantics of programming languages that is both operational (i.e. effective) and denotational (i.e. inductive on the language syntax). The key idea of the Geometry of Synthesis (GOS) approach is that for certain programming languages, namely Reynolds's affine version of Idealized Algol (called Syntactic Control of Interference--SCI) the processes interpreting the language can be given finitary representations, for both internal state and network tokens. A physical realisation of this representation becomes a semantics-directed compiler for SCI into hardware. In the talk I will (very) briefly visit the theoretical foundations of GOS, then describe the compiler with an emphasis on compilation of recursive functions. I will conclude with an analysis of several simple examples that indicate that the performance of the compiler is good enough to suggest this can be a practical method of higher-level circuit synthesis.

Computing with real numbers

represented as infinite sequences of digits

Martin Escardo

University of Birmingham

You are all familiar with the error problems that are inherent to computation with real numbers via floating-point notation. Most of you have heard that it is possible to avoid them using infinite sequences of digits with lazy evaluation. But fewer of you have seen how this actually works, what can be done, what can't be done, how fast, and so on. On the theoretical side, I will look at constructive mathematics, higher-type computability theory, and topology. But only very briefly, because I plan to spend most of my time showing you many functional algorithms and running them. At the beginning of the talk I will launch an infinite computation of pi, and we'll see how far it gets by the end of the talk. The presentation will be based on work by many people, Brouwer to begin with.