Travelled to:1 × Austria
1 × Denmark
1 × The Netherlands
1 × United Kingdom
2 × Germany
2 × Poland
3 × USA
Collaborated with:N.Gorogiannis M.I.Kanovich J.Villard C.Calcagno A.Simpson ∅ R.Vestergaard G.Tellez D.Distefano R.L.Petersen R.Bornat J.E.Dawson R.Goré C.Fuhs J.A.N.Pérez Reuben Rowe
Talks about:logic (10) separ (7) induct (5) cyclic (4) proof (4) formalis (2) program (2) complet (2) classic (2) calculi (2)
Person: James Brotherston
DBLP: Brotherston:James
Contributed to:
2015
2014
2014
2014
201120102009200820072007
2001
201620172016Wrote 15 papers:
- CSL-2015-BrotherstonV #logic
- Sub-classical Boolean Bunched Logics and the Meaning of Par (JB, JV), pp. 325–342.
- LICS-CSL-2014-BrotherstonFPG #induction #logic #satisfiability
- A decision procedure for satisfiability in separation logic with inductive predicates (JB, CF, JANP, NG), p. 10.
- POPL-2014-BrotherstonV #parametricity
- Parametric completeness for separation theories (JB, JV), pp. 453–464.
- SAS-2014-BrotherstonG #abduction #safety #termination
- Cyclic Abduction of Inductively Defined Safety and Termination Preconditions (JB, NG), pp. 68–84.
- CADE-2011-BrotherstonDP #automation #logic #proving
- Automated Cyclic Entailment Proofs in Separation Logic (JB, DD, RLP), pp. 131–146.
- LICS-2010-BrotherstonK #logic
- Undecidability of Propositional Separation Logic and Its Neighbours (JB, MIK), pp. 130–139.
- POPL-2009-BrotherstonC #logic #reasoning
- Classical BI: a logic for reasoning about dualising resources (JB, CC), pp. 328–339.
- POPL-2008-BrotherstonBC #logic #proving #termination
- Cyclic proofs of program termination in separation logic (JB, RB, CC), pp. 101–112.
- LICS-2007-BrotherstonS #calculus #induction #infinity
- Complete Sequent Calculi for Induction and Infinite Descent (JB, AS), pp. 51–62.
- SAS-2007-Brotherston #induction #logic #reasoning
- Formalised Inductive Reasoning in the Logic of Bunched Implications (JB), pp. 87–103.
- RTA-2001-VestergaardB #confluence #first-order #proving #using #λ-calculus
- A Formalised First-Order Confluence Proof for the λ-Calculus Using One-Sorted Variable Names (RV, JB), pp. 306–321.
- IJCAR-2016-DawsonBG #calculus #logic #theorem #using
- Machine-Checked Interpolation Theorems for Substructural Logics Using Display Calculi (JED, JB, RG), pp. 452–468.
- CADE-2017-BrotherstonGK #array #logic #problem
- Biabduction (and Related Problems) in Array Separation Logic (JB, NG, MIK), pp. 472–490.
- CADE-2017-TellezB #automation #pointer #proving #source code #verification
- Automatically Verifying Temporal Properties of Pointer Programs with Cyclic Proof (GT, JB), pp. 491–508.
- POPL-2016-BrotherstonGKR #induction #logic #model checking
- Model checking for symbolic-heap separation logic with inductive predicates (JB, NG, MIK, RR), pp. 84–96.