Dr. James Brotherston

EPSRC Postdoctoral Research Fellow
Department of Computing, Imperial College London

Publications (most recent first):

Classical BI: Its Semantics and Proof Theory, with Cristiano Calcagno
- Abstract
- Article (PDF), in Logical Methods in Computer Science 6(3), 2010
- BibTeX entry
- NB. This article is an expanded journal version of the POPL'09 paper below.
Undecidability of Propositional Separation Logic and its Neighbours, with Max Kanovich
- Abstract
- Article (PDF), in Proceedings of LICS-25, 2010 (© IEEE Computer Society)
- BibTeX entry
- NB. A preliminary version of this paper was released as Imperial College technical report DTR10-1.
A Unified Display Proof Theory for Bunched Logic
- Abstract
- Article (PDF), pre-proceedings version, to appear in Proceedings of MFPS-26, 2010
- BibTeX entry
Classical BI (A Logic for Reasoning about Dualising Resources), with Cristiano Calcagno
- Abstract
- Article (PDF), in Proceedings of POPL-36, 2009 (© ACM)
- BibTeX entry
Cyclic Proofs of Program Termination in Separation Logic, with Richard Bornat and Cristiano Calcagno
- Abstract
- Article (PDF), in Proceedings of POPL-35, 2008 (© ACM)
- BibTeX entry
Formalised Inductive Reasoning in the Logic of Bunched Implications
- Abstract
- Article (PDF), in Proceedings of SAS-14, 2007 (© Springer LNCS series)
- BibTeX entry
- NB. The version here corrects a minor error in the published version, described here (PDF).
Complete Sequent Calculi for Induction and Infinite Descent, with Alex Simpson
- Abstract
- Article (PDF), in Proceedings of LICS-22, 2007 (© IEEE Computer Society)
- BibTeX entry
Sequent Calculus Proof Systems for Inductive Definitions, supervised by Alex Simpson
- Abstract
- PhD thesis (PDF) (PhD awarded November 2006, University of Edinburgh)
- BibTeX entry
Cyclic Proofs for First-Order Logic with Inductive Definitions
- Abstract
- Article (PDF), in Proceedings of TABLEAUX 2005 (© Springer LNAI series )
- BibTeX entry
A Formalised First-Order Confluence Proof for the Lambda-Calculus using One-Sorted Variable Names, with Rene Vestergaard
- Abstract
- Article (PDF), in Information and Computation 183(2), 2003 (© Elsevier Science)
- BibTeX entry
- Isabelle/HOL proof developments
- NB. This article is an expanded journal version of the RTA 2001 article below.
Searching for Invariants using Temporal Resolution, with Anatoli Degtyarev, Michael Fisher and Alexei Lisitsa
- Abstract
- Article (PDF), in Proceedings of LPAR 2002 (© Springer LNAI series )
- BibTeX entry
The Mechanisation of Barendregt-Style Equational Proofs (The Residual Perspective), with Rene Vestergaard
- Abstract
- Article (PDF), in Proceedings of MERLIN 2001 (© Elsevier Science B.V.)
- BibTeX entry
- Isabelle/HOL proof developments
A Formalised First-Order Confluence Proof for the Lambda-Calculus using One-Sorted Variable Names (Barendregt was right after all ... almost), with Rene Vestergaard
- Abstract
- Article (PDF), in Proceedings of RTA 2001 (© Springer Verlag, LNCS series)
- BibTeX entry
- Isabelle/HOL proof developments

Technical reports and unpublications (most recent first):

These articles are of the following types: (i) submitted papers; (ii) technical reports; (iii) papers in refereed workshops without formal proceedings.

