© University of Kent - Contact | Feedback | Legal | FOI | Cookies
Reuben Rowe
Research Associate
|
|
|
Publications
My publications are available from the University of Kent's Academic Repository.
Please also see my dblp and Google Scholar entries.
Recent & Unpublished Work
-
Uniform Inductive Reasoning in Transitive Closure Logic via Infinite Descent.
Liron Cohen and Reuben N. S. Rowe. In Proceedings of CSL 2018.
extended version available on arXiv. -
Towards Large-scale Refactoring for OCaml.
Reuben N. S. Rowe and Simon J. Thompson. Submitted. -
A Functional Perspective on Machine Learning via Programmable Induction and Abduction.
Steven Cheung, Victor Darvariu, Dan R. Ghica, Koko Muroya, and Reuben N. S. Rowe. Accepted to FLOPS 2018.
OCaml extension for the abductive calculus: github.com/reubenrowe/ocaml-decml. -
ROTOR: First Steps Towards a Refactoring Tool for OCaml.
Reuben N. S. Rowe and Simon J. Thompson. Abstract of talk for the OCaml Workshop at ICFP 2017.
Docker image. -
Realizability in Cyclic Proof: Extracting Ordering Information for Infinite Descent.
Reuben N. S. Rowe and James Brotherston. In Proceedings of TABLEAUX 2017.
Technical report available on arXiv. -
Automatic Cyclic Termination Proofs for Recursive Procedures in Separation Logic.
Reuben N. S. Rowe and James Brotherston. In Proceedings of CPP 2017. -
Type Inference for Nakano's Modality.
This paper collects some of the results from my PhD thesis on guarded recursive types.
Talks
- Towards a Formal Theory of Renaming for OCaml. Theoretical Computer Science Seminar, University of Birmingham.
- Uniform Inductive Reasoning in Transitive Closure Logic via Infinite Descent.
- Transitive Closure Logic: Infinitary and Cyclic Proof Systems. PARIS 2018.
- Realizability in Cyclic Proof: Extracting Ordering Information for Infinite Descent. TABLEAUX 2017.
- ROTOR: First Steps Towards a Refactoring Tool for OCaml. OCaml Users Workshop 2017.
-
Automatic Cyclic Termination Proofs for Recursive Procedures in Separation Logic.
- slides presented at CPP 2017 conference.
- slides presented at TAPAS 2016 workshop.
- Program Verification Using Cyclic Proof. Programming Research Group Seminar, Cambridge, May 2016.
- Model Checking for Symbolic-Heap Separation Logic with Inductive Predicates. POPL'16, January 2016
- Verifying Heap-manipulating Recursive Procedures Using Cyclic Proof. Resource Reasoning Research Meeting, April 2015.
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.