James Brotherston

A grouping.

The boundary the separation-logic decidability literature works inside: the undecidability of propositional separation logic with inductive definitions is the negative result that makes the rest of that literature about fragments rather than about the logic. Two further records find fragments where decision is possible, in satisfiability with inductive predicates and in array separation logic; a fourth is about program termination rather than decidability.