Sequent Calculi for Induction and Infinite Descent, with Alex Simpson
- Abstract
- Article (PDF), revised version, submitted 2010 (original version submitted 2009)
- BibTeX entry
- NB. This article is an expanded and revised version of the LICS '07 paper above.
A Cut-Free Proof Theory for Boolean BI (via Display Logic)
- Abstract
- Article (PDF), released as Imperial College technical report DTR09-13, 2009
- BibTeX entry
- NB. This is an expanded and revised version of a previous incarnation of this paper. The old version is no longer available.
Algebraic Models and Complete Proof Calculi for Classical BI, with Cristiano Calcagno
- Abstract
- Article (PDF), released as Imperial College London technical report no. 2008/7
- BibTeX entry
Classical Logic of Bunched Implications, with Cristiano Calcagno
- Abstract
- Article (PDF), in the informal proceedings of CL&C 2008 (an ICALP satellite workshop)
- BibTeX entry
A Cyclic Termination Proof of In-Place List Reversal using Separation Logic, with Richard Bornat and Cristiano Calcagno
- Abstract
- Short article (PDF), in the informal proceedings of WST 2007 (an RDP satellite workshop)
- BibTeX entry
Proof Systems for Inductive Reasoning in the Logic of Bunched Implications
- Abstract
- Article (PDF), in the informal proceedings of HAV 2007 (an ETAPS satellite workshop)
- BibTeX entry
Formalizing Proofs in Isabelle/HOL of Equational Properties for the Lambda-Calculus using One-Sorted Variable Names, supervised by Rene Vestergaard
- Abstract
- Undergraduate Honours dissertation (PDF), for BSc(Hons) Computer Science & Mathematics, University of Edinburgh 2001
- BibTeX entry
- Isabelle/HOL developments for chapter 2 and chapter 3

Slides

Undecidability of Propositional Separation Logic and its Neighbours
- Slides (PDF) of a talk given at LICS-25 in Edinburgh on 12 July 2010, on the paper of the same name with Max Kanovich
- A longer and earlier version (PDF) of the slides above, used for talks given at Edinburgh University on 24 March 2010, and at Cambridge University on 12 March 2010,
A Unified Display Proof Theory for Bunched Logic, a.k.a. Bunched Logics Displayed
- Slides (PDF) of a talk given at MFPS in Ottawa, Canada, 9 May 2010, on the paper of the same name (earlier talks on the same subject were also given at UNILOG in Estoril, Portugal on 23 April 2010, and at the Gentzen Centenary Symposium, University of St. Andrews on 28 Nov 2009)
- A longer and earlier version (PDF) of the slides above, used for a talk given at the University of Edinburgh on 28 Oct 2009
Classical BI (A Logic for Reasoning about Dualising Resource)
- Slides (PDF) of a talk given at POPL in Savannah, GA on 23 Jan 2009, on the paper of the same name with Cristiano Calcagno
- A longer and earlier version (PDF) of the slides above, used for a talk given at the BLC meeting in Nottingham, 4 September 2008
- An even longer and earlier version (PDF), used for talks given at the University of Edinburgh on 23 Oct 2008 and at Cambridge University on 10 Oct 2008
An Introduction to Cyclic Proofs
- Slides (PDF) of a talk given at the London Theory Day, Imperial College London, 11 April 2008
Cyclic Proofs of Program Termination in Separation Logic
- Slides (PDF) of a talk given at POPL in San Francisco, USA, 10 January 2008, on the paper of the same name with Richard Bornat and Cristiano Calcagno
- An earlier and longer version (PDF) of the slides above, used for a seminar given at Imperial College on 12 December 2007
Formalised Inductive Reasoning in the Logic of Bunched Implications
- Slides (PDF) for a talk given at SAS in Kongens Lyngby, Denmark, 22 August 2007, on the paper of the same name
- An earlier version (PDF) of the same slides, used for a talk at the HAV workshop in Braga, Portugal, March 2007 on the earlier version of the paper
Complete Sequent Calculi for Induction and Infinite Descent
- Slides (PDF) for a talk given at LICS in Wroclaw, Poland, 10 July 2007, on the paper of the same name with Alex Simpson
- An earlier and longer version (PDF) of the same slides, used for a seminar given at the Dept. of Computing, University of Leicester on 2 March 2007

Contact details

E-mail:	J DOT Brotherston AT imperial DOT ac DOT uk
Phone:	+44 (0)207 594 8291
Fax:	+44 (0)207 581 8024
Address:	Room 449 Huxley Building, Department of Computing, 180 Queen's Gate, South Kensington Campus, Imperial College London, London SW7 2AZ.

Statement on the Retention of Intellectual Property Rights

The copyright of all works linked on this page rests with the author(s), unless otherwise stated. The items may be downloaded, used, and referenced exclusively for scholarly, non-commercial purposes and proper reference to their origin must be provided on each occasion. Excerpts beyond scholarly referencing may be reproduced solely with the express consent of the copyright holder(s).