Name
Abstract | ||
|---|---|---|
This paper proves the decidability of entailments in separation logic with monadic inductive definitions and implicit existentials. This system is obtained from the bounded-treewidth separation logic SLRDbtw of Iosif et al. in 2013 by adding implicit existential variables and restricting inductive definitions to monadic ones. The system proposed in this paper is a decidable system where one can use general recursive data structures with pointers as data, such as lists of pointers. The key idea is to reduce the problem to the decidability of SLRDbtw, by assigning local addresses or some distingu ished address to implicit existential variables so that the resulting definition clauses satisfy the establishment condition of SLRDbtw. This paper also proves the undecidability of the entailments when one adds implicit existentials to SLRDbtw. This shows that the implicit existentials are critical for the decidability. |
Year | DOI | Venue |
|---|---|---|
2015 | 10.1007/978-3-319-26529-2_5 | PROGRAMMING LANGUAGES AND SYSTEMS, APLAS 2015 |
Field | DocType | Volume |
Pointer (computer programming),Data structure,Separation logic,Programming language,Computer science,Theoretical computer science,Decidability,Monad (functional programming),Monadic predicate calculus,Recursion | Conference | 9458 |
ISSN | Citations | PageRank |
0302-9743 | 2 | 0.37 |
References | Authors | |
3 | 2 | |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Makoto Tatsuta | 1 | 111 | 22.36 |
| Daisuke Kimura | 2 | 5 | 2.14 |