James Brotherston

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

• Journal of Logic and Computation
• Logic Journal of the IGPL

• CSL 2024 (Computer Science Logic)
• FoSSaCS 2024 (Foundations of Software Science and Computation Structures)
• IJCAR 2020 (International Joint Conference on Automated Reasoning)
• CSL 2020 (Computer Science Logic)
• TABLEAUX 2019 (Tableaux and Related Methods)
• LiCS 2017 (Logic in Computer Science)
• FoSSaCS 2017 (Foundations of Software Science and Computation Structures)
• APLAS 2015 (Asian Symposium on Programming Languages and Systems)
• MFPS 2015 (Mathematical Foundations of Programming Semantics)
• CPP 2015 (Certified Programs and Proofs)
• APLAS 2011 (Asian Symposium on Programming Languages and Systems)

• RADICAL 2023 (Recent Advances in Concurrency and Logic)
• ASL 2022 (Advances in Separation Logics)
• ADSL 2020 (Automated Deduction for Separation Logics)
• RADICAL 2019 (Recent Advances in Concurrency and Logic)
• EICNCL 2018 (External and Internal Calculi for Non-Classical Logics)
• ADSL 2018 (Automated Deduction for Separation Logics)
• RADICAL 2017 (Recent Advances in Concurrency and Logic)
• SD 2017 (Structures and Deduction)

• Dr Estibaliz Fraca, Research Fellow at UCL, Nov 2020 - Dec 2024
  
• Dr Paul Brunet, Research Fellow at UCL, Oct 2018 - 2021
  
• Dr Diana Costa, Research Fellow at UCL, Oct 2018 - 2021
  
• Prof. Max Kanovich, Research Associate / Fellow at UCL, Jan 2015 - Jan 2018, and Sept 2018 - present
  
• Dr Reuben Rowe, Research Associate at UCL, May 2014 - Nov 2016
  
• Dr Quratul-ain Mahesar, Research Associate at UCL, Dec 2013 - Sept 2014
  

• Luke Geeson, PhD student at UCL, April 2023 - present
  
• Dr Jas Semrl, PhD student at UCL, Oct 2019 - Sep 2023 (second supervisor)
• Dr Pavle Subotic, PhD student at UCL, Oct 2015 - August 2018 (second supervisor)
  
• Kareem Khazem, PhD student at UCL, Oct 2014 - 2018
  
• Dr Brett McLean, PhD student at UCL, Oct 2013 - Feb 2018 (second supervisor)
  
• Dr Gadi Tellez Espinosa, PhD student at UCL, Oct 2013 - Dec 2018

• Facebook Testing and Verification Research Award
  USD 50,000, Oct 2019.


• Co-Investigator, "Interface Reasoning for Interacting Systems (IRIS)"
  EPSRC Programme Grant EP/R006865/1, PI: David Pym. GBP 6,146,075, Jan 2018 - Dec 2024.


• Facebook Faculty Grant
  USD 30,000, Sept 2015.


• Principal Investigator, "Boosting Automated Verification using Cyclic Proof"
  EPSRC Responsive Mode Grant EP/K040049/1. GBP 550,181, Nov 2013 - May 2017.


• EPSRC Career Acceleration Fellowship, "Logical Foundations of Resource"
  EPSRC grant EP/J002224/1. GBP 465,503, Dec 2011 - Nov 2016.


• EPSRC Postdoctoral Fellowship, "Cyclic Proofs for Logic-Based Program Verification"
  EPSRC grant EP/F043767/1. GBP 253,391, Nov 2008 - Oct 2011.

• An Introduction to Formal Logic (YouTube)
  A 15-lecture series of prerecorded online lectures on formal mathematical logic, aimed at first-year CS undergraduates and produced during the Covid-19 pandemic in 2020/21.

• Mix Testing: Specifying and Testing ABI Compatibility of C/C++ Atomics Implementations [BibTeX]
  Luke Geeson, James Brotherston, Wilco Dijkstra, Alastair Donaldson, Lee Smith, Tyler Sorensen and John Wickerson. To appear in Proceedings of OOPSLA, 2024.
  
  
• The failure of cut-elimination in cyclic proof for first-order logic with inductive definitions [BibTeX]
  Yukihiro Oda, James Brotherston and Makoto Tatsuta. In Journal of Logic and Computation, exad068, Dec 2023.
  
  
• A Compositional Deadlock Detector for Android Java [BibTeX]
  James Brotherston, Paul Brunet, Nikos Gorogiannis and Max Kanovich. In Proceedings of ASE-36, 2021.
  
  
