@@ -24,7 +24,7 @@ We prconcurrencyesent JSCert, a formalisation of the current ECMA standard in th
Pages={474--499},
Volume={208},
Project={ concurrency, web },
Project={ TBD },
Abstract={We study adjunct-elimination results for Context Logic applied to trees, following previous results by Lozes for Separation Logic and Ambient Logic. In fact, it is not possible to prove such elimination results for the original single-holed formulation of Context Logic. Instead, we prove our results for multi-holed Context Logic.}
}
...
...
@@ -36,7 +36,7 @@ We prconcurrencyesent JSCert, a formalisation of the current ECMA standard in th
Year={2007},
Pages={255--270},
Project={ concurrency, web },
Project={ TBD },
Abstract={We study adjunct-elimination results for Context Logic applied to trees, following previous results by Lozes for Separation Logic and Ambient Logic. In fact, it is not possible to prove such elimination results for the original single-holed formulation of Context Logic. Instead, we prove our results for multi-holed Context Logic.}
}
...
...
@@ -48,7 +48,7 @@ We prconcurrencyesent JSCert, a formalisation of the current ECMA standard in th
Year={2005},
Pages={395--409},
Project={ concurrency, web },
Project={ TBD },
Abstract={Separation logic is a spatial logic for reasoning locally about heap structures. A decidable fragment of its assertion language was presented in [3], based on a bounded model property. We exploit this property to give an encoding of this fragment into a first-order logic containing only the propositional connectives, quantification over the natural numbers and equality. This result is the first translation from Separation Logic into a logic which does not depend on the heap, and provides a direct decision procedure based on well-studied algorithms for first-order logic. Moreover, our translation is compositional in the structure of formulae, whilst previous results involved enumerating either heaps or formulae arising from the bounded model property.}
}
...
...
@@ -60,7 +60,7 @@ We prconcurrencyesent JSCert, a formalisation of the current ECMA standard in th
Year={2007},
Pages={123--134},
Project={ concurrency, web },
Project={ TBD },
Abstract={Separation Logic, Ambient Logic and Context Logic are based on a similar style of reasoning about structured data. They each consist of a structural (separating) composition for reasoning about disjoint subdata, and corresponding structural adjoint(s) for reasoning hypothetically about data. We show how to interpret these structural connectives as modalities in Modal Logic and prove completeness results. The structural connectives are essential for describing properties of the underlying data, such as weakest preconditions for Hoare reasoning for Separation and Context Logic, and security properties for Ambient Logic. In fact, we introduced Context Logic to reason about tree update, precisely because the structural connectives of the Ambient Logic did not have enough expressive power. Despite these connectives being essential, first Lozes then Dawar, Gardner and Ghelli proved elimination results for Separation Logic and Ambient Logic (without quantifiers). In this paper, we solve this apparent contradiction. We study parametric inexpressivity results, which demonstrate that the structural connectives are indeed fundamental for this style of reasoning.}
}
...
...
@@ -73,7 +73,7 @@ We prconcurrencyesent JSCert, a formalisation of the current ECMA standard in th
Pages={133--175},
Volume={172},
Project={ concurrency, web },
Project={ TBD },
Abstract={We present local Hoare reasoning about data update, using Context Logic for analysing structured data. We apply our reasoning to tree update, heap update which is analogous to local Hoare reasoning using Separation Logic, and term rewriting.}
}
...
...
@@ -85,7 +85,7 @@ We prconcurrencyesent JSCert, a formalisation of the current ECMA standard in th
Year={2005},
Pages={271--282},
Project={ concurrency, web },
Project={ TBD },
Abstract={Spatial logics have been used to describe properties of tree-like structures (Ambient Logic) and in a Hoare style to reason about dynamic updates of heap-like structures (Separation Logic). We integrate this work by analysing dynamic updates to tree-like structures with pointers (such as XML with identifiers and idrefs). Naive adaptations of the Ambient Logic are not expressive enough to capture such local updates. Instead we must explicitly reason about arbitrary tree contexts in order to capture updates throughout the tree. We introduce Context Logic, study its proof theory and models, and show how it generalizes Separation Logic and its general theory BI. We use it to reason locally about a small imperative programming language for updating trees, using a Hoare logic in the style of O'Hearn, Reynolds and Yang, and show that weakest preconditions are derivable. We demonstrate the robustness of our approach by using Context Logic to capture the locality of term rewrite systems.}
}
...
...
@@ -98,7 +98,7 @@ We prconcurrencyesent JSCert, a formalisation of the current ECMA standard in th
Pages={177--201},
Volume={172},
Project={ concurrency, web },
Project={ TBD },
Abstract={We define an operational semantics and a type system for manipulating semistructured data that contains hidden information. The data model is simple labeled trees with a hiding operator. Data manipulation is based on pattern matching, with types that track the use of hidden labels.}
}
...
...
@@ -110,7 +110,7 @@ We prconcurrencyesent JSCert, a formalisation of the current ECMA standard in th
Year={2003},
Pages={216--232},
Project={ concurrency, web },
Project={ TBD },
Abstract={We define an operational semantics and a type system for manipulating semistructured data that contains hidden information. The data model is simple labeled trees with a hiding operator. Data manipulation is based on pattern matching, with types that track the use of hidden labels.}
}
...
...
@@ -122,7 +122,7 @@ We prconcurrencyesent JSCert, a formalisation of the current ECMA standard in th
Year={2002},
Pages={597--610},
Project={ web },
Project={ TBD },
Abstract={We study a spatial logic for reasoning about labelled directed graphs, and the application of this logic to provide a query language for analysing and manipulating such graphs. We give a graph description using constructs from process algebra. We introduce a spatial logic in order to reason locally about disjoint subgraphs. We extend our logic to provide a query language which preserves the multiset semantics of our graph model. Our approach contrasts with the more traditional set-based semantics found in query languages such as TQL, Strudel and GraphLog.}
}
...
...
@@ -136,7 +136,7 @@ We prconcurrencyesent JSCert, a formalisation of the current ECMA standard in th
Pages={263--310},
Volume={205},
Project={ concurrency, web },
Project={ TBD },
Abstract={We investigate the complexity and expressive power of a spatial logic for reasoning about graphs. This logic was previously introduced by Cardelli, Gardner and Ghelli, and provides the simplest setting in which to explore such results for spatial logics. We study several forms of the logic: the logic with and without recursion, and with either an exponential or a linear version of the basic composition operator. We study the combined complexity and the expressive power of the four combinations. We prove that, without recursion, the linear and exponential versions of the logic correspond to significant fragments of first-order (FO) and monadic second-order (MSO) Logics; the two versions are actually equivalent to FO and MSO on graphs representing strings. However, when the two versions are enriched with mu-style recursion, their expressive power is sharply increased.Both are able to express PSPACE-complete problems, although their combined complexity and data complexity still belong to PSPACE.}
}
...
...
@@ -148,7 +148,7 @@ We prconcurrencyesent JSCert, a formalisation of the current ECMA standard in th
Year={2004},
Pages={211--223},
Project={ concurrency, web },
Project={ TBD },
Abstract={Spatial logics are used to reason locally about disjoint data structures. They consist of standard first-order logic constructs, spatial (structural) connectives and their corresponding adjuncts. Lozes has shown that the adjuncts add no expressive power to a spatial logic for analysing tree structures, a surprising and important result. He also showed that a related logic does not have this adjunct elimination property. His proofs yield little information on the generality of adjunct elimination. We present a new proof of these results based on model-comparison games, and strengthen Lozes' results. Our proof is directed by the intuition that adjuncts can be eliminated when the corresponding moves are not useful in winning the game. The proof is modular with respect to the operators of the logic, providing a general technique for determining which combinations of operators admit adjunct elimination.}
}
...
...
@@ -185,7 +185,7 @@ In this paper, we present the 'Concurrent Views Framework', a metatheory of conc
Year={2011},
Pages={36--39},
Project={ concurrency },
Project={ TBD },
Abstract={Hoare logic ([7]) is an important tool for formally proving correctness properties of programs. It takes advantage of modularity by treating program fragments in terms of provable specifications. However, heap programs tend to break this type of modular reasoning by permitting pointer aliasing. For instance, the specification that a program reverses one list does not imply that it leaves a second list alone. To achieve this disjointness property, it is necessary to establish disjointness conditions
throughout the proof.}
...
...
@@ -198,7 +198,7 @@ throughout the proof.}
Year={2010},
Pages={199--215},
Project={ concurrency },
Project={ TBD },
Abstract={Local reasoning has become a well-established technique in program verification, which has been shown to be useful at many different levels of abstraction. In separation logic, we use a low-level abstraction that is close to how the machine sees the program state. In context logic, we work with high-level abstractions that are close to how the clients of modules see the program state. We apply program refinement to local reasoning, demonstrating that high-level local reasoning is sound for module implementations. We consider two approaches: one that preserves the high-level locality at the low level; and one that breaks the high-level`fiction' of locality.}
}
...
...
@@ -324,7 +324,7 @@ We introduce a program logic for reasoning about a broad subset of JavaScript, i
Year={2009},
Pages={178--195},
Project={ concurrency, web },
Project={ TBD },
Abstract={O'Hearn, Reynolds and Yang introduced Separation Logic to provide modular reasoning about simple, mutable data structures in memory. They were able to construct small specifications of programs, by reasoning about the local parts of memory accessed by programs. Gardner, Calcagno and Zarfaty generalised this work, introducing Context Logic to reason about more complex data structures. In particular, they developed a formal,compositional specification of the Document Object Model,a W3C XML update library. Whilst keeping to the spirit of local reasoning, they were not able to retain small specifications. We introduce Segment Logic, which provides a more fine-grained analysis of the tree structure and yields small specifications. As well as being aesthetically pleasing, small specifications are important for reasoning about concurrent tree update.}
}
...
...
@@ -336,7 +336,7 @@ We introduce a program logic for reasoning about a broad subset of JavaScript, i
Year={2007},
Pages={189--202},
Project={ concurrency, web },
Project={ TBD },
Abstract={This paper provides a gentle introduction to Context Logic. It contains work previously published with Calcagno [1,2], and is based on Gardner's notes for her course on Local Reasoning about Data Update at the Appsem PhD summer school [3] and Zarfaty's thesis [4].}
