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).
Program committees:
Supervision:
- Ana Armas, MSc(Distinction) in Computing, Imperial College London, 2010-11
Teaching:
Submitted papers:
[back to top]
Journal and conference papers:
- Craig Interpolation in Displayable Logics, with Rajeev Goré
- Automated Cyclic Entailment Proofs in Separation Logic, with Dino Distefano and Rasmus L. Petersen
- 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
- A Unified Display Proof Theory for Bunched Logic
- Classical BI (A Logic for Reasoning about Dualising Resources), with Cristiano Calcagno
- Cyclic Proofs of Program Termination in Separation Logic, with Richard Bornat and Cristiano Calcagno
- Formalised Inductive Reasoning in the Logic of Bunched Implications
- Complete Sequent Calculi for Induction and Infinite Descent,
with Alex Simpson
- Cyclic Proofs for First-Order Logic with Inductive Definitions
- A Formalised First-Order Confluence Proof for the Lambda-Calculus using One-Sorted Variable Names, with Rene Vestergaard
- Searching for Invariants using Temporal
Resolution, with
Anatoli Degtyarev,
Michael Fisher and
Alexei Lisitsa
- The Mechanisation of Barendregt-Style Equational Proofs
(The Residual Perspective), with
Rene Vestergaard
- A Formalised First-Order
Confluence Proof for the Lambda-Calculus using One-Sorted Variable
Names (Barendregt was right after all ... almost),
with Rene Vestergaard
[back to top]
Theses and dissertations:
- Sequent Calculus Proof Systems for Inductive Definitions,
supervised by Alex Simpson
- Formalizing Proofs in Isabelle/HOL of Equational Properties for the
Lambda-Calculus using One-Sorted Variable Names, supervised by
Rene Vestergaard
[back to top]
Slides:
- 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)
- 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
- 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
[back to top]