James Brotherston

Senior Lecturer
Programming Principles, Logic and Verification Group (PPLV)
Dept. of Computer Science, University College London

E-mail: J.Brotherston@ucl.ac.uk

Address: Room 5.20,
Dept. of Computer Science,
Malet Place Engineering Building,
Gower Street,
London.
WC1E 6BT
United Kingdom

Erdös number: 4 (MathSciNet)
h-index: 17 (Google Scholar)

Jump to: Publications Slides

Program committees:


RAs and students:


Funding:


Online lectures:


Submitted papers:

[back to top]

Journal and conference papers:

  1. Automatic Cyclic Termination Proofs for Recursive Procedures in Separation Logic [BibTeX]
    Reuben Rowe and James Brotherston. In Proceedings of CPP-6, 2017.

  2. Machine-checked Interpolation Theorems for Substructural Logics using Display Calculi [BibTeX]
    Jeremy Dawson, James Brotherston and Rajeev Goré. In Proceedings of IJCAR-8, 2016.

  3. Model Checking for Symbolic-Heap Separation Logic with Inductive Predicates [BibTeX]
    James Brotherston, Nikos Gorogiannis, Max Kanovich and Reuben Rowe. In Proceedings of POPL-43, 2016.

  4. Disproving Inductive Entailments in Separation Logic via Base Pair Approximation [BibTeX]
    James Brotherston and Nikos Gorogiannis. In Proceedings of TABLEAUX-24, 2015.

  5. Sub-Classical Boolean Bunched Logics and the Meaning of Par [BibTeX]
    James Brotherston and Jules Villard. In Proceedings of CSL-24, 2015.

  6. Cyclic Abduction of Inductively Defined Safety and Termination Preconditions [BibTeX]
    James Brotherston and Nikos Gorogiannis. In Proceedings of SAS-21, 2014.

  7. A Decision Procedure for Satisfiability in Separation Logic with Inductive Predicates [BibTeX]
    James Brotherston, Carsten Fuhs, Nikos Gorogiannis and Juan Navarro Perez. In Proceedings of CSL-LICS, 2014.

  8. Undecidability of Propositional Separation Logic and its Neighbours [BibTeX]
    James Brotherston and Max Kanovich. In Journal of the ACM 61(2), April 2014.
    (Expanded journal version of the LICS'10 paper of the same name.)

  9. Parametric Completeness for Separation Theories [BibTeX]
    James Brotherston and Jules Villard. In Proceedings of POPL-41, 2014.

  10. A Generic Cyclic Theorem Prover [BibTeX]
    James Brotherston, Nikos Gorogiannis and Rasmus L. Petersen. In Proceedings of APLAS-10, 2012

  11. Bunched Logics Displayed [BibTeX]
    James Brotherston. In Studia Logica 100(6), Dec 2012
    (Expanded journal version of the MFPS'10 paper "A Unified Display Proof Theory for Bunched Logic".)

  12. Craig Interpolation in Displayable Logics [BibTeX]
    James Brotherston and Rajeev Goré. In Proceedings of TABLEAUX-20, 2011
    (An expanded version (PDF) containing detailed proofs is available as Imperial College technical report DTR11-1, 2011.)

  13. Automated Cyclic Entailment Proofs in Separation Logic [BibTeX]
    James Brotherston, Dino Distefano and Rasmus L. Petersen. In Proceedings of CADE-23, 2011.

  14. Sequent Calculi for Induction and Infinite Descent [BibTeX]
    James Brotherston and Alex Simpson. In Journal of Logic and Computation 21(6), Dec 2011.
    (Expanded journal version of the LICS'07 paper "Complete Sequent Calculi for Induction and Infinite Descent".)

  15. Undecidability of Propositional Separation Logic and its Neighbours [BibTeX]
    James Brotherston and Max Kanovich. In Proceedings of LICS-25, 2010.

  16. Classical BI: Its Semantics and Proof Theory [BibTeX]
    James Brotherston and Cristiano Calcagno. In Logical Methods in Computer Science 6(3), 2010.
    (Expanded journal version of the POPL'09 paper "Classical BI (A Logic for Reasoning about Dualising Resources)".)

  17. A Unified Display Proof Theory for Bunched Logic [BibTeX]
    James Brotherston. In Proceedings of MFPS-26, 2010.

  18. Classical BI (A Logic for Reasoning about Dualising Resources) [BibTeX]
    James Brotherston and Cristiano Calcagno. In Proceedings of POPL-36, 2009.

  19. Cyclic Proofs of Program Termination in Separation Logic [BibTeX]
    James Brotherston, Richard Bornat and Cristiano Calcagno. In Proceedings of POPL-35, 2008.

  20. Formalised Inductive Reasoning in the Logic of Bunched Implications [BibTeX] [Errata]
    James Brotherston. In Proceedings of SAS-14, 2007.

  21. Complete Sequent Calculi for Induction and Infinite Descent [BibTeX]
    James Brotherston and Alex Simpson. In Proceedings of LICS-22, 2007.

  22. Cyclic Proofs for First-Order Logic with Inductive Definitions [BibTeX]
    James Brotherston. In Proceedings of TABLEAUX-14, 2005.

  23. A Formalised First-Order Confluence Proof for the Lambda-Calculus using One-Sorted Variable Names [BibTeX]
    Rene Vestergaard and James Brotherston. In Information and Computation 183(2), 2003.
    (Expanded journal version of the RTA'01 article of the same name.)
    Isabelle/HOL proof developments

  24. Searching for Invariants using Temporal Resolution [BibTeX]
    James Brotherston, Anatoli Degtyarev, Michael Fisher and Alexei Lisitsa. In Proceedings of LPAR 2002.

  25. The Mechanisation of Barendregt-Style Equational Proofs (The Residual Perspective) [BibTeX]
    Rene Vestergaard and James Brotherston. In Proceedings of MERLIN 2001.
    Isabelle/HOL proof developments

  26. A Formalised First-Order Confluence Proof for the Lambda-Calculus using One-Sorted Variable Names (Barendregt was right after all ... almost) [BibTeX]
    Rene Vestergaard and James Brotherston. In Proceedings of RTA 2001.
    Isabelle/HOL proof developments
[back to top]

Theses and dissertations:

[back to top]

Slides:

[back to top]