I’m a PhD student at the University of Birmingham, supervised by Paul Levy.
» more about me

I recently wrote a paper Iteration and labelled iteration with Paul.  Summary: When you naively add iteration to lambda calculus, nested loops with control are very inconvenient in the resulting language. The inconvenience is rather like trying to program with De Bruijn indices. We give an alternative syntax using second-order labels.
» paper html / pdf

My research is about improving functional programming, specifically tweaking algebraic operations and handlers. Intuitively, we know that we can “implement” all kinds of effects using handlers. But is this really true? Can we make it true?

If we handle get/set operations with runState, then we want to optimise e.g. get() + get() to 2 × get(). Unfortunately, this optimisation is invalid under lambdas, at least in most incarnations of effect&handler systems. This is because you can always install a new handler for get and then run your lambda under the new handler. It is very difficult to know what handler will be active at the time a lambda is activated.

So I play with a different effect&handler system. In my system, handlers bind operation names. So if you make (λx. get() + get()) directly under runState, then even if you install a new handler, the get will still always point to the runState. And so we know that  (λx. get() + get()) = (λx. 2 × get()).

My recent iteration paper helps set up the syntax for such a language with handlers of lexical operations.  » more about my research

I did my master’s thesis under Herman Geuvers about a continuation calculus with a code=data feel, which yielded 2 papers: paper 1, paper 2.