Expressive Completeness of Separation Logic With Two Variables and No Separating Conjunction

ABSTRACT. We show that first-order separation logic restricted to two variables and to separating implication (no separating conjunction) is as expressive as weak second-order logic, substantially sharpening a previous result without such syntactic restrictions. So, two variables suffice for capturing second-order logic and we do so by using only separating implication, which requires a non-trivial update to known proof techniques. As a by-product, we identify the smallest fragment of separation logic known to be undecidable, namely first-order separation logic with one record field, two variables, and no separating conjunction.