Loading...
Please wait, while we are loading the content...
Expressive completeness of separation logic with two variables and no separating conjunction ∗.
| Content Provider | CiteSeerX |
|---|---|
| Author | Demri, Stéphane Deters, Morgan |
| Abstract | We show that first-order separation logic with one record field restricted to two variables and the separating implication (no separating conjunction) is as expressive as weak second-order logic, substantially sharpening a previous result. Capturing weak secondorder logic with such a restricted form of separation logic requires substantial updates to known proof techniques. We develop these, and as a by-product identify the smallest fragment of separation logic known to be undecidable: first-order separation logic with one record field, two variables, and no separating conjunction. |
| File Format | |
| Access Restriction | Open |
| Subject Keyword | Separation Logic Separating Conjunction Expressive Completeness First-order Separation Logic Record Field Substantial Update Proof Technique Restricted Form Weak Second-order Logic By-product Identify Separating Implication Weak Secondorder Logic Previous Result |
| Content Type | Text |
