## 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.