• Contact
• Maps
• Departments

• School of Computing home
• Undergraduate degrees
• Master's degrees
• PhD and research degrees
• Research
• Placements
• Kent IT Consultancy
• Makerspace
• Working with us
• About us
• News
• People
• Contact us

For current students & staff

• Information for students
• Systems support
• Information for staff

Search

School of Computing

Reuben Rowe

Honorary Researcher

workTel:     -- Email: R.N.S.Rowe@kent.ac.uk

Room -- School of Computing University of Kent, School of Computing, University of Kent Canterbury Kent CT2 7NF England

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

• A Non-wellfounded, Labelled Proof System for Propositional Dynamic Logic.
  Simon Docherty and Reuben N. S. Rowe. In Proceedings of TABLEAUX 2019 (to appear).
• Towards Automated Reasoning in Herbrand Structures.
  Liron Cohen, Reuben N. S. Rowe, Yoni Zohar. In the Journal of Logic and Computation, 2019 (to appear).
• Characterising Renaming within OCaml's Module System: Theory and Implementation.
  Reuben N. S. Rowe, Hugo Férée, Simon J. Thompson and Scott Owens. In Proceedings of PLDI 2019.
  Coq formalisation of the theory in the paper. Slides used in the presentation.
• ROTOR: A Tool for Renaming Values in OCaml's Module System. (Short tool presentation paper)
  Reuben N. S. Rowe, Hugo Férée, Simon J. Thompson and Scott Owens. In Proceedings of the International Workshop on Refactoring (IWOR) (to appear), part of ICSE 2019.
• 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. Unpublished manuscript.
• 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. In Proceedings of 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.
  • slides presented at SREPLS 10 workshop.
  • slides presented at CSL 2018 conference.
  • slides presented at Queen Mary Theory Seminary.
• 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:

• Programming Languages and Systems Group

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.