Dr. James Brotherston

EPSRC Career Acceleration Fellow
School of Electronic Engineering and Computer Science
Queen Mary, University of London

The copyright of all works linked on this page rests with the author(s), unless otherwise stated. Excerpts beyond scholarly referencing may be reproduced solely with the express consent of the copyright holder(s).

• APLAS 2011

• Ana Armas, MSc(Distinction) in Computing, Imperial College London, 2010-11

• DCS301 / AMCM060 Computability (QM intranet), Queen Mary, semester 2, academic year 2011/12

• Undecidability of Propositional Separation Logic, with Max Kanovich
  • Abstract
  • Article (PDF), submitted 2012
  • BibTeX entry
  • NB. This article is an expanded journal version of the LICS'10 paper "Undecidability of Propositional Separation Logic and its Neighbours".
  
  
  
• A Generic Cyclic Theorem Prover, with Nikos Gorogiannis and Rasmus L. Petersen
  • Abstract
  • Article (PDF), submitted 2012
  • BibTeX entry
  • Source code (gzipped tarball) for the CYCLIST theorem prover

• Craig Interpolation in Displayable Logics, with Rajeev Goré
  • Abstract
  • Article (PDF), in Proceedings of TABLEAUX-20, 2011 (© Springer LNAI series)
  • Expanded version (PDF), containing detailed proofs and released as Imperial College technical report DTR11-1, 2011
  • BibTeX entries for both the article and the technical report
  
  
  
• Automated Cyclic Entailment Proofs in Separation Logic, with Dino Distefano and Rasmus L. Petersen
  • Abstract
  • Article (PDF), in Proceedings of CADE-23, 2011 (© Springer LNAI series)
  • BibTeX entry
  
  
  
• Bunched Logics Displayed
  • Abstract
  • Article (PDF), to appear in Studia Logica: Special Issue on Recent Developments related to Residuated Lattices and Substructural Logics, 2011
  • BibTeX entry
  • NB. This article is an expanded journal version of the MFPS'10 paper "A Unified Display Proof Theory for Bunched Logic".
  
  
  
• Sequent Calculi for Induction and Infinite Descent, with Alex Simpson
  • Abstract
  • Article (PDF), to appear in Journal of Logic and Computation, Advance Access version published 2010 (© Oxford University Press)
  • BibTeX entry
  • NB. This article is an expanded journal version of the LICS'07 paper "Complete Sequent Calculi for Induction and Infinite Descent".
  
  
  
• 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 "Classical BI (A Logic for Reasoning about Dualising Resources)".
  
  
  
• 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), in Proceedings of MFPS-26, 2010 (© Elsevier B.V. ENTCS series)
  • 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
  
  
  
• Cyclic Proofs for First-Order Logic with Inductive Definitions
  • Abstract
  • Article (PDF), in Proceedings of TABLEAUX-14, 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'01 article of the same name.
  
  
  
• 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 B.V. ENTCS series)
  • 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

• Sequent Calculus Proof Systems for Inductive Definitions, supervised by Alex Simpson
  • Abstract
  • PhD thesis (PDF) (PhD awarded November 2006, University of Edinburgh)
  • BibTeX entry
  
  
  
• Formalizing Proofs in Isabelle/HOL of Equational Properties for the Lambda-Calculus using One-Sorted Variable Names, supervised by Rene Vestergaard
  • Abstract
  • Honours dissertation (PDF), for BSc(Hons) Computer Science & Mathematics, University of Edinburgh 2001
  • BibTeX entry
  • Isabelle/HOL developments for chapter 2 and chapter 3

• Craig Interpolation in Displayable Logics
  • Slides (PDF) of a talk given at TABLEAUX-20 in Bern, Switzerland on 7 July 2011, on the paper of the same name with Rajeev Goré (an earlier version was given at the ALCOP workshop in Bern, Switzerland on 28 April 2011)
  
  
  
• Undecidability of Propositional Separation Logic and its Neighbours
  • Slides (PDF) of a talk given at Tallinn University of Technology on 17 Nov 2011, on the paper of the same name with Max Kanovich (earlier talks on the same subject were also given Sussex University on 24 Nov 2010, at Edinburgh University on 24 March 2010, and at Cambridge University on 12 March 2010)
  • An older and shorter version (PDF) of the slides, used for the talk given at LICS-25 in Edinburgh on 12 July 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