I started as a lecturer at Royal Holloway in August 2019. Prior to that I worked as a postdoctoral researcher in the PLAS group at the University of Kent and the PPLV group at University College London. Before that, I spent some time as a Teaching Fellow at Imperial College London, where I was responsible for teaching and admissions for the MSc in Computing Science. I have also worked in industry as a web developer.

See my personal web pages: https://www.cs.rhul.ac.uk/home/rrowe/

I obtained my BA in Computer Science from the University of Cambridge Computer Lab in 2004. I was a member of Fitzwilliam College. I was awarded my MSc (Distinction) in Advanecd Computing in 2008 and my PhD in 2013, both from Imperial College London.

My research interests centre around formal program verification and Proof Theory. 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.

Trustworthy Refactoring

Whilst at the University of Kent, I worked on the Trustworthy Refactoring project (EPSRC Grant EP/N028759/1) with Simon Thompson, Scott Owens, and Hugo Férée. The aim was to build a refactoring tool for the OCaml programming language in which refactoring instances can be formally verified to be behaviour preserving. We developed a prototype tool called ROTOR, and an abstract static semantics for a subset of OCaml that formalises our approach.

Non-wellfounded/Cyclic Proof and Automated Verification

I work on aspects of proof theory, specifically a notion of proof in which we allow derivations of infinite height but with a well-formedness condition that guarantees soundness. This essentially encodes forms of inductive reasoning. A natural finite representation of infinite proofs is using finite derivation trees with cycles, hence the term "cyclic" proof. I have investigated the theory of non-wellfounded and cyclic proofs in different contexts, including first order logic, Herbrand logics, and modal logics.

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 described an encoding of the Factorisation Calculus into Lambda Calculus; I have also supervised an 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. (I really should move this over to Github, or similar!)