| 2009 |
| 9 | EE | James Brotherston,
Cristiano Calcagno:
Classical BI: a logic for reasoning about dualising resources.
POPL 2009: 328-339 |
| 2008 |
| 8 | EE | James Brotherston,
Richard Bornat,
Cristiano Calcagno:
Cyclic proofs of program termination in separation logic.
POPL 2008: 101-112 |
| 2007 |
| 7 | EE | James Brotherston,
Alex Simpson:
Complete Sequent Calculi for Induction and Infinite Descent.
LICS 2007: 51-62 |
| 6 | EE | James Brotherston:
Formalised Inductive Reasoning in the Logic of Bunched Implications.
SAS 2007: 87-103 |
| 2005 |
| 5 | EE | James Brotherston:
Cyclic Proofs for First-Order Logic with Inductive Definitions.
TABLEAUX 2005: 78-92 |
| 2003 |
| 4 | EE | René Vestergaard,
James Brotherston:
A formalised first-order confluence proof for the -calculus using one-sorted variable names.
Inf. Comput. 183(2): 212-244 (2003) |
| 2002 |
| 3 | EE | James Brotherston,
Anatoli Degtyarev,
Michael Fisher,
Alexei Lisitsa:
Searching for Invariants Using Temporal Resolution.
LPAR 2002: 86-101 |
| 2001 |
| 2 | EE | René Vestergaard,
James Brotherston:
A Formalised First-Order Confluence Proof for the lambda-Calculus Using One-Sorted Variable Names.
RTA 2001: 306-321 |
| 1 | EE | René Vestergaard,
James Brotherston:
The Mechanisation of Barendregt-Style Equational Proofs (the Residual Perspective).
Electr. Notes Theor. Comput. Sci. 58(1): (2001) |