Research

My current interests centre around formal program verification. I am currently investigating how to expand verification techniques making use of separation logic and cyclic proofs in the context of the Cyclist theorem proving framework. 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 (I am affiliated with the SLURP research group at Imperial College London); fundamental models of computation (Lambda Calculus, Term Rewriting Systems, Process Calculi); Curry-Howard Isomorphisms; Logics for Computer Science.

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 in particular.

Recent & Unpublished Work

• Automatic Cyclic Termination Proofs for Recursive Procedures in Separation Logic.
  Reuben N. S. Rowe and James Brotherston. Accepted to CPP 2017.
• Type Inference for Nakano's Modality.
  This paper collects some of the results from my PhD thesis on guarded recursive types.
• A Parsing Algorithm for Recursive Adaptive Grammars. Description and Java code on Sourceforge

Talks

• Automatic Cyclic Termination Proofs for Recursive Procedures in Separation Logic. TAPAS 2016
• Program Verification Using Cyclic Proof. Programming Research Group Seminar, Cambridge, May 2016.
• Verifying Heap-manipulating Recursive Procedures Using Cyclic Proof. (Slides)
  A talk given at the recent Resource Reasoning Research Meeting, April 2015.