James Brotherston
Senior Lecturer & EPSRC Career Acceleration Fellow
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
Jump to:
Publications
Slides
Program committees:
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)
RAs and students:
Prof. Max Kanovich
, Research Associate at UCL, Jan 2015 - present
Dr. Reuben Rowe
, Research Associate at UCL, May 2014 - present
Dr. Quratul-ain Mahesar, Research Associate at UCL, Dec 2013 - Sept '14
Pavle Subotic
, PhD student at UCL from 2015 (second supervisor)
Kareem Khazem
, PhD student at UCL from 2014
Brett McLean
, PhD student at UCL from 2013 (second supervisor)
Gadi Tellez Espinosa
, PhD student at UCL from 2013
Ana Armas
, MSc(Distinction) in Computing, Imperial College London, 2010-11
Online lectures:
An Introduction to Separation Logic
(YouTube)
Delivered at Oracle Labs, Brisbane in Dec 2015, with accompanying
slides
.
Submitted papers:
Biabduction (and Related Problems) in Array Separation Logic
[
BibTeX
]
James Brotherston,
Nikos Gorogiannis
and
Max Kanovich
. arXiv:1607.01993. Revised, Nov 2016; v1 submitted July 2016.
Automatically Verifying Temporal Properties of Programs with Cyclic Proof
[
BibTeX
]
Gadi Tellez Espinosa
and James Brotherston. Submitted, 2016.
[
back to top
]
Journal and conference papers:
Automatic Cyclic Termination Proofs for Recursive Procedures in Separation Logic
[
BibTeX
]
Reuben Rowe
and James Brotherston. To appear 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
[
back to top
]
Theses and dissertations:
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
[
back to top
]
Slides:
Biabduction (and Related Problems) in Array Separation Logic
Presented at the University of Bath in Nov 2016.
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:
An introduction to separation logic
Boolean bunched logic: its semantics and completeness
Proof theory for Boolean bunched logic
Undecidability of Boolean bunched logic
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.
Cyclic Abduction of Inductive Safety and Termination Preconditions
Presented at the LIX Colloquium on the Theory and Application of Formal Proofs, Nov 2013.
Parametric Completeness for Separation Theories
Presented at the University of Birmingham in Oct 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.
[
back to top
]