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) |