I'm a third 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.
∃ Compilation à la Carte {code} (submitted to ICFP '13)
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 à 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 compilers.
∃ PhD Transfer Report: The Modular Compilation of Effects (UoN '11)
In this report I present the preliminary results of my research into the code generation stage of the modular compilation of programming languages according to the effects which they support. To this end, I demonstrate an elegant combination of previously developed techniques from the literature to decouple the recursive and syntactic aspects of a source language, and develop a semantics, compiler and virtual machine for such a language which is parameterised over its syntax and the monads which support effectful operations. All prerequisite knowledge to engage with the research material is presented in a background section within the opening chapters of this report. In addition, I present a detailed review of the existing literature concerning compiler modularity and the characterisation of effects, and lay out a preliminary draft for the structure of the thesis which this research aims towards.
∃ Towards Modular Compilers for Effects {code} (LNCS '11)
[awarded Best Student Paper: TFP'11]
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 and so forth. 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.
Spring Semester
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]
Autumn Semester
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]
After being born in Cambridge, England back in the Eighties, I left the UK at the age of seven for Johannesburg, South Africa. There, I (amongst other things!) completed my seven-subject IEB Matric at St Peter's College shortly before returning to Blighty. After a brief teaching stint at St Faith's, Cambridge in the Information Technology department, I began reading for a joint honours mathematics degree at Nottingham, where I graduated as the top student of the School of Computer Science in 2010, taking a Double First.
During my final undergraduate year, I founded CompSoc - the University's official Computer Science society: I consider this ragtag group of bandits my proudest university-related achievement. On the topic of university life, during the 2010-11 academic year I was a resident tutor at Sherwood Hall on University Park, where I spent a lot of time shouting at people at three in the morning. Furthermore, I was the Vice-President of the University of Nottingham Association for Resident Tutors (UNART), the political quasi-union representing tutor interests.
Orthogonally to my doctoral studies, I am an active member of British Mensa and a qualified teacher for English as a foreign language. How these things are relevant to my career is an exercise for the interested reader. I've recently become interested in playing chess and can be found at chess.com, however I'm appallingly bad at it, with an Elo rating of 799 (Glicko RD 28) as of 28th March 2013. Oh, and my Erdös number is five.
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