| 2026 | ITP | Certified Infinite Descent Criteria in Isabelle/HOL. | Jamie Wright, Liron Cohen, Reuben N. S. Rowe, Andrei Popescu |
| 2025 | TACAS | Cyclone: A Heterogeneous Tool for Verifying Infinite Descent. | Liron Cohen, Reuben N. S. Rowe, Matan Shaked |
| 2021 | CAV | Deductive Synthesis of Programs with Pointers: Techniques, Challenges, Opportunities - (Invited Paper). | Shachar Itzhaky, Hila Peleg, Nadia Polikarpova, Reuben N. S. Rowe, Ilya Sergey |
| 2021 | PLDI | Cyclic program synthesis. | Shachar Itzhaky, Hila Peleg, Nadia Polikarpova, Reuben N. S. Rowe, Ilya Sergey |
| 2020 | CADE | Integrating Induction and Coinduction via Closure Operators and Proof Cycles. | Liron Cohen, Reuben N. S. Rowe |
| 2019 | ICSE | Rotor: a tool for renaming values in OCaml's module system. | Reuben N. S. Rowe, Hugo Fre, Simon J. Thompson, Scott Owens |
| 2019 | PLDI | Characterising renaming within OCaml's module system: theory and implementation. | Reuben N. S. Rowe, Hugo Fre, Simon J. Thompson, Scott Owens |
| 2019 | TABLEAUX | A Non-wellfounded, Labelled Proof System for Propositional Dynamic Logic. | Simon Docherty, Reuben N. S. Rowe |
| 2018 | CSL | Uniform Inductive Reasoning in Transitive Closure Logic via Infinite Descent. | Liron Cohen, Reuben N. S. Rowe |
| 2018 | FLOPS | A Functional Perspective on Machine Learning via Programmable Induction and Abduction. | Steven Cheung, Victor Darvariu, Dan R. Ghica, Koko Muroya, Reuben N. S. Rowe |
| 2017 | CPP | Automatic cyclic termination proofs for recursive procedures in separation logic. | Reuben N. S. Rowe, James Brotherston |
| 2017 | TABLEAUX | Realizability in Cyclic Proof: Extracting Ordering Information for Infinite Descent. | Reuben N. S. Rowe, James Brotherston |
| 2009 | ECOOP | Semantic predicate types and approximation for class-based object oriented programming. | Steffen van Bakel, Reuben N. S. Rowe |