I'm a fourth-year research PhD student in the Functional Programming Laboratory of the School of Computer Science at the University of Nottingham, supervised by Professor Graham Hutton.
My current research concerns investigating the possibilities of using monads as an aid to constructing modular compilers within a functional framework, building upon previous work in the field on modular interpreters. I'm also interested in methods of proving program correctness, category theory, automated theorem proving within functional languages and computational complexity theory.
∃ Pick'n'Fix: Modular Control Structures (with Patrick Bahr)We present a modular framework for implementing languages with effects and control structures such as loops and conditionals. This framework enables modular definitions of both syntax and semantics as well as modular implementations of compilers and virtual machines. In order to compile control structures, in particular cyclic ones, we employ Oliveira and Cook's purely functional representation of graphs. Moreover, to separate control flow features semantically from other language features, we represent source languages using Johann and Ghani's encoding of generalised algebraic datatypes as fixpoints of higher-order functors. We demonstrate the usage of our modular compiler framework with two running examples and highlight the extensibility of our modular semantic definitions and compiler implementations.
∃ Compilation A La Carte (with Graham Hutton, IFL 2013)
In previous work, we proposed a new approach to the problem of implementing compilers in a modular manner, by combining earlier work on the development of modular interpreters using monad transformers with the a la carte approach to modular syntax. In this article, we refine and extend our existing framework in a number of directions. In particular, we show how generalised algebraic datatypes can be used to support a more modular approach to typing individual language features, we increase the expressive power of the framework by considering mutable state, variable binding, and the issue of noncommutative effects, and we show how the Zinc Abstract Machine can be adapted to provide a modular universal target machine for our modular interpreters.
∃ Programming Macro Tree Transducers (with Patrick Bahr, WGP 2013)
Tree transducers are tree automata defining functions from trees to trees. Put simply, a tree transducer is a set of mutually recursive functions transforming an input tree into an output tree. Macro tree transducers extend this recursion scheme by allowing each function to be defined in terms of an arbitrary number of accumulation parameters. In this paper, we show how macro tree transducers can be concisely represented in Haskell, and demonstrate the benefits of using such an approach with a number of examples. In particular, tree transducers afford a modular programming style as thy can be easily composed and manipulated. Our Haskell representation generalises the original definition of (macro) tree transducers, abolishing a restriction on finite state spaces. However, as we demonstrate, this generalisation does not affect compositionality.
∃ Towards Modular Compilers For Effects (with Graham Hutton, TFP 2011) [winner: Best Paper Award]
Compilers are traditionally factorised into a number of separate phases, such as parsing, type checking, code generation, etc. However, there is another potential factorisation that has received comparatively little attention: the treatment of separate language features, such as mutable state, input/output, exceptions, concurrency, etc. In this article we focus on the problem of modular compilation, where the aim is to develop compilers for separate language features and prove their correctness independently, which can then be combined as required. We summarise our progress so far, issues that have arisen, and further work.
G51FUN Functional Programming ['12-'13] ['11-'12] ['10-'11], ['09-'10]
G52AFP Advanced Functional Programming ['12-'13] ['11-'12] ['10-11]
G52MAL Machines and their Languages ['12-'13] ['11-'12] ['10-'11]
G51MCS Mathematics for Computer Scientists ['12-'13] ['11-'12] ['10-'11]
G51APS Algorithmic Problem Solving ['12-'13] ['11-'12]
G53CMP Compilers ['12-'13] ['11-'12]
IRL: Office A04, Functional Programming Laboratory, School of Computer Science, Jubilee Campus, Nottingham NG8 1BB
Facebook: Laurence E. Day (surprise!)
Email: led at cs dot nott dot ac dot uk
School of Computer Science, University of Nottingham
My Academia.edu page