Paper Info
Title
Elimination of spatial connectives in static spatial logics
Abstract
The recent interest for specification on resources yields so-called spatial logics, that is specification languages offering new forms of reasoning: the local reasoning through the separation of the resource space into two disjoint subspaces, and the contextual reasoning through hypothetical extension of the resource space.We consider two resource models and their related logics: •The static ambient model, proposed as an abstraction of semistructured data (Proc. ESOP'01, Lecture Notes in Computer Science, vol. 2028, Springer, Berlin, 2001, pp. 1-22 (invited paper)) with the static ambient logic (SAL) that was proposed as a request language, both obtained by restricting the mobile ambient calculus (Proc. FOSSACS'98, Lecture Notes in Computer Science, vol. 1378, Springer, Berlin, 1998, pp. 140-155) and logic (Proc. POPL'00, ACM Press, New York, 2000, pp. 365-377) to their purely static aspects. • The memory model and the assertion language of separation logic, both defined in Reynolds (Proc. LICS'02, 2002) for the purpose of the axiomatic semantic of imperative programs manipulating pointers.We raise the questions of the expressiveness and the minimality of these logics. Our main contribution is a minimalisation technique we may apply for these two logics. We moreover show some restrictions of this technique for the extension SAL∀ with universal quantification, and we establish the minimality of the adjunct-free fragment (SALint).
Year
DOI
Venue
2005
10.1016/j.tcs.2004.10.006
Theor. Comput. Sci.
Keywords
DocType
Volume
Computer Science,contextual reasoning,static ambient logic,mobile ambients,mobile ambient calculus,local reasoning,spatial connective,resource space,resource model,Lecture Notes,related logic,spatial logics,separation logic,static spatial logic,minimality.
Journal
330
Issue
ISSN
Citations 
3
Theoretical Computer Science
7
PageRank 
References 
Authors
0.56
16
1
Name
Order
Citations
PageRank
Étienne Lozes112114.32