School of Computing

Reuben Rowe

Honorary Researcher

Photo of Reuben Rowe, if available
  • Room --
    School of Computing
    University of Kent,
    CT2 7NF


My publications are available from the University of Kent's Academic Repository.

Please also see my dblp and Google Scholar entries.

Recent & Unpublished Work


Research Interests

I belong to the following research groups:

My research interests centre around formal program verification. I am also interested in type systems and type-based analysis in general, with particular emphasis on intersection types and guarded recursive types. My wider research interests also include: programming languages and language design; fundamental models of computation (Lambda Calculus, Term Rewriting Systems, Process Calculi); Curry-Howard Isomorphisms; Logics for Computer Science. I am affiliated with the SLURP research group at Imperial College London (warning, website very out of date!), and the PPLV research group at UCL.

Trustworthy Refactoring

I am currently working on the Trustworthy Refactoring project (EPSRC Grant EP/N028759/1) with Simon Thompson, Scott Owens, and Hugo Férée. The aim is to build a refactoring tool for the OCaml programming language in which refactoring instances can be formally verified to be behaviour preserving. For this, we will be making use of the CakeML project, which is a formalisation of a subset of OCaml in the HOL theorem prover.

Automated Verification using Cyclic Proof

I worked with James Brotherston at University College London on investigating how to expand verification techniques making use of separation logic and cyclic proofs. This project (funded by EPSRC Grant EP/K040049/1) focussed on the development of the Cyclist theorem proving framework. My work in particular added capabilities for proving termination of procedural code with recursion.

Other Projects

I like thinking about the Factorisation Calculus, which is a combinatory rewrite system that has the capability to analyse the syntactic structure of a wide class of its own terms. This makes it a good candidate for a fundamental model in which to study issues like intensional computation, reflection, and meta-programming. I have published a paper describing an encoding of the Factorisation Calculus into Lambda Calculus; I have also supervised Alexander Bates' MEng dissertation, where we looked at a structural type system for the Factorisation Calculus.

An older research interest, which has been on the back burner for a while, is in frameworks for extensible programming languages, and recursive adaptive grammars (RAGs) in particular. I have written a RAG-based parser in Java which is hosted on Sourceforge.

About Me

I have been at Kent since December 2016. Prior to that, from May 2014 I was a postdoctoral research associate in the PPLV group at UCL. Before that, I worked as a Teaching Fellow in the Department of Computing at Imperial College London, where I was responsible for teaching and admissions for the MSc in Computing Science.

I completed my PhD at Imperial College in 2012 under the supervision of Dr Steffen van Bakel, on the topic of semantic types for class-based objects.

I was awarded an MSc in Advanced Computing with Distinction by Imperial College in 2008.

I gained my BA degree in 2004 from Fitzwilliam College Cambridge, where I studied the Computer Science Tripos as a member of the Computer Laboratory.

I have also spent time in industry as a web applications developer, some of it at Hyperspheric Solutions.

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

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

Last Updated: 20/10/2020