• Reasoning over Permissions Regions in Concurrent Separation Logic [BibTeX]
  James Brotherston, Diana Costa, Aquinas Hobor and John Wickerson. In Proceedings of CAV-32, 2020.
  
  
• Automatically Verifying Temporal Properties of Programs with Cyclic Proof [BibTeX]
  Gadi Tellez Espinosa and James Brotherston. In Journal of Automated Reasoning, 2019.
  (Expanded journal version of the CADE'17 paper of the same name.)
  
  
• On the Complexity of Pointer Arithmetic in Separation Logic [BibTeX]
  James Brotherston and Max Kanovich. In Proceedings of APLAS-16, 2018.
  
  
• Realizability in Cyclic Proof: Extracting Ordering Information for Infinite Descent [BibTeX]
  Reuben Rowe and James Brotherston. In Proceedings of TABLEAUX-26, 2017.
  
  
• Biabduction (and Related Problems) in Array Separation Logic [BibTeX]
  James Brotherston, Nikos Gorogiannis and Max Kanovich. In Proceedings of CADE-26, 2017. Long version available as arXiv:1607.01993.
  
  
• Automatically Verifying Temporal Properties of Programs with Cyclic Proof [BibTeX]
  Gadi Tellez Espinosa and James Brotherston. In Proceedings of CADE-26, 2017.
  
  
• Automatic Cyclic Termination Proofs for Recursive Procedures in Separation Logic [BibTeX]
  Reuben Rowe and James Brotherston. In Proceedings of CPP-6, 2017.
  
  
• Machine-checked Interpolation Theorems for Substructural Logics using Display Calculi [BibTeX]
  Jeremy Dawson, James Brotherston and Rajeev Goré. In Proceedings of IJCAR-8, 2016.
  
  
• 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.
  
  
• Disproving Inductive Entailments in Separation Logic via Base Pair Approximation [BibTeX]
  James Brotherston and Nikos Gorogiannis. In Proceedings of TABLEAUX-24, 2015.
  
  
• Sub-Classical Boolean Bunched Logics and the Meaning of Par [BibTeX]
  James Brotherston and Jules Villard. In Proceedings of CSL-24, 2015.
  
  
• Cyclic Abduction of Inductively Defined Safety and Termination Preconditions [BibTeX]
  James Brotherston and Nikos Gorogiannis. In Proceedings of SAS-21, 2014.
  
  
• 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.
  
  
• 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.)
  
  
• Parametric Completeness for Separation Theories [BibTeX]
  James Brotherston and Jules Villard. In Proceedings of POPL-41, 2014.
  
  
• A Generic Cyclic Theorem Prover [BibTeX]
  James Brotherston, Nikos Gorogiannis and Rasmus L. Petersen. In Proceedings of APLAS-10, 2012
  
  
• 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".)
  
  
• 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.)
  
  
• Automated Cyclic Entailment Proofs in Separation Logic [BibTeX]
  James Brotherston, Dino Distefano and Rasmus L. Petersen. In Proceedings of CADE-23, 2011.
  
  
• 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".)
  
  
• Undecidability of Propositional Separation Logic and its Neighbours [BibTeX]
  James Brotherston and Max Kanovich. In Proceedings of LICS-25, 2010.
  
  
• 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)".)
  
  
• A Unified Display Proof Theory for Bunched Logic [BibTeX]
  James Brotherston. In Proceedings of MFPS-26, 2010.
  
  
• Classical BI (A Logic for Reasoning about Dualising Resources) [BibTeX]
  James Brotherston and Cristiano Calcagno. In Proceedings of POPL-36, 2009.
  
  
• Cyclic Proofs of Program Termination in Separation Logic [BibTeX]
  James Brotherston, Richard Bornat and Cristiano Calcagno. In Proceedings of POPL-35, 2008.
  
  
• Formalised Inductive Reasoning in the Logic of Bunched Implications [BibTeX] [Errata]
  James Brotherston. In Proceedings of SAS-14, 2007.
  
  
• Complete Sequent Calculi for Induction and Infinite Descent [BibTeX]
  James Brotherston and Alex Simpson. In Proceedings of LICS-22, 2007.
  
  
• Cyclic Proofs for First-Order Logic with Inductive Definitions [BibTeX]
  James Brotherston. In Proceedings of TABLEAUX-14, 2005.
  
  
