School of Computing

Simon Thompson

Emeritus Professor of Logic and Computation

Photo of SJ Thompson, if available
  • Room --
    School of Computing
    University of Kent,
    CT2 7NF
Wrangler OCaml Rotor Marlowe
Wrangler: a refactoring tool for Erlang. It is extensible and scriptable, and helps detect clones. Rotor is a refactoring tool for OCaml, described in these slides. PLDI 2019 paper here. Marlowe is a DSL for financial contracts on blockchain, described in this paper. I am very grateful to IOHK for their support of this work.
Haskell craft 3e TTFP book cover Erlang Master classes
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.

Research interests


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 worked for a number of years on building refactoring tools for functional programs in Erlang (Wrangler) and Haskell (HaRe). Recently, I've been working with Scott Owens, Reuben Rowe, Hugo Férée, Steven Varoumas and Joe Harrison on the ROTOR tool for OCaml. This work has been supported by the EU and EPSRC.

From October 2020 I'll be working on the STARDUST project with Laura Bocchi at Kent, and colleagues at the University of Glasgow and Imperial College. In STARDUST we'll be investigating how to put together session types with fault tolerance – i.e. with programs that can fail – to build more robust distributed systems. We'll be focussing initially on Erlang, working with a group of industrial partners.

I'm also looking at DSLs running on blockchain, and have designed the Marlowe DSL for financial contracts on Cardano, supported by IOHK, and working with Pablo Lamela and at team at IOHK.

I have publications forthcoming at ISoLA, 2020, and the OCaml Workshop 2020.

Links

Some recent presentations and talks

Projects


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 EPSRC project is to establish the feasibility of building trustworthy refactoring tools that guarantee that behaviour is not changed.

The project has built ROTOR https://trustworthy-refactoring.gitlab.io/refactorer/, a tool for refactoring large, multi-file OCaml codebases, written in OCaml. Currently, ROTOR can perform renaming of top-level value bindings within modules, and also carry out a fine-grained module dependency analysis of an OCaml codebase.

In buiulding ROTOR we developed a novel analysis and framework for analysing the way that name binding works in the OCaml module system. Properties of the anaysis are proved correct using Coq, and this analysis underlies our implementations in ROTOR. The work was published at PLDI 2019.

We are currently working on extending the range of refactorings, on API upgrade, and on checking equivalence of programs to verify refactoring connrectness in practice.

In doing this work 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 worked with IOHK on scripting languages for distributed ledgers (paper). I have also had two Knowledge Transfer Partnerships with Erlang Solutions: the first on refactoring and components for Erlang, the second on using e-learning technologies in high-quality online training.

Books

Functional Programming in Education

I work to promote the use of functional programming in education. I was chair of the conference on Trends in Functional Programming in Education, 2017, and chair of 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 was book reviews editor for the Journal of Functional Programming for more than 20 years.

Teaching innovation

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."

Some older presentations and talks

Other research

Other research that I have been involved with recently includes work in refactoring, reasoning with diagrams, computer algebra, verification and constructive type theory:

Real life

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.

[Last updated 26 August 2020]

School of Computing, University of Kent, Canterbury, Kent, CT2 7NF

Enquiries: +44 (0)1227 824180 or contact us.

Last Updated: 21/09/2020