diff --git a/publications.bib b/publications.bib index f6261459e757a537af7d5b87f142f3ce250b3a3e..749abf8761cd241c51493267a2c5f74ed043c0a0 100644 --- a/publications.bib +++ b/publications.bib @@ -1160,12 +1160,7 @@ We have previously introduced Xdπ, a calculus for reasoning about dynamic Web d school = {Imperial College London}, year = {2007}, type = {phdthesis}, - abstract = {This thesis introduces Context Logic, a novel spatial logic which was developed to -allow local Hoare-style reasoning about tree update, but which also permits reasoning -about more general data update. Spatial logics have previously been used to describe -properties of tree-like structures (as in Ambient Logic) and to reason locally about -dynamic updates of heaps (as in Separation Logic). However, simple adaptations of -the Ambient Logic are not expressive enough to capture dynamic updates of trees. + abstract = {This thesis introduces Context Logic, a novel spatial logic which was developed to allow local Hoare-style reasoning about tree update, but which also permits reasoning about more general data update. Spatial logics have previously been used to describe properties of tree-like structures (as in Ambient Logic) and to reason locally about dynamic updates of heaps (as in Separation Logic). However, simple adaptations of the Ambient Logic are not expressive enough to capture dynamic updates of trees. Instead, one must reason explicitly about tree contexts in order to capture updates throughout the tree. For example, a typical update removes a portion of data and replaces it by inserting new data in the same place. Context Logic allows us to reason