Dr. James Brotherston

EPSRC Postdoctoral Research Fellow
Department of Computing, Imperial College London

Publications (most recent first):

Classical BI (A Logic for Reasoning about Dualising Resource), with Cristiano Calcagno
- Abstract
- Article (PDF), in Proceedings of POPL-36, 2009 (© ACM)
- BibTeX entry
- NB. This article supersedes the CL&C 2008 workshop paper below.
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
- NB. This article supersedes the WST 2007 workshop paper below.
Formalised Inductive Reasoning in the Logic of Bunched Implications
- Abstract
- Article (PDF), in Proceedings of SAS-14, 2007 (© Springer LNCS series)
- BibTeX entry
- NB I. The version of the article here corrects a minor error in the published version, described here (PDF).
- NB II. This article supersedes the HAV 2007 workshop paper below.
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 (PostScript), also available gzipped, in Information and Computation 183:2, 2003 (© Elsevier Science)
- BibTeX entry
- Isabelle/HOL proof developments
- NB. This article is an expanded 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 (PostScript), in Proceedings of RTA 2001 (© Springer Verlag, LNCS series)
- BibTeX entry
- Isabelle/HOL proof developments

Technical reports and unpublications (most recent first):

Classical BI: Its Semantics and Proof Theory, with Cristiano Calcagno
- Abstract
- Article (PDF), revised version, submitted 2010
- BibTeX entry
- NB. This article is an expanded and revised version of the POPL '09 paper above.
Undecidability of Propositional Separation Logic and its Neighbours, with Max Kanovich
- Submitted, 2010
Sequent Calculi for Induction and Infinite Descent, with Alex Simpson
- Abstract
- Article (PDF), revised version, submitted 2009
- BibTeX entry
- NB. This article is an expanded and revised version of the LICS '07 paper above.
A Unified Display Proof Theory for Bunched Logic
- Abstract
- Article (PDF), submitted 2009
- BibTeX entry
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
- 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
- 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 (PS), for BSc(Hons) Computer Science & Mathematics, University of Edinburgh 2001
- BibTeX entry
- Isabelle/HOL developments for chapter 2 and chapter 3

Slides

Bunched Logics Displayed
- Slides (PDF), of a talk given at the Gentzen Centenary Symposium, University of St. Andrews on 28 Nov 2009, on the paper "A Unified Display Proof Theory for Bunched Logic"
- A longer version (PDF) of the slides above, used for a talk given at the University of Edinburgh on 28 Oct 2009, on the paper "A Unified Display Proof Theory for Bunched Logic"
Classical BI (A Logic for Reasoning about Dualising Resource)
- Slides (PDF) of a talk given at the University of Edinburgh on 23 Oct 2008 (and previously at Cambridge University on 10 Oct 2008), on the paper of the same name with Cristiano Calcagno
- A shorter version (PDF) of the slides above, used for a talk given at the BLC meeting in Nottingham, 4 September 2008
- An even shorter version (PDF), used for a talk given at POPL in Savannah, GA on 23 Jan 2009
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
- A more detailed 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 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).