Publications
122 results found
Dinsdale-Young T, Gardner P, Wheelhouse M, 2010, Locality refinement, Departmental Technical Report: 10/8, Publisher: Department of Computing, Imperial College London, 10/8
We study re nement in the setting of local reasoning. Inparticular, we explore general translations that preserve and that breaklocality.
Gardner P, Smith G, Wright A, 2010, Local reasoning about mashups, Departmental Technical Report: 10/10, Publisher: Department of Computing, Imperial College London, 10/10
Web mashups are complex programs that dynamically compose XML data and JavaScript code from many sources. Whereas data is sometimes formally specified by XML schema, code never is. This makes it difficult to construct reliable software. Using local Hoare reasoning, introduced in separation logic to reason about e.g. C programs and extended in context logic to reason about e.g. the DOM library, we are able to reason about mashup programs, proving that they are fault-free and providing specifications for code that are analogous to XML schema for data.
Dinsdale-Young T, Dodds M, Gardner PA, et al., 2010, Concurrent Abstract Predicates, 24th European Conference on Object-Oriented Programming (ECOOP 2010), Publisher: Springer, Pages: 504-528, ISSN: 0302-9743
Calcagno C, Dinsdale-Young T, Gardner P, 2009, Adjunct elimination in Context Logic for trees, 14th International Workshop on Logic, Language, Information and Computation, Publisher: Elsevier, Pages: 474-499, ISSN: 1090-2651
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.
Gardner P, Geerts F, 2009, Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics): Preface, ISBN: 9783642037924
Gardner PA, Wheelhouse M, 2009, Small specifications for tree update, Web Services and Formal Methods: 6th International Workshop, WS-FM 2009, Publisher: Springer Verlag, Pages: 178-195, ISSN: 0302-9743
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.
Cardelli L, Caron E, Gardner P, et al., 2009, A process model of Rho GTP-binding proteins, Conference on From Biology to Concurrency and Back, Publisher: ELSEVIER, Pages: 3166-3185, ISSN: 0304-3975
- Author Web Link
- Cite
- Citations: 14
Cardelli L, Caron E, Gardner P, et al., 2009, A Process Model of Actin Polymerisation, Electronic Notes in Theoretical Computer Science, Vol: 229, Pages: 127-144, ISSN: 1571-0661
Actin is the monomeric subunit of actin filaments which form one of the three major cytoskeletal networks in eukaryotic cells. Actin dynamics, be it the polymerisation of actin monomers into filaments or the reverse process, plays a key role in many cellular activities such as cell motility and phagocytosis. There is a growing number of experimental, theoretical and mathematical studies on the components of actin polymerisation and depolymerisation. However, it remains a challenge to develop compositional models of actin dynamics, e.g., by using differential equations. In this paper, we propose compositional process algebra models of actin polymerisation, and present a geometric representation of these models that allows to generate movies reflecting their dynamics. © 2009 Elsevier B.V. All rights reserved.
Gardner P, Zarfaty U, 2009, Reasoning about high-level tree update and its low-level implementation, Departmental Technical Report: 09/9, Publisher: Department of Computing, Imperial College London, 09/9
We relate Context Logic reasoning about a high-leveltree update language with Separation Logic reasoningabout a low-level implementation.
Raza M, Gardner P, 2009, Footprints in local reasoning, 11th International Conference on Foundations of Software Science and Computational Structures, Publisher: Logical Methods in Computer Science e.V., ISSN: 1860-5974
Local reasoning about programs exploits the natural local behaviour common in programs by focussing on the footprint - that part of the resource accessed by the program. We address the problem of formally characterising and analysing the footprint notion for abstract local functions introduced by Calcagno, O Hearn and Yang. With our definition, we prove that the footprints are the only essential elements required for a complete specification of a local function. We formalise the notion of small specifications in local reasoning and show that for well-founded resource models, a smallest specification always exists that only includes the footprints, and also present results for the non-well-founded case. Finally, we use this theory of footprints to investigate the conditions under which the footprints correspond to the smallest safe states. We present a new model of RAM in which, unlike the standard model, the footprints of every program correspond to the smallest safe states, and we also identify a general condition on the primitive commands of a programming language which guarantees this property for arbitrary models.
Gardner P, Zarfaty U, 2009, Reasoning about High-Level Tree Update and its Low-Level Implementation
We relate Context Logic reasoning about a high-leveltree update language with Separation Logic reasoningabout a low-level implementation.
Cardelli L, Gardner P, 2009, Processes in space, Departmental Technical Report: 09/4, Publisher: Department of Computing, Imperial College London, 09/4
We introduce a geometric process algebra based on affine geometry,with the aim of describing the concurrent evolution of geometric structures in3D space. We prove a relativity theorem stating that algebraic equations are invariantunder rigid body transformations.
Raza M, Calcagno C, Gardner P, 2009, Automatic Parallelization with Separation Logic, 15th International Conference on Tools and Algorithms for the Construction and Analysis of Systems held at Joint European Conferences on Theory and Practice of Software, Publisher: SPRINGER-VERLAG BERLIN, Pages: 348-362, ISSN: 0302-9743
- Author Web Link
- Open Access Link
- Cite
- Citations: 17
Maffeis S, Gardner P, 2008, Behavioural equivalences for dynamic web data, JOURNAL OF LOGIC AND ALGEBRAIC PROGRAMMING, Vol: 75, Pages: 86-138, ISSN: 1567-8326
Cardelli L, Gardner P, Kahramanoǧullari O, 2008, A Process Model of Rho GTP-binding Proteins in the Context of Phagocytosis, Electronic Notes in Theoretical Computer Science, Vol: 194, Pages: 87-102, ISSN: 1571-0661
At the early stages of the phagocytic signalling, Rho GTP-binding proteins play a key role. With the stimulus from the cell membrane and with the help from the regulators (GEF, GAP, Effector, GDI), these proteins serve as switches that interact with their environment in a complex manner. We present a generic process model for the Rho GTP-binding proteins, and compare it with a previous model that uses ordinary differential equations. We then extend the basic model to include the behaviour of the GDIs. We discuss the challenges this extension brings and directions of further research. © 2008 Elsevier B.V. All rights reserved.
Gardner PA, Smith G, Wheelhouse M, et al., 2008, DOM: Towards a Formal Specification, ACM SIGPLAN Workshop ACM SIGPLAN Workshop on Programming Language Technologies for XML (PLAN-X)
The W3C Document Object Model (DOM) specifies an XML update library. DOM is written in English, and is therefore not compositional and not complete. We provide a first step towards a compositional specification of DOM. Unlike DOM, we are able to workwith a minimal set of commands and obtain a complete reasoning for straight-line code. Our work transfers O’Hearn, Reynoldsand Yang’s local Hoare reasoning for analysing heaps to XML,viewing XML as an in-place memory store as does DOM. In particular, we apply recent work by Calcagno, Gardner and Zarfatyon local Hoare reasoning about a simple tree-update language toDOM, showing that our reasoning scales to DOM. Our reasoningnot only formally specifies a significant subset of DOM Core Level1, but can also be used to verify e.g. invariant properties of simpleJavascript programs.
Raza M, Calcagno C, Gardner P, 2008, Automatic parallelization with separation logic, Departmental Technical Report: 08/16, Publisher: Department of Computing, Imperial College London, 08/16
Separation logic is a recent approach to the analysis of pointer programsin which resource separation is expressed with a logical connective in assertionsthat describe the state at any given point in the program. We extend thisapproach to express properties of memory separation between different points inthe program, and present an algorithm for determining independences betweenprogram statements which can be used for parallelization.
Gardner PA, Smith G, Wheelhouse M, et al., 2008, Local Hoare Reasoning about DOM, 27th ACM SIGMOD-SIGACT-SIGART Symposium on Principles of Database Systems (PODS 2008), Publisher: ACM, Pages: 261-270
Raza M, Gardner P, 2008, Footprints in local reasoning, 11th International Conference on Foundations of Software Science and Computational Structures, Publisher: SPRINGER-VERLAG BERLIN, Pages: 201-215, ISSN: 0302-9743
- Author Web Link
- Open Access Link
- Cite
- Citations: 1
Cardelli L, Gardner P, Ghelli G, 2007, Manipulating trees with hidden labels, Electronic Notes in Theoretical Computer Science, Vol: 172, Pages: 177-201, ISSN: 1571-0661
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.
Calcagno C, Gardner P, Zarfaty U, 2007, Local Reasoning about Data Update, Electronic Notes in Theoretical Computer Science, Vol: 172, Pages: 133-175, ISSN: 1571-0661
We present local Hoare reasoning about data update, introducing Context Logic for analysing structured data. We apply our reasoning to tree update, heap update, and term rewriting. Our reasoning about heap update is exactly analogous to the local Hoare reasoning of Separation Logic. Our reasoning about tree update and term rewriting can only be done with Context Logic. © 2007 Elsevier B.V. All rights reserved.
Calcagno C, Gardner P, Zarfaty U, 2007, Context logic as modal logic: Completeness and parametric, Pages: 123-134, ISSN: 1523-2867
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. Copyright © 2007 ACM.
Gardner P, Zarfaty U, 2007, An introduction to context logic, 14th International Workshop on Logic, Language, Information and Computation, Publisher: SPRINGER-VERLAG BERLIN, Pages: 189-+, ISSN: 0302-9743
- Author Web Link
- Cite
- Citations: 3
Gardner P, Laneve C, Wischik L, 2007, Linear Forwarders, Journal of Information and Computation
Calcagno C, Dinsdale-Young T, Gardner P, 2007, Adjunct elimination in Context Logic for trees, 5th Asian Symposium on Programming Languages and Systems, Publisher: SPRINGER-VERLAG BERLIN, Pages: 255-270, ISSN: 0302-9743
- Author Web Link
- Open Access Link
- Cite
- Citations: 3
Calcagno C, Gardner P, Zarfaty U, 2007, Context Logic as Modal Logic: Completeness and Parametric Inexpressivity, 34th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Publisher: ASSOC COMPUTING MACHINERY, Pages: 123-134
- Author Web Link
- Cite
- Citations: 11
Calcagno C, Gardner P, Zarfaty U, 2007, Context logic as modal logic: completeness and parametric inexpressivity, Symposium on Principles of Programming Languages, Pages: 123-134, ISSN: 0362-1340
Gardner P, Yoshida N, 2006, Concurrency theory - (CONCUR 2004), THEORETICAL COMPUTER SCIENCE, Vol: 358, Pages: 149-149, ISSN: 0304-3975
Zarfaty U, Gardner P, 2006, Local reasoning about tree update, ENTCS, Vol: 158, Pages: 399-424, ISSN: 1571-0661
This data is extracted from the Web of Science and reproduced under a licence from Thomson Reuters. You may not copy or re-distribute this data in whole or in part without the written consent of the Science business of Thomson Reuters.