• 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
  
  
• Searching for Invariants using Temporal Resolution [BibTeX]
  James Brotherston, Anatoli Degtyarev, Michael Fisher and Alexei Lisitsa. In Proceedings of LPAR 2002.
  
  
• 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
  
  
• 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

• Sequent Calculus Proof Systems for Inductive Definitions [BibTeX]
  James Brotherston. PhD thesis, University of Edinburgh, 2006.
  
  
• Formalizing Proofs in Isabelle/HOL of Equational Properties for the Lambda-Calculus using One-Sorted Variable Names [BibTeX]
  James Brotherston. Honours dissertation, BSc(Hons) Computer Science & Mathematics, University of Edinburgh, 2001.
  Isabelle/HOL developments for chapter 2 and chapter 3

• PPLV seminar slides, Oct 2022: two alternative talks here and here.
• Reasoning over Permissions Regions in Concurrent Separation Logic
  Presented at the IRIS Day O'Science, remotely, in April 2020.
  
  
• Separation Logics for Pointer Programs
  Keynote talk at the Lorentz Workshop "Effective Verification: Static Analysis Meets Program Logics", in Leiden, the Netherlands in May 2019.
  
  
• On the Complexity of Pointer Arithmetic in Separation Logic
  Presented at APLAS-16 in Wellington, New Zealand in December 2018.
  
  
• An Introduction to Cyclic Proofs (part I) and (part II)
  Invited talk in two parts at the PARIS workshop at FLoC, at the University of Oxford in July 2018.
  
  
• Biabduction (and Related Problems) in Array Separation Logic
  Invited talk for the TICAMORE project kickoff meeting at the University of Vienna in March 2017.
  
  
• Machine-checked Interpolation Theorems for Substructural Logics using Display Calculi
  Presented at IJCAR-8 in Coimbra, Portugal in June 2016.
  
  
• Complete Sequent Calculi for Induction and Infinite Descent
  Presented at the University of Leeds in Feb 2016 (and, long before that, at LICS 2007 in Wroclaw, Poland).
  
  
• Model Checking for Symbolic-Heap Separation Logic with Inductive Predicates
  Presented at Oracle Labs in Brisbane, Australia (and at the Australian National University in Canberra) in Dec 2015.
  
  
• A Short Course on Boolean Bunched Logic
  A 5-lecture series presented at the Logic Summer School, Australian National University, Dec 2015:
  
  1. An introduction to separation logic
  2. Boolean bunched logic: its semantics and completeness
  3. Proof theory for Boolean bunched logic
  4. Undecidability of Boolean bunched logic
  5. Definability in Boolean bunched logic
  
  
• Sub-Classical Boolean Bunched Logics and the Meaning of Par
  Presented at CSL-24 in Berlin, Germany in Sept 2015.
  
  
• Disproving Inductive Entailments in Separation Logic via Base Pair Approximation
  Presented at TABLEAUX-24 in Wroclaw, Poland in Sept 2015.
  
  
• Parametric Completeness for Separation Theories
  Presented at New York University in Dec 2014.
  
  
• Cyclic Abduction of Inductive Safety and Termination Preconditions
  Invited talk at the LIX Colloquium on the Theory and Application of Formal Proofs, Nov 2013.
  
  
• Craig Interpolation in Displayable Logics
  Presented at TABLEAUX-20 in Bern, Switzerland in July 2011.
  
  
• Undecidability of Propositional Separation Logic and its Neighbours
  Presented at LICS-25 in Edinburgh in July 2010.
  Seminar-length version of the same slides, presented at Tallinn University of Technology in Nov 2011.
  
  
• A Unified Display Proof Theory for Bunched Logic, a.k.a. Bunched Logics Displayed
  Presented at MFPS-26 in Ottawa, Canada in May 2010.
  Seminar-length version of the same slides above, presented at the University of Edinburgh in Oct 2009.
  
  
• Classical BI (A Logic for Reasoning about Dualising Resource)
  Presented at POPL-36 in Savannah, GA in Jan 2009.
  Seminar-length version of the same slides, presented at the University of Edinburgh in Oct 2008.
  
  
• An Introduction to Cyclic Proofs
  Presented at the London Theory Day, Imperial College London in April 2008.
  
  
• Cyclic Proofs of Program Termination in Separation Logic
  Presented at POPL-35 in San Francisco, USA in January 2008.
  Seminar-length version of the same slides, presented at Imperial College on 12 December 2007
  
  
• Formalised Inductive Reasoning in the Logic of Bunched Implications
  Presented at SAS-14 in Kongens Lyngby, Denmark in August 2007.