A Formalised First-Order Confluence Proof for the lambda-Calculus Using One-Sorted Variable Names. - René Vestergaard; James Brotherston (RTA, 2001)

The Mechanisation of Barendregt-Style Equational Proofs (the Residual Perspective). - René Vestergaard; James Brotherston (MERLIN, 2001)

Searching for Invariants Using Temporal Resolution. - James Brotherston; Anatoli Degtyarev; Michael Fisher 001; Alexei Lisitsa 001 (LPAR, 2002)

A formalised first-order confluence proof for the -calculus using one-sorted variable names. - René Vestergaard; James Brotherston (Inf. Comput., 2003)

Cyclic Proofs for First-Order Logic with Inductive Definitions. - James Brotherston (TABLEAUX, 2005)

Complete Sequent Calculi for Induction and Infinite Descent. - James Brotherston; Alex Simpson (LICS, 2007)

Formalised Inductive Reasoning in the Logic of Bunched Implications. - James Brotherston (SAS, 2007)

Cyclic proofs of program termination in separation logic. - James Brotherston; Richard Bornat; Cristiano Calcagno (POPL, 2008)

Classical BI: a logic for reasoning about dualising resources. - James Brotherston; Cristiano Calcagno (POPL, 2009)

Undecidability of Propositional Separation Logic and Its Neighbours. - James Brotherston; Max I. Kanovich (LICS, 2010)

Classical BI: Its Semantics and Proof Theory - James Brotherston; Cristiano Calcagno (Log. Methods Comput. Sci., 2010)

A Unified Display Proof Theory for Bunched Logic. - James Brotherston (MFPS, 2010)

Automated Cyclic Entailment Proofs in Separation Logic. - James Brotherston; Dino Distefano; Rasmus Lerchedahl Petersen (CADE, 2011)

Craig Interpolation in Displayable Logics. - James Brotherston; Rajeev Goré (TABLEAUX, 2011)

Sequent calculi for induction and infinite descent. - James Brotherston; Alex Simpson (J. Log. Comput., 2011)

A Generic Cyclic Theorem Prover. - James Brotherston; Nikos Gorogiannis; Rasmus Lerchedahl Petersen (APLAS, 2012)

Bunched Logics Displayed. - James Brotherston (Stud Logica, 2012)

A decision procedure for satisfiability in separation logic with inductive predicates. - James Brotherston; Carsten Fuhs; Juan Antonio Navarro Pérez; Nikos Gorogiannis (CSL-LICS, 2014)

Parametric completeness for separation theories. - James Brotherston; Jules Villard (POPL, 2014)

Cyclic Abduction of Inductively Defined Safety and Termination Preconditions. - James Brotherston; Nikos Gorogiannis (SAS, 2014)

Sub-classical Boolean Bunched Logics and the Meaning of Par. - James Brotherston; Jules Villard (CSL, 2015)

Disproving Inductive Entailments in Separation Logic via Base Pair Approximation. - James Brotherston; Nikos Gorogiannis (TABLEAUX, 2015)

Machine-Checked Interpolation Theorems for Substructural Logics Using Display Calculi. - Jeremy E. Dawson; James Brotherston; Rajeev Goré (IJCAR, 2016)

Model checking for symbolic-heap separation logic with inductive predicates. - James Brotherston; Nikos Gorogiannis; Max I. Kanovich; Reuben Rowe (POPL, 2016)

Biabduction (and Related Problems) in Array Separation Logic. - James Brotherston; Nikos Gorogiannis; Max I. Kanovich (CADE, 2017)

Automatically Verifying Temporal Properties of Pointer Programs with Cyclic Proof. - Gadi Tellez; James Brotherston (CADE, 2017)

Automatic cyclic termination proofs for recursive procedures in separation logic. - Reuben N. S. Rowe; James Brotherston (CPP, 2017)

Realizability in Cyclic Proof: Extracting Ordering Information for Infinite Descent. - Reuben N. S. Rowe; James Brotherston (TABLEAUX, 2017)

Size Relationships in Abstract Cyclic Entailment Systems. - Reuben N. S. Rowe; James Brotherston (CoRR, 2017)

On the Complexity of Pointer Arithmetic in Separation Logic. - James Brotherston; Max I. Kanovich (APLAS, 2018)

On the Complexity of Pointer Arithmetic in Separation Logic (an extended version). - James Brotherston; Max I. Kanovich (CoRR, 2018)

Reasoning over Permissions Regions in Concurrent Separation Logic. - James Brotherston; Diana Costa 001; Aquinas Hobor; John Wickerson (CAV (2), 2020)

A Compositional Deadlock Detector for Android Java. - James Brotherston; Paul Brunet; Nikos Gorogiannis; Max I. Kanovich (ASE, 2021)

Mix Testing: Specifying and Testing ABI Compatibility of C/C++ Atomics Implementations. - Luke Geeson; James Brotherston; Wilco Dijkstra; Alastair F. Donaldson; Lee Smith; Tyler Sorensen 001; John Wickerson (Proc. ACM Program. Lang., 2024)

The failure of cut-elimination in cyclic proof for first-order logic with inductive definitions. - Yukihiro Oda; James Brotherston; Makoto Tatsuta (J. Log. Comput., 2025)

Cyclic Proofs in Hoare Logic and its Reverse. - James Brotherston; Quang Loc Le; Gauri Desai; Yukihiro Oda (CoRR, 2025)