This description was written by a machine and published without a person checking it. It is what the agent made of this grouping, and not a statement anybody has stood behind.
James Brotherston
A grouping.
James Brotherston: the undecidability of propositional separation logic with inductive definitions, the result the decidability literature works around, plus decidable fragments (inductive predicates, arrays) and cyclic termination proofs.
6 references
Biabduction (and Related Problems) in Array Separation Logic
James Brotherston and others (2017) · Automated Deduction – CADE 26 · Springer
Sub-classical Boolean Bunched Logics and the Meaning of Par
James Brotherston and others (2015) · Stephan Kreutzer, editor: Conference on Computer Science Logic (CSL 2015), Leibniz International Proceedings in Informatics (LIPIcs) 41, Schloss Dagstuhl– Leibniz-Zentrum fuer Informatik
A Decision Procedure for Satisfiability in Separation Logic with Inductive Definitions
James Brotherston and others (2014) · Proceedings of the Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS) · Association for Computing Machinery
Classical BI: Its Semantics and Proof Theory
James Brotherston and others (2010) · Centre pour la Communication Scientifique Directe (CCSD)
Undecidability of propositional separation logic and its neighbours
James Brotherston and others (2010) · 25th IEEE Symposium on Logic in Computer Science (LICS) · IEEE
Cyclic proofs of program termination in separation logic
James Brotherston and others (2008) · ACM SIGPLAN Notices