James Brotherston

Available identifiers

zbMath Open brotherston.jamesMaRDI QIDQ1401935

List of research outcomes

Publication	Date of Publication	Type
On the complexity of pointer arithmetic in separation logic	2023-08-02	Paper
Reasoning over permissions regions in concurrent separation logic	2021-02-09	Paper
Automatically verifying temporal properties of pointer programs with cyclic proof	2020-03-03	Paper
A decision procedure for satisfiability in separation logic with inductive predicates	2018-04-23	Paper
Realizability in cyclic proof: extracting ordering information for infinite descent	2018-02-02	Paper
Automatically verifying temporal properties of pointer programs with cyclic proof	2017-09-22	Paper
Biabduction (and related problems) in array separation logic	2017-09-22	Paper
Sub-classical Boolean Bunched Logics and the Meaning of Par	2017-08-31	Paper
Model checking for symbolic-heap separation logic with inductive predicates	2016-10-24	Paper
Machine-Checked Interpolation Theorems for Substructural Logics Using Display Calculi	2016-09-05	Paper
A Unified Display Proof Theory for Bunched Logic	2016-07-08	Paper
Disproving Inductive Entailments in Separation Logic via Base Pair Approximation	2015-12-11	Paper
Classical BI	2015-07-03	Paper
Undecidability of Propositional Separation Logic and Its Neighbours	2014-09-12	Paper
Cyclic proofs of program termination in separation logic	2014-09-12	Paper
Parametric completeness for separation theories	2014-04-10	Paper
The mechanisation of Barendregt-style equational proofs (the residual perspective)	2013-07-24	Paper
Bunched logics displayed	2013-02-18	Paper
Sequent calculi for induction and infinite descent	2011-12-19	Paper
Automated Cyclic Entailment Proofs in Separation Logic	2011-07-29	Paper
Craig Interpolation in Displayable Logics	2011-07-01	Paper
Classical BI: Its Semantics and Proof Theory	2010-07-27	Paper
Formalised Inductive Reasoning in the Logic of Bunched Implications	2009-03-03	Paper
Automated Reasoning with Analytic Tableaux and Related Methods	2006-07-07	Paper
A formalised first-order confluence proof for the \(\lambda\)-calculus using one-sorted variable names.	2003-08-19	Paper
https://portal.mardi4nfdi.de/entity/Q2778886	2002-03-21	Paper

Research outcomes over time

This page was built for person: James Brotherston