Professor of Logic and Computation/ Director of Innovation
|Wrangler: a refactoring tool for Erlang, which is extensible and scriptable by users, and supports clone detection.||Third edition of Haskell: the Craft of Functional Programming||My first book, on Type Theory and Functional Programming gives an introduction to Martin-Löf type theory. PDF.||Erlang master classes with Joe Armstrong and Francesco Cesarini, part of a project to build MOOCs on Functional Erlang and Concurrent Erlang on FutureLearn.|
My main research interests are in functional programming, most recently in designing tools to help people to write and test programs more effectively. In particular, together with Huiqing Li I have been working on building refactoring tools for functional programs in Erlang and Haskell, supported by EU and EPSRC funding; I am also looking at refactoring other languages with my PhD students, as well as at Erlang and web services testing. I'm just about to start a new project: details next.
With Scott Owens, Hugo Férée and Reuben Rowe we're just about to start an EPSRC project on Trustworthy Refactoring.
Refactoring is the process of transforming program source code to improve it in some way, without changing what it does. Performing any refactoring in practice comes with the risk that it does indeed change program behaviour. The aim of this project is to establish the feasibility of building trustworthy refactoring tools that guarantee that behaviour is not changed.
Our approach in this project will provide different levels of assurance from the strongest case of a fully formal proof that a refactoring can be trusted to work on all programs, given some pre-conditions, to other, more generally applicable guarantees, that a refactoring applied to a particular program does not change the behaviour of that program.
In doing this we build on our expertise in building refactoring tools for Erlang and Haskell (Wrangler and HaRe), and in state of the art machine-supported verification. CakeML is a dialect of ML, designed to play a central role in trustworthy software systems. We will also work in collaboration with a leading industrial user of OCaml, Jane Street Capital.
I have also worked on three EU projects, each with links to Erlang. The Prowess project built on the success of ProTest, and extended property-based testing to rapidly-evolving systems such as web services and internet applications. Kent worked on extracting QuickCheck state machine models from tests, as well as refactorings to support building tests. The RELEASE project aimed to port Erlang to massively-multicore systems. Here we developed refactorings to support multicore programs in SD-Erlang, as well as building tools for offline and online monitoring, and a general extension API and scripting DSL for Wrangler.
I am also interested in working with industry, and have had two Knowledge Transfer Partnerships with Erlang Solutions: the first (now completed) on refactoring and components for Erlang, the second on using e-learning technologies in high-quality online training.
Some recent presentations and talks
Postgrad research students
I am currently working with six postgrad students.
- Pablo Lamela is working on extracting state machine models from tests, and other aspects of property-based testing for Erlang.
- Stephen Adams is working on data-oriented refactorings for Haskell, including the "monad to applicative" refactoring.
- Andreas Reuleaux is working on refactorings for dependently-typed languages, and in particular for PiForall.
- Sam Williams is running Erlang and BEAM on "bare metal", to support research on fault-tolerant operating systems.
- Joe Harrison is looking at extending static and dynamic tools to support checking communications in Erlang.
I am very keen to recruit research students to work with me on these topics, and particularly in
- refactoring functional and other languages, and
- program transformation in general;
- property-based testing and model extraction;
- functional software engineering in general, including tooling support.
The School's website has lots of stuff about becoming a postgrad student and some suggested projects in my and related areas of interest. Current students are working on refactoring Haskell and dependently-typed languages, implementing Erlang and property-based testing and modelling.
Functional Programming in Education
I work to promote the use of functional programming in education. I was chair of the conference on Functional and Declarative Programming in Education in 2005 (Tallin), 2002 (Pittsburgh) and 1999 (Paris). I have written texts on introductory functional programming in Haskell and Miranda as well as a problem solving approach for beginning functional programmers.
Journal of Functional Programming
I am book reviews editor for the Journal of Functional Programming. If you are interested in becoming a reviewer, please see books currently seeking reviewers and book review guidelines. At the University of Kent I play an active role in the Functional Programming Group.
I am an enthusiastic user of the ProfCast software for recording lectures in sync with their slide presentations. You can see examples at CO524, an introductory course on programming language technology. If you are trying these out, it's best to ignore the first; I was just getting used to the microphone on my PowerBook.
A student from the course says "I'm finding during revision that the recordings are immensely useful, if I come across a topic that isn't well explained in the slides or my notes it's great to be able to listen back to your explanations with the slides on screen and write new notes for revision purposes."
Other researchOther research that I have been involved with recently includes work in refactoring, reasoning with diagrams, computer algebra, verification and constructive type theory:
What do I do when I am not working? I enjoy cooking, cycling and jogging (I used to call it running). I rode the London 100 in 2016, with a ride time of 6:30. Most of all I enjoy walking, and, for example, have walked the Stevenson trail and in the Harz mountains.