From 689933b01007d2cda2d222d90048e346c4dca678 Mon Sep 17 00:00:00 2001
From: Thomas Wood <thomas.wood09@imperial.ac.uk>
Date: Wed, 3 Feb 2016 18:36:37 +0000
Subject: [PATCH] Reindex/reformat publications.bib using jabref
---
publications.bib | 1227 ++++++++++++++++++++++++----------------------
1 file changed, 637 insertions(+), 590 deletions(-)
diff --git a/publications.bib b/publications.bib
index 85709f7..879fc26 100644
--- a/publications.bib
+++ b/publications.bib
@@ -1,596 +1,643 @@
-%San Francisco, CA, USA
-@InProceedings{gardner:cav:2015,
- Title = {{A Trusted Mechanised Specification of JavaScript: One Year On}},
- Author = {Philippa Gardner and Gareth Smith and Conrad Watt and Thomas Wood},
- Booktitle = {Proceedings of the 27\textsuperscript{th} International Conference on Computer Aided Verification ({CAV})},
- Year = {2015},
- Pages = {3--10},
- abstract = {The JSCert project provides a Coq mechanised specification of the core JavaScript language. A key part of the project was to develop a methodology for establishing trust, by designing JSCert in such a way as to provide a strong connection with the JavaScript standard, and by developing JSRef, a reference interpreter which was proved correct with respect to JSCert and tested using the standard Test262 test suite. In this paper, we assess the previous state of the project at POPL?14 and the current state of the project at CAV?15. We evaluate the work of POPL?14, providing an analysis of the methodology as a whole and a more detailed analysis of the tests. We also describe recent work on extending JSRef to include Google?s V8 Array library, enabling us to cover more of the language and to pass more tests.}
-}
-
-@inproceedings{rochapinto:mpfs:2015,
- title = {{Steps in Modular Specifications for Concurrent Modules}},
- author = {Pedro da Rocha Pinto and Thomas Dinsdale-Young and Philippa Gardner},
- booktitle = {Proceedings of the 31\textsuperscript{st} Conference on the Mathematical Foundations of Programming Semantics},
- year = {2015},
- abstract = {The specification of a concurrent program module is a difficult problem. The specifications must be strong enough to enable reasoning about the intended clients without reference to the underlying module implementation. We survey a range of verification techniques for specifying concurrent modules, in particular highlighting four key concepts: auxiliary state, interference abstraction, resource ownership and atomicity. We show how these concepts combine to provide powerful approaches to specifying concurrent modules.},
-}
-
-@InProceedings{gardner:edbticdt:2010,
- Title = {{Reasoning About Client-side Web Programs: Invited Talk}},
- Author = {Philippa Gardner},
- Booktitle = {Proceedings of the 2010 {EDBT/ICDT} Workshops, Lausanne, Switzerland, March 22-26, 2010},
- Year = {2010},
- abstract = {In PODS 2008, I presented a paper on a formal, compositional specification of the Document Object Model (DOM), a W3C XML Update library. This work concentrated on Featherweight DOM, a small fragment of DOM which focuses on the XML tree structure and simple text nodes. Since the formal reasoning is compositional, we are able to work with a minimal set of commands and obtain complete reasoning for straight-line code. We are also able to verify, for example, invariant properties of simple DOM programs. This work is based on a recent breakthrough in program verification, based on analysing a program's use of resource. The idea is that the reasoning should follow the programmers' intuitions about which part of the computer memory the program touches. This style of reasoning was introduced by O'Hearn (Queen Mary) and Reynolds (CMU) in their work on Separation Logic for reasoning modularly about large C-programs (e.g. Microsoft device driver code, Linux). I substantially extended the range of local resource reasoning, introducing Context Logic to reason about programs that directly manipulate complex data structures such as XML. In this survey talk, I will give an overview of our theoretical and practical work on reasoning about DOM, highlighting recent developments which include: 1. the extension of this work to DOM Core Level 1. A substantial piece of work, not because of the reasoning, but because full DOM is large, underspecified and difficult to interpret, with no consensus between browsers; 2. reasoning about the combination of JavaScript and DOM to provide, for example, secure mashups for a more flexible, secure integration of outsourced payment services; 3. on-going work on a verification tool for automatically reasoning about DOM programs and the identification of key examples of web applications on which to test our DOM reasoning: e.g., with current technology, we can prove by hand that mashup programs are fault free; with our tool, such proofs will be automatic. An ultimate challenge is to develop the necessary reasoning technology to provide a safe and secure web environment on which to build the next generation of web applications, thus demonstrating the scientific feasibility of a reliable Web.},
-}
-
-%Rio de Janeiro, Brazil
-@InProceedings{gardner:wollic:2007,
- Title = {{An Introduction to Context Logic}},
- Author = {Philippa Gardner and Uri Zarfaty},
- Booktitle = {Proceedings of the 14\textsuperscript{th} International Workshop on Logic, Language, Information and Computation (WoLLIC)},
- Year = {2007},
- Pages = {189--202},
- 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].}
-}
-
-
-@InProceedings{dinsdaleyoung:calco:2011,
- Title = {{Abstract Local Reasoning for Program Modules}},
- Author = {Thomas Dinsdale{-}Young and Philippa Gardner and Mark J. Wheelhouse},
- Booktitle = {Proceedings of the 4\textsuperscript{th} International Conference on Algebra and Coalgebra in Computer Science ({CALCO})},
- Year = {2011},
- Pages = {36--39},
- 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
+% This file was created with JabRef 2.10.
+% Encoding: UTF8
+
+
+@InProceedings{Barber1997From,
+ Title = {{From Action Calculi to Linear Logic}},
+ Author = {Andrew Barber and Philippa Gardner and Masahito Hasegawa and Gordon D. Plotkin},
+ Booktitle = {Proceedings of the 11\textsuperscript{th} International Workshop on Computer Science Logic {CSL}},
+ Year = {1997},
+ Pages = {78--97},
+
+ Abstract = {Milner introduced action calculi as a framework for investigating models of interactive behaviour. We present a type-theoretic account of action calculi using the propositions-as-types paradigm; the type theory has a sound and complete interpretation in Power?s categorical models. We go on to give a sound translation of our type theory in the (type theory of) intuitionistic linear logic, corresponding to the relation between Benton?s models of linear logic and models of action calculi. The conservativity of the syntactic translation is proved by a model-embedding construction using the Yoneda lemma. Finally, we briefly discuss how these techniques can also be used to give conservative translations between various extensions of action calculi.}
+}
+
+@InProceedings{Bodin2014Trusted,
+ Title = {{A Trusted Mechanised {JavaScript} Specification}},
+ Author = {Martin Bodin and Arthur Chargu{\'{e}}raud and Daniele Filaretti and Philippa Gardner and Sergio Maffeis and Daiva Naud\v{z}i\={u}nien\.{e} and Alan Schmitt and Gareth Smith},
+ Booktitle = {Proceedings of the 41\textsuperscript{st} Annual {ACM} {SIGPLAN-SIGACT} Symposium on Principles of Programming Languages ({POPL})},
+ Year = {2014},
+ Pages = {87--100},
+
+ Abstract = {JavaScript is the most widely used web language for client-side applications. Whilst the development of JavaScript was initially just led by implementation, there is now increasing momentum behind the ECMA standardisation process. The time is ripe for a formal, mechanised specification of JavaScript, to clarify ambiguities in the ECMA standards, to serve as a trusted reference for high-level language compilation and JavaScript implementations, and to provide a platform for high-assurance proofs of language properties.
+We present JSCert, a formalisation of the current ECMA standard in the Coq proof assistant, and JSRef, a reference interpreter for JavaScript extracted from Coq to OCaml. We give a Coq proof that JSRef is correct with respect to JSCert and assess JSRef using test262, the ECMA conformance test suite. Our methodology ensures that JSCert is a comparatively accurate formulation of the English standard, which will only improve as time goes on. We have demonstrated that modern techniques of mechanised specification can handle the complexity of JavaScript.}
+}
+
+@Article{Calcagno2010Adjunct,
+ Title = {{Adjunct elimination in Context Logic for Trees}},
+ Author = {Cristiano Calcagno and Thomas Dinsdale{-}Young and Philippa Gardner},
+ Journal = {Information and Computation},
+ Year = {2010},
+ Number = {5},
+ Pages = {474--499},
+ Volume = {208},
+
+ 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.}
+}
+
+@InProceedings{Calcagno2007Adjunct,
+ Title = {{Adjunct Elimination in Context Logic for Trees}},
+ Author = {Cristiano Calcagno and Thomas Dinsdale{-}Young and Philippa Gardner},
+ Booktitle = {Proceedings of the 5\textsuperscript{th} Asian Symposium on Programming Languages and Systems ({APLAS})},
+ Year = {2007},
+ Pages = {255--270},
+
+ 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.}
+}
+
+@InProceedings{Calcagno2005From,
+ Title = {{From Separation Logic to First-Order Logic}},
+ Author = {Cristiano Calcagno and Philippa Gardner and Matthew Hague},
+ Booktitle = {Proceedings of the 8\textsuperscript{th} International Conference on Foundations of Software Science and Computational Structures ({FOSSACS})},
+ Year = {2005},
+ Pages = {395--409},
+
+ 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.}
+}
+
+@InProceedings{Calcagno2007Context,
+ Title = {{Context Logic as Modal Logic: Completeness and Parametric Inexpressivity}},
+ Author = {Cristiano Calcagno and Philippa Gardner and Uri Zarfaty},
+ Booktitle = {Proceedings of the 34\textsuperscript{th} {ACM} {SIGPLAN-SIGACT} Symposium on Principles of Programming Languages ({POPL})},
+ Year = {2007},
+ Pages = {123--134},
+
+ 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 dis- joint subdata, and corresponding structural adjoint(s) for reasoning hypothetically about data. We show how to interpret these struc- tural connectives as modalities in Modal Logic and prove complete- ness 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.}
+}
+
+@Article{Calcagno2007Local,
+ Title = {{Local Reasoning about Data Update}},
+ Author = {Cristiano Calcagno and Philippa Gardner and Uri Zarfaty},
+ Journal = {Electronic Notes on Theoretical Computer Science},
+ Year = {2007},
+ Pages = {133--175},
+ Volume = {172},
+
+ 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.}
+}
+
+@InProceedings{Calcagno2005Context,
+ Title = {{Context Logic and Tree Update}},
+ Author = {Cristiano Calcagno and Philippa Gardner and Uri Zarfaty},
+ Booktitle = {Proceedings of the 32\textsuperscript{nd} {ACM} {SIGPLAN-SIGACT} Symposium on Principles of Programming Languages ({POPL})},
+ Year = {2005},
+ Pages = {271--282},
+
+ 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.}
+}
+
+@Article{Cardelli2009Process,
+ Title = {{A Process Model of Actin Polymerisation}},
+ Author = {Luca Cardelli and Emmanuelle Caron and Philippa Gardner and Ozan Kahramanogullari and Andrew Phillips},
+ Journal = {Electronic Notes in Theoretical Computer Science},
+ Year = {2009},
+ Number = {1},
+ Pages = {127--144},
+ Volume = {229},
+
+ Abstract = {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.}
+}
+
+@Article{Cardelli2009Processa,
+ Title = {{A Process Model of Rho GTP-binding Proteins}},
+ Author = {Luca Cardelli and Emmanuelle Caron and Philippa Gardner and Ozan Kahramanogullari and Andrew Phillips},
+ Journal = {Theoretical Computer Science},
+ Year = {2009},
+ Number = {33-34},
+ Pages = {3166--3185},
+ Volume = {410},
+
+ Abstract = {Rho GTP-binding proteins play a key role as molecular switches in many cellular activities. In response to extracellular stimuli and with the help from regulators (GEF, GAP, Effector, GDI), these proteins serve as switches that interact with their environment in a complex manner. Based on the structure of a published ordinary differential equations (ODE) model, we first present a generic process model for the Rho GTP- binding proteins, and compare it with the ODE model. We then extend the basic model to include the behaviour of the GDIs and explore the parameter space for the extended model with respect to biological data from the literature. We discuss the challenges this extension brings and the directions of further research. In particular, we present techniques for modular representation and refinement of process models, where, for example, different Rho proteins with different rates for regulator interactions can be given as the instances of the same parametric model.}
+}
+
+@Article{Cardelli2012Processes,
+ Title = {{Processes in Space}},
+ Author = {Luca Cardelli and Philippa Gardner},
+ Journal = {Theoretical Computer Science},
+ Year = {2012},
+ Pages = {40--55},
+ Volume = {431},
+
+ Abstract = {We introduce a geometric process algebra based on affine geometry, with the aim of describing the concurrent evolution of geometric structures in 3D space. We prove a relativity theorem stating that algebraic equations are invariant under rigid body transformations.}
+}
+
+@InProceedings{Cardelli2010Processes,
+ Title = {Processes in Space},
+ Author = {Luca Cardelli and Philippa Gardner},
+ Booktitle = {Proceedings of the 6\textsuperscript{th} Conference on Computability in Europe {CiE} - Programs, Proofs, Processes},
+ Year = {2010},
+ Pages = {78--87},
+
+ Abstract = {We introduce a geometric process algebra based on affine geometry, with the aim of describing the concurrent evolution of geometric structures in 3D space. We prove a relativity theorem stating that algebraic equations are invariant under rigid body transformations.}
+}
+
+@Article{Cardelli2007Manipulating,
+ Title = {{Manipulating Trees with Hidden Labels}},
+ Author = {Luca Cardelli and Philippa Gardner and Giorgio Ghelli},
+ Journal = {Electronic Notes in Theoretical Computer Science},
+ Year = {2007},
+ Pages = {177--201},
+ Volume = {172},
+
+ Abstract = {We define an operational semantics and a type system for manipulat- ing semistructured data that contains hidden information. The data model is sim- ple labeled trees with a hiding operator. Data manipulation is based on pattern matching, with types that track the use of hidden labels.}
+}
+
+@InProceedings{Cardelli2003Manipulating,
+ Title = {{Manipulating Trees with Hidden Labels}},
+ Author = {Luca Cardelli and Philippa Gardner and Giorgio Ghelli},
+ Booktitle = {Proceedings of the 6\textsuperscript{th} International Conference on Foundations of Software Science and Computational Structures ({FOSSACS})},
+ Year = {2003},
+ Pages = {216--232},
+
+ Abstract = {We define an operational semantics and a type system for manipulat- ing semistructured data that contains hidden information. The data model is sim- ple labeled trees with a hiding operator. Data manipulation is based on pattern matching, with types that track the use of hidden labels.}
+}
+
+@InProceedings{Cardelli2002Spatial,
+ Title = {{A Spatial Logic for Querying Graphs}},
+ Author = {Luca Cardelli and Philippa Gardner and Giorgio Ghelli},
+ Booktitle = {Proceedings of the 29\textsuperscript{th} International Colloquium on Automata, Languages and Programming ({ICALP})},
+ Year = {2002},
+ Pages = {597--610},
+
+ 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.}
+}
+
+@Article{Cardelli2008Process,
+ Title = {{A Process Model of Rho GTP-binding Proteins in the Context of Phagocytosis}},
+ Author = {Luca Cardelli and Philippa Gardner and Ozan Kahramanogullari},
+ Journal = {Electronic Notes in Theoretical Computer Science},
+ Year = {2008},
+ Number = {3},
+ Pages = {87--102},
+ Volume = {194},
+
+ Abstract = {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.}
+}
+
+@Article{Dawar2007Expressiveness,
+ Title = {{Expressiveness and Complexity of Graph Logic}},
+ Author = {Anuj Dawar and Philippa Gardner and Giorgio Ghelli},
+ Journal = {Information and Computation},
+ Year = {2007},
+ Number = {3},
+ Pages = {263--310},
+ Volume = {205},
+
+ 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 ?-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.}
+}
+
+@InProceedings{Dawar2004Adjunct,
+ Title = {{Adjunct Elimination Through Games in Static Ambient Logic}},
+ Author = {Anuj Dawar and Philippa Gardner and Giorgio Ghelli},
+ Booktitle = {Proceedings of the 24\textsuperscript{th} International Conference on Foundations of Software Technology and Theoretical Computer Science ({FSTTCS})},
+ Year = {2004},
+ Pages = {211--223},
+
+ 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.}
+}
+
+@InProceedings{Dinsdale-Young2013Views,
+ Title = {{Views: Compositional Reasoning for Concurrent Programs}},
+ Author = {Thomas Dinsdale{-}Young and Lars Birkedal and Philippa Gardner and Matthew J. Parkinson and Hongseok Yang},
+ Booktitle = {Proceedings of the 40\textsuperscript{th} Annual {ACM} {SIGPLAN-SIGACT} Symposium on Principles of Programming Languages ({POPL})},
+ Year = {2013},
+ Pages = {287--300},
+
+ Abstract = {Compositional abstractions underly many reasoning principles for concurrent programs: the concurrent environment is abstracted in order to reason about a thread in isolation; and these abstractions are composed to reason about a program consisting of many threads. For instance, separation logic uses formulae that describe part of the state, abstracting the rest; when two threads use disjoint state, their specifications can be composed with the separating con- junction. Type systems abstract the state to the types of variables; threads may be composed when they agree on the types of shared variables.
+In this paper, we present the ?Concurrent Views Framework?, a metatheory of concurrent reasoning principles. The theory is parameterised by an abstraction of state with a notion of composition, which we call views. The metatheory is remarkably simple, but highly applicable: the rely-guarantee method, concurrent separation logic, concurrent abstract predicates, type systems for recursive references and for unique pointers, and even an adaptation of the Owicki-Gries method can all be seen as instances of the Con- current Views Framework. Moreover, our metatheory proves each of these systems is sound without requiring induction on the operational semantics.}
+}
+
+@InProceedings{Dinsdale-Young2010Concurrent,
+ Title = {{Concurrent Abstract Predicates}},
+ Author = {Thomas Dinsdale{-}Young and Mike Dodds and Philippa Gardner and Matthew J. Parkinson and Viktor Vafeiadis},
+ Booktitle = {Proceedings of the 24\textsuperscript{th} European Conference on Object-Oriented Programming ({ECOOP})},
+ Year = {2010},
+ Pages = {504--528},
+
+ Abstract = {Abstraction is key to understanding and reasoning about large computer systems. Abstraction is simple to achieve if the relevant data structures are disjoint, but rather difficult when they are partially shared, as is often the case for concurrent modules. We present a pro- gram logic for reasoning abstractly about data structures that provides a fiction of disjointness and permits compositional reasoning. The internal details of a module are completely hidden from the client by concurrent abstract predicates. We reason about a module?s implementation using separation logic with permissions, and provide abstract specifications for use by client programs using concurrent abstract predicates. We illustrate our abstract reasoning by building two implementations of a lock module on top of hardware instructions, and two implementations of a concurrent set module on top of the lock module.}
+}
+
+@InProceedings{Dinsdale-Young2011Abstract,
+ Title = {{Abstract Local Reasoning for Program Modules}},
+ Author = {Thomas Dinsdale{-}Young and Philippa Gardner and Mark J. Wheelhouse},
+ Booktitle = {Proceedings of the 4\textsuperscript{th} International Conference on Algebra and Coalgebra in Computer Science ({CALCO})},
+ Year = {2011},
+ Pages = {36--39},
+
+ 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.}
}
-@inproceedings{Total-TaDA,
- author = {Pedro da Rocha Pinto and Thomas Dinsdale-Young and Philippa Gardner and Julian Sutherland},
- title = {Modular Termination Verification for Non-blocking Concurrency},
- booktitle = {Proceedings of the 25\textsuperscript{th} European Symposium on Programming ({ESOP})},
- year = {2016},
- abstract = {We present Total-TaDA, a program logic for verifying the total correctness of concurrent programs: that such programs both terminate and produce the correct result. With Total-TaDA, we can specify constraints on a thread?s concurrent environment that are necessary to guarantee termination. This allows us to verify total correctness for non-blocking algorithms, e.g. a counter and a stack. Our specifications can express lock- and wait-freedom. More generally, they can express that one operation cannot impede the progress of another, a new non-blocking property we call non-impedance. Moreover, our approach is modular. We can verify the operations of a module independently, and build up modules on top of each other.},
-}
-
-@InProceedings{ntzik:oopsla:2015,
- author = {Gian Ntzik and Philippa Gardner},
- title = {{\textit{Reasoning about the POSIX File System: Local Update and Global Pathnames}}},
- Booktitle = {Proceedings of the 30\textsuperscript{th} Annual {ACM} {SIGPLAN} Conference on Object-Oriented Programming, Systems, Languages, and Applications ({OOPSLA})},
- year = {2015},
- note = {(Awaiting Publication)},
- abstract = {We introduce a program logic for specifying a core sequential subset of the POSIX file system and for reasoning abstractly about client programs working with the file system. The challenge is to reason about the combination of local directory update and global pathname traversal (including ?..? and symbolic links) which may overlap the directories be- ing updated. Existing reasoning techniques are either based on first-order logic and do not scale, or on separation logic and can only handle linear pathnames (no ?..? or symbolic links). We introduce fusion logic for reasoning about local update and global pathname traversal, introducing a novel effect frame rule to propagate the effect of a local update on overlapping pathnames. We apply our reasoning to the standard recursive remove utility (rm -r), discovering bugs in well-known implementations.},
-}
-
-@InProceedings{ntzik:aplas:2015,
- author = {Gian Ntzik and Pedro da Rocha Pinto and Philippa Gardner},
- title = {{\em Fault-tolerant Resource Reasoning}},
- Booktitle = {Proceedings of the 13\textsuperscript{th} Asian Symposium on Programming Languages and Systems ({APLAS})},
- year = {2015},
- note = {(Awaiting Publication)$^*$},
- abstract = {Separation logic has been successful at verifying that pro- grams do not crash due to illegal use of resources. The underlying assumption, however, is that machines do not fail. In practice, machines can fail unpredictably for various reasons, e.g. power loss, corrupting resources. Critical software, e.g. file systems, employ recovery methods to mitigate these effects. We introduce an extension of the Views framework to reason about such methods. We use concurrent separation logic as an instance of the framework to illustrate our reasoning, and explore programs using write-ahead logging, e.g. an ARIES recovery algorithm.},
-}
-
-%Programming Languages and Systems
-@InProceedings{raad:esop:2015,
- Title = {{CoLoSL: Concurrent Local Subjective Logic}},
- Author = {Azalea Raad and Jules Villard and Philippa Gardner},
- Booktitle = {Proceedings of the 24\textsuperscript{th} European Symposium on Programming ({ESOP})},
- Year = {2015},
- Pages = {710--735},
- abstract = {A key difficulty in verifying shared-memory concurrent pro- grams is reasoning compositionally about each thread in isolation. Existing verification techniques for fine-grained concurrency typically require reasoning about either the entire shared state or disjoint parts of the shared state, impeding compositionality. This paper introduces the program logic CoLoSL, where each thread is verified with respect to its subjective view of the global shared state. This subjective view describes only that part of the state accessed by the thread. Subjective views may arbitrarily overlap with each other, and expand and contract depending on the resource required by the thread. This flexibility gives rise to small specifications and, hence, more compositional reasoning for concurrent programs. We demonstrate our reasoning on a range of examples, including a concurrent computation of a spanning tree of a graph.},
-}
-
-@Article{gardner:mfps:2014,
- Title = {{Abstract Local Reasoning for Concurrent Libraries: Mind the Gap}},
- Author = {Philippa Gardner and Azalea Raad and Mark J. Wheelhouse and Adam Wright},
- Journal = {Proceedings of the 30\textsuperscript{th} Conference on the Mathematical Foundations of Programming Semantics ({MFPS})},
- Year = {2014},
- Pages = {147--166},
- Volume = {308},
- abstract = {We study abstract local reasoning for concurrent libraries. There are two main approaches: provide a specification of a library by abstracting from concrete reasoning about an implementation; or provide a direct abstract library specification, justified by refining to an implementation. Both approaches have a significant gap in their reasoning, due to a mismatch between the abstract connectivity of the abstract data structures and the concrete connectivity of the concrete heap representations. We demonstrate this gap using structural separation logic (SSL) for specifying a concurrent tree library and concurrent abstract predicates (CAP) for reasoning about a concrete tree implementation. The gap between the abstract and concrete connectivity emerges as a mismatch between the SSL tree predicates and CAP heap predicates. This gap is closed by an interface function I which links the abstract and concrete connectivity. In the accompanying technical report, we generalise our SSL reasoning and results to arbitrary concurrent data libraries.},
-}
-
-@InProceedings{rochapinto:ecoop:2014,
- Title = {{\em TaDA: A Logic for Time and Data Abstraction}},
- Author = {Pedro da Rocha Pinto and Thomas Dinsdale{-}Young and Philippa Gardner},
- Booktitle = {Proceedings of the 28\textsuperscript{th} European Conference on Object-Oriented Programming ({ECOOP})},
- Year = {2014},
- Pages = {207--231},
- abstract = {To avoid data races, concurrent operations should either be at distinct times or on distinct data. Atomicity is the abstraction that an operation takes effect at a single, discrete instant in time, with linearisability being a well-known correctness condition which asserts that concurrent operations appear to behave atomically. Disjointness is the abstraction that operations act on distinct data resource, with concur- rent separation logics enabling reasoning about threads that appear to operate independently on disjoint resources.
Building on separation logic with concurrent abstract predicates (CAP), we introduce TaDA, a program logic which combines the benefits of abstract atomicity and abstract disjointness. We give several examples: an atomic lock module, a CAP example with a twist, which cannot be done using linearisability; an atomic MCAS module implemented using our lock module, a classic linearisability example which cannot be done us- ing CAP; and a double-ended queue module implemented using MCAS.},
-}
-
-@InProceedings{bodin:popl:2014,
- Title = {{\em A Trusted Mechanised {JavaScript} Specification}},
- Author = {Martin Bodin and Arthur Chargu{\'{e}}raud and Daniele Filaretti and Philippa Gardner and Sergio Maffeis and Daiva Naud\v{z}i\={u}nien\.{e} and Alan Schmitt and Gareth Smith},
- Booktitle = {Proceedings of the 41\textsuperscript{st} Annual {ACM} {SIGPLAN-SIGACT} Symposium on Principles of Programming Languages ({POPL})},
- Year = {2014},
- Pages = {87--100},
- abstract = {JavaScript is the most widely used web language for client-side applications. Whilst the development of JavaScript was initially just led by implementation, there is now increasing momentum behind the ECMA standardisation process. The time is ripe for a formal, mechanised specification of JavaScript, to clarify ambiguities in the ECMA standards, to serve as a trusted reference for high-level language compilation and JavaScript implementations, and to provide a platform for high-assurance proofs of language properties.
We present JSCert, a formalisation of the current ECMA standard in the Coq proof assistant, and JSRef, a reference interpreter for JavaScript extracted from Coq to OCaml. We give a Coq proof that JSRef is correct with respect to JSCert and assess JSRef using test262, the ECMA conformance test suite. Our methodology ensures that JSCert is a comparatively accurate formulation of the English standard, which will only improve as time goes on. We have demonstrated that modern techniques of mechanised specification can handle the complexity of JavaScript.},
-}
-
-%Programming Languages and Systems -
-@InProceedings{ntzik:esop:2014,
- Title = {{Local Reasoning for the {POSIX} File System}},
- Author = {Philippa Gardner and Gian Ntzik and Adam Wright},
- Booktitle = {Proceedings of the 23\textsuperscript{rd} European Symposium on Programming ({ESOP})},
- Year = {2014},
- Pages = {169--188},
- abstract = {We provide a program logic for specifying a core subset of the sequential POSIX file system, and for reasoning abstractly about client programs working with the file system.},
-}
-
-@InProceedings{dinsdaleyoung:popl:2013,
- Title = {{\em Views: Compositional Reasoning for Concurrent Programs}},
- Author = {Thomas Dinsdale{-}Young and Lars Birkedal and Philippa Gardner and Matthew J. Parkinson and Hongseok Yang},
- Booktitle = {Proceedings of the 40\textsuperscript{th} Annual {ACM} {SIGPLAN-SIGACT} Symposium on Principles of Programming Languages ({POPL})},
- Year = {2013},
- Pages = {287--300},
- abstract = {Compositional abstractions underly many reasoning principles for concurrent programs: the concurrent environment is abstracted in order to reason about a thread in isolation; and these abstractions are composed to reason about a program consisting of many threads. For instance, separation logic uses formulae that describe part of the state, abstracting the rest; when two threads use disjoint state, their specifications can be composed with the separating con- junction. Type systems abstract the state to the types of variables; threads may be composed when they agree on the types of shared variables.
In this paper, we present the ?Concurrent Views Framework?, a metatheory of concurrent reasoning principles. The theory is parameterised by an abstraction of state with a notion of composition, which we call views. The metatheory is remarkably simple, but highly applicable: the rely-guarantee method, concurrent separation logic, concurrent abstract predicates, type systems for recursive references and for unique pointers, and even an adaptation of the Owicki-Gries method can all be seen as instances of the Con- current Views Framework. Moreover, our metatheory proves each of these systems is sound without requiring induction on the operational semantics.},
-}
-
-@InProceedings{gardner:popl:2012,
- Title = {{\em Towards a Program Logic for JavaScript}},
- Author = {Philippa Gardner and Sergio Maffeis and Gareth Smith},
- Booktitle = {Proceedings of the 39\textsuperscript{th} {ACM} {SIGPLAN-SIGACT} Symposium on Principles of Programming Languages ({POPL})},
- Year = {2012},
- Pages = {31--44},
- abstract = {JavaScript has become the most widely used language for client- side web programming. The dynamic nature of JavaScript makes understanding its code notoriously difficult, leading to buggy pro- grams and a lack of adequate static-analysis tools. We believe that logical reasoning has much to offer JavaScript: a simple description of program behaviour, a clear understanding of module boundaries, and the ability to verify security contracts.
We introduce a program logic for reasoning about a broad subset of JavaScript, including challenging features such as prototype inheritance and with. We adapt ideas from separation logic to provide tractable reasoning about JavaScript code: reasoning about easy programs is easy; reasoning about hard programs is possible. We prove a strong soundness result. All libraries written in our subset and proved correct with respect to their specifications will be well-behaved, even when called by arbitrary JavaScript code.},
-}
-
-@InProceedings{rochapinto:oopsla:2011,
- Title = {{\em A Simple Abstraction for Complex Concurrent Indexes}},
- Author = {Pedro da Rocha Pinto and Thomas Dinsdale{-}Young and Mike Dodds and Philippa Gardner and Mark J. Wheelhouse},
- Booktitle = {Proceedings of the 26\textsuperscript{th} Annual {ACM} {SIGPLAN} Conference on Object-Oriented Programming, Systems, Languages, and Applications ({OOPSLA})},
- Year = {2011},
- Pages = {845--864},
- abstract = {Indexes are ubiquitous. Examples include associative arrays, dictionaries, maps and hashes used in applications such as databases, file systems and dynamic languages. Abstractly, a sequential index can be viewed as a partial function from keys to values. Values can be queried by their keys, and the index can be mutated by adding or removing mappings. Whilst appealingly simple, this abstract specification is in- sufficient for reasoning about indexes that are accessed con- currently.
We present an abstract specification for concurrent indexes. We verify several representative concurrent client applications using our specification, demonstrating that clients can reason abstractly without having to consider specific underlying implementations. Our specification would, how- ever, mean nothing if it were not satisfied by standard implementations of concurrent indexes. We verify that our specification is satisfied by algorithms based on linked lists, hash tables and BLink trees. The complexity of these algorithms, in particular the BLink tree algorithm, can be completely hidden from the client?s view by our abstract specification.},
-}
-
-@InProceedings{dinsdaleyoung:vstte:2010,
- Title = {{Abstraction and Refinement for Local Reasoning}},
- Author = {Thomas Dinsdale{-}Young and Philippa Gardner and Mark J. Wheelhouse},
- Booktitle = {Proceedings of the 3\textsuperscript{rd} International Conference on Verified Software: Theories, Tools, Experiments ({VSTTE})},
- Year = {2010},
- Pages = {199--215},
- 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.},
-}
-
-@InProceedings{dinsdaleyoung:ecoop:2010,
- Title = {{\em Concurrent Abstract Predicates}},
- Author = {Thomas Dinsdale{-}Young and Mike Dodds and Philippa Gardner and Matthew J. Parkinson and Viktor Vafeiadis},
- Booktitle = {Proceedings of the 24\textsuperscript{th} European Conference on Object-Oriented Programming ({ECOOP})},
- Year = {2010},
- Pages = {504--528},
- abstract = {Abstraction is key to understanding and reasoning about large computer systems. Abstraction is simple to achieve if the relevant data structures are disjoint, but rather difficult when they are partially shared, as is often the case for concurrent modules. We present a pro- gram logic for reasoning abstractly about data structures that provides a fiction of disjointness and permits compositional reasoning. The internal details of a module are completely hidden from the client by concurrent abstract predicates. We reason about a module?s implementation using separation logic with permissions, and provide abstract specifications for use by client programs using concurrent abstract predicates. We illustrate our abstract reasoning by building two implementations of a lock module on top of hardware instructions, and two implementations of a concurrent set module on top of the lock module.},
-}
-
-@InProceedings{cardelli:cie:2010,
- Title = {Processes in Space},
- Author = {Luca Cardelli and Philippa Gardner},
- Booktitle = {Proceedings of the 6\textsuperscript{th} Conference on Computability in Europe {CiE} - Programs, Proofs, Processes},
- Year = {2010},
- Pages = {78--87},
- abstract = {We introduce a geometric process algebra based on affine geometry, with the aim of describing the concurrent evolution of geometric structures in 3D space. We prove a relativity theorem stating that algebraic equations are invariant under rigid body transformations.},
-}
-
-@InProceedings{whellhouse:WSFM:2009,
- Title = {{Small Specifications for Tree Update}},
- Author = {Philippa Gardner and Mark J. Wheelhouse},
- Booktitle = {Proceedings of the 6\textsuperscript{th} International Workshop on Web Services and Formal Methods ({WS-FM})},
- Year = {2009},
- Pages = {178--195},
- 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.},
-}
-
-@InProceedings{raza:esop:2009,
- Title = {{Automatic Parallelization with Separation Logic}},
- Author = {Mohammad Raza and Cristiano Calcagno and Philippa Gardner},
- Booktitle = {Proceedings of the 18\textsuperscript{th} European Symposium on Programming ({ESOP})},
- Year = {2009},
- Pages = {348--362},
- abstract = {We present a separation logic framework which can express proper- ties of memory separation between different points in a program. We describe an algorithm based on this framework for determining independences between statements in a program which can be used for parallelization.},
-}
-
-@InProceedings{raza:fossacs:2008,
- Title = {{Footprints in Local Reasoning}},
- Author = {Mohammad Raza and Philippa Gardner},
- Booktitle = {Proceedings of the 11\textsuperscript{th} International Conference on Foundations of Software Science and Computational Structures ({FOSSACS})},
- Year = {2008},
- Pages = {201--215},
- abstract = {We present a separation logic framework which can express proper- ties of memory separation between different points in a program. We describe an algorithm based on this framework for determining independences between statements in a program which can be used for parallelization.},
-}
-
-@InProceedings{gardner:planx:2008,
- Title = {{DOM: Towards a Formal Specification}},
- Author = {Philippa Gardner and Gareth Smith and Mark J. Wheelhouse and Uri Zarfaty},
- Booktitle = {Proceedings of the {ACM} {SIGPLAN} Workshop on Programming Language Technologies for XML ({PLAN-X})},
- Year = {2008},
- abstract = {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 work with a minimal set of commands and obtain a complete reasoning for straight-line code. Our work transfers O?Hearn, Reynolds and 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 Zarfaty on local Hoare reasoning about a simple tree-update language to DOM, showing that our reasoning scales to DOM. Our reasoning not only formally specifies a significant subset of DOM Core Level 1, but can also be used to verify e.g. invariant properties of simple Javascript programs.},
-}
-
-@InProceedings{gardner:pods:2008,
- Title = {{\em Local Hoare Reasoning about {DOM}}},
- Author = {Philippa Gardner and Gareth Smith and Mark J. Wheelhouse and Uri Zarfaty},
- Booktitle = {Proceedings of the 27\textsuperscript{th} {ACM} {SIGMOD-SIGACT-SIGART} Symposium on Principles of Database Systems ({PODS})},
- Year = {2008},
- Pages = {261--270},
- abstract = {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 work with a minimal set of commands and obtain a complete reasoning for straight-line code. Our work transfers O?Hearn, Reynolds and 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 Zarfaty on local Hoare reasoning about simple tree update to this real-world DOM application. Our reasoning not only formally specifies a significant subset of DOM Core Level 1, but can also be used to verify, for example, invariant properties of simple Javascript programs.},
-}
-
-@InProceedings{calcagno:aplas:2007,
- Title = {{Adjunct Elimination in Context Logic for Trees}},
- Author = {Cristiano Calcagno and Thomas Dinsdale{-}Young and Philippa Gardner},
- Booktitle = {Proceedings of the 5\textsuperscript{th} Asian Symposium on Programming Languages and Systems ({APLAS})},
- Year = {2007},
- Pages = {255--270},
- 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.},
-}
-
-@InProceedings{calcagno:popl:2007,
- Title = {{Context Logic as Modal Logic: Completeness and Parametric Inexpressivity}},
- Author = {Cristiano Calcagno and Philippa Gardner and Uri Zarfaty},
- Booktitle = {Proceedings of the 34\textsuperscript{th} {ACM} {SIGPLAN-SIGACT} Symposium on Principles of Programming Languages ({POPL})},
- Year = {2007},
- Pages = {123--134},
- 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 dis- joint subdata, and corresponding structural adjoint(s) for reasoning hypothetically about data. We show how to interpret these struc- tural connectives as modalities in Modal Logic and prove complete- ness 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.},
-}
-
-%Edinburgh, UK
-@InProceedings{calcagno:fossacs:2005,
- Title = {{From Separation Logic to First-Order Logic}},
- Author = {Cristiano Calcagno and Philippa Gardner and Matthew Hague},
- Booktitle = {Proceedings of the 8th International Conference on Foundations of Software Science and Computational Structures ({FOSSACS})},
- Year = {2005},
- Pages = {395--409},
- 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.},
-}
-
-%Long Beach, California, USA
-@InProceedings{calcagno:popl:2005,
- Title = {{\em Context Logic and Tree Update}},
- Author = {Cristiano Calcagno and Philippa Gardner and Uri Zarfaty},
- Booktitle = {Proceedings of the 32\textsuperscript{nd} {ACM} {SIGPLAN-SIGACT} Symposium on Principles of Programming Languages ({POPL})},
- Year = {2005},
- Pages = {271--282},
- 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.},
-}
-
-%Chennai, India
-@InProceedings{dawar:fsttcs:2004,
- Title = {{Adjunct Elimination Through Games in Static Ambient Logic}},
- Author = {Anuj Dawar and Philippa Gardner and Giorgio Ghelli},
- Booktitle = {Proceedings of the 24\textsuperscript{th} International Conference on Foundations of Software Technology and Theoretical Computer Science ({FSTTCS})},
- Year = {2004},
- Pages = {211--223},
- 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.}
-}
-
-%Exploring New Frontiers of Theoretical Informatics, {IFIP} 18\textsuperscript{th} World Computer Congress, {TC1},
-% Toulouse, France
-@InProceedings{maffeis:tcs:2004,
- Title = {{Behavioural Equivalences for Dynamic Web Data}},
- Author = {Sergio Maffeis and Philippa Gardner},
- Booktitle = {Proceedings of 3\textsuperscript{rd} International Conference on Theoretical Computer Science {TCS}},
- Year = {2004},
- Pages = {535--548},
- abstract = {We study behavioural equivalences for dynamic web data in Xd$\pi$, a model for reasoning about behaviour found in (for example) dynamic web page programming, applet interaction, and web-service orchestration. Xd$\pi$ is based on an idealised model of semistructured data, and an extension of the 7r-calculus with locations and operations for interacting with data. The equivalences are nonstandard due to the integration of data and processes, and the presence of locations.},
-}
-
-%Barcelona, Spain
-@InProceedings{wischik:fossacs:2004,
- Title = {{Strong Bisimulation for the Explicit Fusion Calculus}},
- Author = {Lucian Wischik and Philippa Gardner},
- Booktitle = {Proceedings of the 7\textsuperscript{th} International Conference on Foundations of Software Science and Computation Structures ({FOSSACS})},
- Year = {2004},
- Pages = {484--498},
- abstract = {The pi calculus holds the promise of compile-time checks for whether a given program will have the correct interactive behaviour.},
-}
-
-% Potsdam, Germany
-@InProceedings{gardner:dbpl:2003,
- Title = {{Modelling Dynamic Web Data}},
- Author = {Philippa Gardner and Sergio Maffeis},
- Booktitle = {Proceedings of 9\textsuperscript{th} International Workshop on Database Programming Languages ({DBPL})},
- Year = {2003},
- Pages = {130--146},
- abstract = {We introduce Xd$\pi$, a peer-to-peer model for reasoning about the dynamic behaviour of web
- data. It is based on an idealised model of semi- structured data, and an extension of the ?-calculus with process
- mobility and with an operation for interacting with data. Our model can be used to reason about behaviour found
- in, for example, dynamic web page program- ming, applet interaction, and service orchestration. We study
- behavioural equivalences for Xd$\pi$, motivated by examples.}
-}
-
-%Marseille, France
-@InProceedings{gardner:concur:2003,
- Title = {{Linear Forwarders}},
- Author = {Philippa Gardner and Cosimo Laneve and Lucian Wischik},
- Booktitle = {Proceedings of the 14\textsuperscript{th} International Conference on Concurrency Theory ({CONCUR})},
- Year = {2003},
- Pages = {408--422},
- abstract = {A linear forwarder is a process that receives one message on a channel and sends it on a different channel. We use linear forwarders to provide a distributed implementation of Milner?s asynchronous pi calculus. Such a distributed implementation is known to be difficult due to input capability, where a received name is used as the subject of a subsequent input. This allows the dynamic creation of large input processes in the wrong place, thus requiring comparatively large code migrations in order to avoid consensus problems. Linear forwarders constitute a small atom of input capability that is easy to move.
We show that the full input capability can be simply encoded using linear for- warders. We also design a distributed machine, demonstrating the ease with which we can implement the pi calculus using linear forwarders. We also show that linear forwarders allow for a simple encoding of distributed choice and have ?clean? behaviour in the presence of failures.},
-}
-
-% Warsaw, Poland
-@InProceedings{cardelli:fossacs:2003,
- Title = {{Manipulating Trees with Hidden Labels}},
- Author = {Luca Cardelli and Philippa Gardner and Giorgio Ghelli},
- Booktitle = {Proceedings of the 6\textsuperscript{th} International Conference on Foundations of Software Science and Computational Structures ({FOSSACS})},
- Year = {2003},
- Pages = {216--232},
- abstract = {We define an operational semantics and a type system for manipulat- ing semistructured data that contains hidden information. The data model is sim- ple labeled trees with a hiding operator. Data manipulation is based on pattern matching, with types that track the use of hidden labels.},
-}
-
-% Malaga, Spain
-@InProceedings{cardelli:icalp:2002,
- Title = {{A Spatial Logic for Querying Graphs}},
- Author = {Luca Cardelli and Philippa Gardner and Giorgio Ghelli},
- Booktitle = {Proceedings of the 29\textsuperscript{th} International Colloquium on Automata, Languages and Programming ({ICALP})},
- Year = {2002},
- Pages = {597--610},
- 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.},
-}
-
-%Brno, Czech Republic
-@InProceedings{gardner:concur:2002,
- Title = {{The Fusion Machine}},
- Author = {Philippa Gardner and Cosimo Laneve and Lucian Wischik},
- Booktitle = {Proceedings of the 13\textsuperscript{th} International Conference on Concurrency Theory ({CONCUR}) 2002},
- Year = {2002},
- Pages = {418--433},
- abstract = {We present a new model for the distributed implementation of pi-like calculi, which permits strong correctness results that are simple to prove. We describe the distributed channel machine -- a distributed version of a machine proposed by Cardelli. The distributed channel machine groups pi processes at their channels (or locations), in contrast with the more common approach of incorporating additional location information within pi processes. We go on to describe the fusion machine. It uses a form of concurrent constraints called fusions -- equations on channel names -- to distribute fragments of these processes between remote channels. This fragmentation avoids the movement of large continuations between locations, and leads to a more efficient implementation model.},
-}
-
-% University Park, PA, USA, August 22-25, 2000, Proceedings
-@InProceedings{gardner:concur:2000,
- Title = {{From Process Calculi to Process Frameworks}},
- Author = {Philippa Gardner},
- Booktitle = {Proceedings of 11\textsuperscript{th} International Conference on Concurrency Theory ({CONCUR})},
- Year = {2000},
- Pages = {69--88},
- abstract = {We present two process frameworks: the action calculi of Milner, and the fusion systems of Gardner and Wischik. The action calculus framework is based on process constructs arising from the ?-calculus. We give a non-standard presentation of the ?-calculus, to emphasise the similarities between the calculus and the framework.The fusion system framework generalises a new process calculus called the $\pi$F-calculus.We describe the ?F -calculus, which is based on different process constructs to those of the ?-calculus, and show that the generalisation from the calculus to the framework is simple.We compare the frameworks by studying examples. In this paper, we describe two process frameworks: the action calculi of Milner ( Mil96 ), and the fusion systems of Gardner and Wischik ( GW99 ). The action calculus framework is based on process constructs arising from the ?- calculus. We give a non-standard presentation of the ?-calculus, to emphasise the similarities between the calculus and the framework. We also present the fusion system framework which generalises a new process calculus, called the $\pi$-calculus ( GW00 ), in much the same way as the action calculus framework generalises the $\pi$-calculus. The $\pi$F-calculus is similar to the ?-calculus in that its interactive behaviour is based on input and output processes, and different in that its underlying process structure is not the same. We describe the $\pi$F-calculus.}
-}
-
-%2000, Bratislava, Slovakia, August 28 - September 1, 2000, Proceedings
-@InProceedings{gardner:mfcs:2000,
- Title = {{Explicit Fusions}},
- Author = {Philippa Gardner and Lucian Wischik},
- Booktitle = {Proceedings of the 25\textsuperscript{th} International Symposium on Mathematical Foundations of Computer Science ({MFCS})},
- Year = {2000},
- Pages = {373--382},
- abstract = {We introduce explicit fusions of names. An explicit fusion is a process that exists concurrently with the rest of the system and enables two names to be used interchangeably. Explicit fusions provide a small-step account of reaction in process calculi such as the pi calculus and the fusion calculus. In this respect they are similar to the explicit substitutions of Abadi, Cardelli and Curien, which do the same for the lambda calculus. In this paper, we give a technical foundation for explicit fusions. We present the pi-F calculus, a simple process calculus with explicit fusions, and define a strong bisimulation congruence. We study the embeddings of the fusion calculus and the pi calculus. The former is fully abstract with respect to bisimulation.},
-}
-
-% '97, Sendai, Japan, September 23-26, 1997, Proceedings
-@InProceedings{gardner:tacs:97,
- Title = {{Types and Models for Higher-Order Action Calculi}},
- Author = {Philippa Gardner and Masahito Hasegawa},
- Booktitle = {Proceedings of the 3\textsuperscript{rd} International Symposium on Theoretical Aspects of Computer Software ({TACS})},
- Year = {1997},
- Pages = {583--603},
- abstract = {Milner introduced action calculi as a framework for representing models of interactive behaviour. He also introduced the higher-order action calculi, which add higher-order features to the basic setting. We present type theories for action calculi and higher-order action calculi, and give the categorical models of the higher-order calculi. As applications, we give a semantic proof of the conservativity of higher-order action calculi over action calculi, and a precise connection with Moggi's computational lambda calculus and notions of computation.},
-}
-
-%, Aarhus, Denmark, August 23-29, 1997, Selected Papers
-% , Annual Conference of the EACSL, Aarhus, Denmark
-@InProceedings{barber:csl:1997,
- Title = {{From Action Calculi to Linear Logic}},
- Author = {Andrew Barber and Philippa Gardner and Masahito Hasegawa and Gordon D. Plotkin},
- Booktitle = {Proceedings of the 11\textsuperscript{th} International Workshop on Computer Science Logic {CSL}},
- Year = {1997},
- Pages = {78--97},
- abstract = {Milner introduced action calculi as a framework for investigating models of interactive behaviour. We present a type-theoretic account of action calculi using the propositions-as-types paradigm; the type theory has a sound and complete interpretation in Power?s categorical models. We go on to give a sound translation of our type theory in the (type theory of) intuitionistic linear logic, corresponding to the relation between Benton?s models of linear logic and models of action calculi. The conservativity of the syntactic translation is proved by a model-embedding construction using the Yoneda lemma. Finally, we briefly discuss how these techniques can also be used to give conservative translations between various extensions of action calculi.},
-}
-
-% '94, Sendai, Japan, April 19-22, 1994, Proceedings
-@InProceedings{gardner:tacs:94,
- Title = {{Discovering Needed Reductions Using Type Theory}},
- Author = {Philippa Gardner},
- Booktitle = {Proceeding of the International Conference on Theoretical Aspects of Computer Software (TACS)},
- Year = {1994},
- Pages = {555--574},
- abstract = {The identification of the needed redexes in a term is an undecidable problem. We introduce a (partially decidable) type assignment system, which distinguishes certain redexes called the allowable redexes. For a well-typed term e, allowable redexes are-needed redexes. In addition, with principal typing, all the needed redexes of a normalisable term are allowable. Using these results, we are able to identify all the needed reductions of a principally typed normalisable term. Possible applications of these results include strictness and sharing analysis for functional programming languages, and a reduction strategy for well-typed terms which satisfies Levy's notion of optimal reduction.}
-}
-
-%'93, St. Petersburg, Russia, July 13-20, 1993, Proceedings}
-@InProceedings{gardner:lpar:93,
- Title = {{A New Type Theory for Representing Logics}},
- Author = {Philippa Gardner},
- Booktitle = {Proceedings of the 4th International Conference on Logic Programming and Automated Reasoning (LPAR)},
- Year = {1993},
- Pages = {146--157},
- abstract = {We propose a new type theory for representing logics, called LF+ and based on the Edinburgh Logical Framework. The new framework allows us to give, apparently for the first time, general definitions which capture how well a logic has been represented. Using our definitions, we show that, for example, first-order logic can be wellrepresented in LF+, whereas linear and relevant logics cannot. These syntactic definitions of representation have a simple formulation as indexed isomorphisms, which both confirms that our approach is a natural one, and provides a link between type-theoretic and categorical approaches to frameworks.},
-}
-
-@Article{cardelli:tcs:2012,
- Title = {{Processes in Space}},
- Author = {Luca Cardelli and Philippa Gardner},
- Journal = {Theoretical Computer Science},
- Year = {2012},
- Pages = {40--55},
- Volume = {431},
- abstract = {We introduce a geometric process algebra based on affine geometry, with the aim of describing the concurrent evolution of geometric structures in 3D space. We prove a relativity theorem stating that algebraic equations are invariant under rigid body transformations.}
-}
-
-@Article{calcagno:ic:2010,
- Title = {{Adjunct elimination in Context Logic for Trees}},
- Author = {Cristiano Calcagno and Thomas Dinsdale{-}Young and Philippa Gardner},
- Journal = {Information and Computation},
- Year = {2010},
- Number = {5},
- Pages = {474--499},
- Volume = {208},
- 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.}
-}
-
-@Article{cardelli:entcs:2009,
- Title = {{A Process Model of Actin Polymerisation}},
- Author = {Luca Cardelli and Emmanuelle Caron and Philippa Gardner and Ozan Kahramanogullari and Andrew Phillips},
- Journal = {Electronic Notes in Theoretical Computer Science},
- Year = {2009},
- Number = {1},
- Pages = {127--144},
- Volume = {229},
- abstract = {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.},
-}
-
-@Article{cardelli:tcs:2009,
- Title = {{A Process Model of Rho GTP-binding Proteins}},
- Author = {Luca Cardelli and Emmanuelle Caron and Philippa Gardner and Ozan Kahramanogullari and Andrew Phillips},
- Journal = {Theoretical Computer Science},
- Year = {2009},
- Number = {33-34},
- Pages = {3166--3185},
- Volume = {410},
- abstract = {Rho GTP-binding proteins play a key role as molecular switches in many cellular activities. In response to extracellular stimuli and with the help from regulators (GEF, GAP, Effector, GDI), these proteins serve as switches that interact with their environment in a complex manner. Based on the structure of a published ordinary differential equations (ODE) model, we first present a generic process model for the Rho GTP- binding proteins, and compare it with the ODE model. We then extend the basic model to include the behaviour of the GDIs and explore the parameter space for the extended model with respect to biological data from the literature. We discuss the challenges this extension brings and the directions of further research. In particular, we present techniques for modular representation and refinement of process models, where, for example, different Rho proteins with different rates for regulator interactions can be given as the instances of the same parametric model.},
-}
-
-@Article{raza:lmcs:2009,
- Title = {{Footprints in Local Reasoning}},
- Author = {Mohammad Raza and Philippa Gardner},
- Journal = {Logical Methods in Computer Science},
- Year = {2009},
- Number = {2},
- Volume = {5},
- abstract = {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 investigate the conditions under which the footprints correspond to the smallest safe states, and present a heap model in which, unlike the standard model, this is the case for every program.},
-}
-
-@Article{cardelli:ents:2008,
- Title = {{A Process Model of Rho GTP-binding Proteins in the Context of Phagocytosis}},
- Author = {Luca Cardelli and Philippa Gardner and Ozan Kahramanogullari},
- Journal = {Electronic Notes in Theoretical Computer Science},
- Year = {2008},
- Number = {3},
- Pages = {87--102},
- Volume = {194},
- abstract = {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.},
-}
-
-@Article{maffeis:jlap:2008,
- Title = {{Behavioural Equivalences for Dynamic Web Data}},
- Author = {Sergio Maffeis and Philippa Gardner},
- Journal = {Logic and Algebraic Programming},
- Year = {2008},
- Number = {1},
- Pages = {86--138},
- Volume = {75},
- abstract = {We study behavioural equivalences for dynamic web data in Xdn, a model for reasoning about behaviour found in (for example) dynamic web page programming, applet interaction, and web-service orchestration. Xdn is based on an idealised model of semistructured data, and an extension of the 7r-calculus with locations and operations for interacting with data. The equivalences are nonstandard due to the integration of data and processes, and the presence of locations. },
-}
-
-@Article{calcagno:entcs:2007,
- Title = {{Local Reasoning about Data Update}},
- Author = {Cristiano Calcagno and Philippa Gardner and Uri Zarfaty},
- Journal = {Electronic Notes on Theoretical Computer Science},
- Year = {2007},
- Pages = {133--175},
- Volume = {172},
- 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.}
-}
-
-@Article{cardelli:entcs:2007,
- Title = {{Manipulating Trees with Hidden Labels}},
- Author = {Luca Cardelli and Philippa Gardner and Giorgio Ghelli},
- Journal = {Electronic Notes in Theoretical Computer Science},
- Year = {2007},
- Pages = {177--201},
- Volume = {172},
- abstract = {We define an operational semantics and a type system for manipulat- ing semistructured data that contains hidden information. The data model is sim- ple labeled trees with a hiding operator. Data manipulation is based on pattern matching, with types that track the use of hidden labels.}
-}
-
-@Article{dawar:ic:2007,
- Title = {{Expressiveness and Complexity of Graph Logic}},
- Author = {Anuj Dawar and Philippa Gardner and Giorgio Ghelli},
- Journal = {Information and Computation},
- Year = {2007},
- Number = {3},
- Pages = {263--310},
- Volume = {205},
- 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 ?-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.},
-}
-
-@Article{gardner:ic:2007,
- Title = {{Linear Forwarders}},
- Author = {Philippa Gardner and Cosimo Laneve and Lucian Wischik},
- Journal = {Information and Computation},
- Year = {2007},
- Number = {10},
- Pages = {1526--1550},
- Volume = {205},
- abstract = {A linear forwarder is a process that receives one message on a channel and sends it on a different channel. We use linear forwarders to provide a distributed implementation of Milner?s asynchronous pi calculus. Such a distributed implementation is known to be difficult due to input capability, where a received name is used as the subject of a subsequent input. This allows the dynamic creation of large input processes in the wrong place, thus requiring comparatively large code migrations in order to avoid consensus problems. Linear forwarders constitute a small atom of input capability that is easy to move.
We show that the full input capability can be simply encoded using linear for- warders. We also design a distributed machine, demonstrating the ease with which we can implement the pi calculus using linear forwarders. We also show that lin- ear forwarders allow for a simple encoding of distributed choice and have ?clean? behaviour in the presence of failures.},
-}
-
-@Article{wischik:tcs:2005,
- Title = {{Explicit Fusions}},
- Author = {{Lucian Wischik and Philippa Gardner}},
- Journal = {Theoretical Computer Science},
- Year = {2005},
- Number = {3},
- Pages = {606--630},
- Volume = {340},
- abstract = {We introduce explicit fusions of names. An explicit fusion is a process that exists concurrently with the rest of the system and enables two names to be used interchangeably. Explicit fusions provide a small-step account of reaction in process calculi such as the pi calculus and the fusion calculus. In this respect they are similar to the explicit substitutions of Abadi, Cardelli and Curien, which do the same for the lambda calculus. In this paper, we give a technical foundation for explicit fusions. We present the pi-F calculus, a simple process calculus with explicit fusions, and define a strong bisimulation congruence. We study the embeddings of the fusion calculus and the pi calculus. The former is fully abstract with respect to bisimulation.},
-}
-
-@Article{gardner:tcs:2005,
- Title = {{Modelling Dynamic Web Data}},
- Author = {Philippa Gardner and Sergio Maffeis},
- Journal = {Theoretical Computer Science},
- Year = {2005},
- Number = {1},
- Pages = {104--131},
- Volume = {342},
- abstract = {We introduce Xd?, a peer-to-peer model for reasoning about the dynamic behaviour of web data. It is based on an idealised model of semi-structured data, and an extension of the $\pi$-calculus with process mobility and with an operation for interacting with data. Our model can be used to reason about behaviour found in, for example, dynamic web page programming, applet interaction, and service orchestration. We study behavioural equivalences for Xd$\pi$, motivated by examples.}
-}
-
-@Article{gardner:tcs:1999,
- Title = {Closed Action Calculi},
- Author = {Philippa Gardner},
- Journal = {Theoretical Computer Science},
- Year = {1999},
- Number = {1-2},
- Pages = {77--103},
- Volume = {228},
- abstract = {Action calculi provide a framework for capturing many kinds of interactive behaviour by focussing on the primitive notion of names. We introduce a name-free account of action calculi, called the closed action calculi, and show that there is a strong correspondence between the original presentation and the name-free presentation. We also add free names plus natural axioms to the closed world, and show that the abstraction operator can be constructed as a derived operator. Our results show that in some sense names are inessential. However, the purpose of action calculi is to understand formalisms which mimic the behaviour of interactive systems. Perhaps more significantly therefore, these results highlight the important presentational role that names play.},
-}
-
-@Article{gardner:entcs:1997,
- Title = {A Type-theoretic Description of Action Calculi},
- Author = {Philippa Gardner},
- Journal = {Electronic Notes in Theoretical Computer Science},
- Year = {1997},
- Pages = {52},
- Volume = {10},
- abstract = {Action calculi, introduced by Milner, provide a framework for investigating models of interaction. This talk will focus on the connection between action calculi and known concepts arising from type theory. The aim of this work is to isolate what is distinctive about action calculi, and to investigate the potential of action calculi as an underlying framework for many kinds of computational behaviour.The first part of the talk will introduce action calculi. In the second part, I'll give a type-theoretic account of action calculi, using the general binding operators of Aczel. I will discuss two extensions: higher-order action calculi which correspond to Moggi's commutative computational lambda-calculus, and linear action calculi which correspond to the linear type theories of Barber and Benton.This talk is based on joint work with Andrew Barber, Masahito Hasegawa and Gordon Plotkin. If time, I will also describe current work arising from the connections described above. }
-}
-
-@Article{gardner:entcs:1995,
- Title = {{A Name-free Account of Action Calculi}},
- Author = {Philippa Gardner},
- Journal = {Electronic Notes in Theoretical Computer Science},
- Year = {1995},
- Pages = {214--231},
- Volume = {1},
- abstract = {Action calculi provide a unifying framework for representing a variety of models of communication, such as CCS, Petri nets and the ?-calculus, within a unified setting. A central idea is to model the interaction between actions using names. We introduce a name-free account of action calculi, called the closed action calculi, and show that there is a strong correspondence between the original presentation and the name-free presentation. These results show that, although names play an important presentational role, they are in some sense inessential.}
-}
-
-@Article{gardner:mscs:1995,
- Title = {{Equivalences between Logics and their Representing Type Theories}},
- Author = {Philippa Gardner},
- Journal = {Mathematical Structures in Computer Science},
- Year = {1995},
- Number = {3},
- Pages = {323--349},
- Volume = {5},
- abstract = {We propose a new framework for representing logics, called LF+, which is based on the Edinburgh Logical Framework. The new framework allows us to give, apparently for the first time, general definitions that capture how well a logic has been represented. These definitions are possible because we are able to distinguish in a generic way that part of the LF+ entailment corresponding to the underlying logic. This distinction does not seem to be possible with other frameworks. Using our definitions, we show that, for example, natural deduction first-order logic can be well-represented in LF, whereas linear and relevant logics cannot. We also show that our syntactic definitions of representation have a simple formulation as indexed isomorphisms, which both confirms that our approach is a natural one and provides a link between type-theoretic and categorical approaches to frameworks.},
-}
-
-@Article{gardner:mscs:1991,
- Title = {{Unfold/Fold Transformations in Logic Programming}},
- Author = {Philippa Gardner},
- Journal = {Mathematical Structures in Computer Science},
- Year = {1991},
- Number = {2},
- Pages = {143--157},
- Volume = {02},
- abstract = {Unfold/fold transformation rules for disjunctive logic programs are proposed in this paper. Our transformation rules preserve the meaning of the programs.},
+@InProceedings{Dinsdale-Young2010Abstraction,
+ Title = {{Abstraction and Refinement for Local Reasoning}},
+ Author = {Thomas Dinsdale{-}Young and Philippa Gardner and Mark J. Wheelhouse},
+ Booktitle = {Proceedings of the 3\textsuperscript{rd} International Conference on Verified Software: Theories, Tools, Experiments ({VSTTE})},
+ Year = {2010},
+ Pages = {199--215},
+
+ 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.}
+}
+
+@InProceedings{Gardner2010Reasoning,
+ Title = {{Reasoning About Client-side Web Programs: Invited Talk}},
+ Author = {Philippa Gardner},
+ Booktitle = {Proceedings of the 2010 {EDBT/ICDT} Workshops, Lausanne, Switzerland, March 22-26, 2010},
+ Year = {2010},
+
+ Abstract = {In PODS 2008, I presented a paper on a formal, compositional specification of the Document Object Model (DOM), a W3C XML Update library. This work concentrated on Featherweight DOM, a small fragment of DOM which focuses on the XML tree structure and simple text nodes. Since the formal reasoning is compositional, we are able to work with a minimal set of commands and obtain complete reasoning for straight-line code. We are also able to verify, for example, invariant properties of simple DOM programs. This work is based on a recent breakthrough in program verification, based on analysing a program's use of resource. The idea is that the reasoning should follow the programmers' intuitions about which part of the computer memory the program touches. This style of reasoning was introduced by O'Hearn (Queen Mary) and Reynolds (CMU) in their work on Separation Logic for reasoning modularly about large C-programs (e.g. Microsoft device driver code, Linux). I substantially extended the range of local resource reasoning, introducing Context Logic to reason about programs that directly manipulate complex data structures such as XML. In this survey talk, I will give an overview of our theoretical and practical work on reasoning about DOM, highlighting recent developments which include: 1. the extension of this work to DOM Core Level 1. A substantial piece of work, not because of the reasoning, but because full DOM is large, underspecified and difficult to interpret, with no consensus between browsers; 2. reasoning about the combination of JavaScript and DOM to provide, for example, secure mashups for a more flexible, secure integration of outsourced payment services; 3. on-going work on a verification tool for automatically reasoning about DOM programs and the identification of key examples of web applications on which to test our DOM reasoning: e.g., with current technology, we can prove by hand that mashup programs are fault free; with our tool, such proofs will be automatic. An ultimate challenge is to develop the necessary reasoning technology to provide a safe and secure web environment on which to build the next generation of web applications, thus demonstrating the scientific feasibility of a reliable Web.}
+}
+
+@InProceedings{Gardner2000From,
+ Title = {{From Process Calculi to Process Frameworks}},
+ Author = {Philippa Gardner},
+ Booktitle = {Proceedings of 11\textsuperscript{th} International Conference on Concurrency Theory ({CONCUR})},
+ Year = {2000},
+ Pages = {69--88},
+
+ Abstract = {We present two process frameworks: the action calculi of Milner, and the fusion systems of Gardner and Wischik. The action calculus framework is based on process constructs arising from the ?-calculus. We give a non-standard presentation of the ?-calculus, to emphasise the similarities between the calculus and the framework.The fusion system framework generalises a new process calculus called the $\pi$F-calculus.We describe the ?F -calculus, which is based on different process constructs to those of the ?-calculus, and show that the generalisation from the calculus to the framework is simple.We compare the frameworks by studying examples. In this paper, we describe two process frameworks: the action calculi of Milner ( Mil96 ), and the fusion systems of Gardner and Wischik ( GW99 ). The action calculus framework is based on process constructs arising from the ?- calculus. We give a non-standard presentation of the ?-calculus, to emphasise the similarities between the calculus and the framework. We also present the fusion system framework which generalises a new process calculus, called the $\pi$-calculus ( GW00 ), in much the same way as the action calculus framework generalises the $\pi$-calculus. The $\pi$F-calculus is similar to the ?-calculus in that its interactive behaviour is based on input and output processes, and different in that its underlying process structure is not the same. We describe the $\pi$F-calculus.}
+}
+
+@Article{Gardner1999Closed,
+ Title = {Closed Action Calculi},
+ Author = {Philippa Gardner},
+ Journal = {Theoretical Computer Science},
+ Year = {1999},
+ Number = {1-2},
+ Pages = {77--103},
+ Volume = {228},
+
+ Abstract = {Action calculi provide a framework for capturing many kinds of interactive behaviour by focussing on the primitive notion of names. We introduce a name-free account of action calculi, called the closed action calculi, and show that there is a strong correspondence between the original presentation and the name-free presentation. We also add free names plus natural axioms to the closed world, and show that the abstraction operator can be constructed as a derived operator. Our results show that in some sense names are inessential. However, the purpose of action calculi is to understand formalisms which mimic the behaviour of interactive systems. Perhaps more significantly therefore, these results highlight the important presentational role that names play.}
+}
+
+@Article{Gardner1997Type,
+ Title = {A Type-theoretic Description of Action Calculi},
+ Author = {Philippa Gardner},
+ Journal = {Electronic Notes in Theoretical Computer Science},
+ Year = {1997},
+ Pages = {52},
+ Volume = {10},
+
+ Abstract = {Action calculi, introduced by Milner, provide a framework for investigating models of interaction. This talk will focus on the connection between action calculi and known concepts arising from type theory. The aim of this work is to isolate what is distinctive about action calculi, and to investigate the potential of action calculi as an underlying framework for many kinds of computational behaviour.The first part of the talk will introduce action calculi. In the second part, I'll give a type-theoretic account of action calculi, using the general binding operators of Aczel. I will discuss two extensions: higher-order action calculi which correspond to Moggi's commutative computational lambda-calculus, and linear action calculi which correspond to the linear type theories of Barber and Benton.This talk is based on joint work with Andrew Barber, Masahito Hasegawa and Gordon Plotkin. If time, I will also describe current work arising from the connections described above. }
+}
+
+@Article{Gardner1995Equivalences,
+ Title = {{Equivalences between Logics and their Representing Type Theories}},
+ Author = {Philippa Gardner},
+ Journal = {Mathematical Structures in Computer Science},
+ Year = {1995},
+ Number = {3},
+ Pages = {323--349},
+ Volume = {5},
+
+ Abstract = {We propose a new framework for representing logics, called LF+, which is based on the Edinburgh Logical Framework. The new framework allows us to give, apparently for the first time, general definitions that capture how well a logic has been represented. These definitions are possible because we are able to distinguish in a generic way that part of the LF+ entailment corresponding to the underlying logic. This distinction does not seem to be possible with other frameworks. Using our definitions, we show that, for example, natural deduction first-order logic can be well-represented in LF, whereas linear and relevant logics cannot. We also show that our syntactic definitions of representation have a simple formulation as indexed isomorphisms, which both confirms that our approach is a natural one and provides a link between type-theoretic and categorical approaches to frameworks.}
+}
+
+@Article{Gardner1995Name,
+ Title = {{A Name-free Account of Action Calculi}},
+ Author = {Philippa Gardner},
+ Journal = {Electronic Notes in Theoretical Computer Science},
+ Year = {1995},
+ Pages = {214--231},
+ Volume = {1},
+
+ Abstract = {Action calculi provide a unifying framework for representing a variety of models of communication, such as CCS, Petri nets and the ?-calculus, within a unified setting. A central idea is to model the interaction between actions using names. We introduce a name-free account of action calculi, called the closed action calculi, and show that there is a strong correspondence between the original presentation and the name-free presentation. These results show that, although names play an important presentational role, they are in some sense inessential.}
}
+@InProceedings{Gardner1994Discovering,
+ Title = {{Discovering Needed Reductions Using Type Theory}},
+ Author = {Philippa Gardner},
+ Booktitle = {Proceeding of the International Conference on Theoretical Aspects of Computer Software (TACS)},
+ Year = {1994},
+ Pages = {555--574},
+
+ Abstract = {The identification of the needed redexes in a term is an undecidable problem. We introduce a (partially decidable) type assignment system, which distinguishes certain redexes called the allowable redexes. For a well-typed term e, allowable redexes are-needed redexes. In addition, with principal typing, all the needed redexes of a normalisable term are allowable. Using these results, we are able to identify all the needed reductions of a principally typed normalisable term. Possible applications of these results include strictness and sharing analysis for functional programming languages, and a reduction strategy for well-typed terms which satisfies Levy's notion of optimal reduction.}
+}
+
+@InProceedings{Gardner1993New,
+ Title = {{A New Type Theory for Representing Logics}},
+ Author = {Philippa Gardner},
+ Booktitle = {Proceedings of the 4\textsuperscript{th} International Conference on Logic Programming and Automated Reasoning (LPAR)},
+ Year = {1993},
+ Pages = {146--157},
+
+ Abstract = {We propose a new type theory for representing logics, called LF+ and based on the Edinburgh Logical Framework. The new framework allows us to give, apparently for the first time, general definitions which capture how well a logic has been represented. Using our definitions, we show that, for example, first-order logic can be wellrepresented in LF+, whereas linear and relevant logics cannot. These syntactic definitions of representation have a simple formulation as indexed isomorphisms, which both confirms that our approach is a natural one, and provides a link between type-theoretic and categorical approaches to frameworks.}
+}
+
+@Article{Gardner1991UnfoldFold,
+ Title = {{Unfold/Fold Transformations in Logic Programming}},
+ Author = {Philippa Gardner},
+ Journal = {Mathematical Structures in Computer Science},
+ Year = {1991},
+ Number = {2},
+ Pages = {143--157},
+ Volume = {02},
+
+ Abstract = {Unfold/fold transformation rules for disjunctive logic programs are proposed in this paper. Our transformation rules preserve the meaning of the programs.}
+}
+
+@InProceedings{Gardner1997Types,
+ Title = {{Types and Models for Higher-Order Action Calculi}},
+ Author = {Philippa Gardner and Masahito Hasegawa},
+ Booktitle = {Proceedings of the 3\textsuperscript{rd} International Symposium on Theoretical Aspects of Computer Software ({TACS})},
+ Year = {1997},
+ Pages = {583--603},
+
+ Abstract = {Milner introduced action calculi as a framework for representing models of interactive behaviour. He also introduced the higher-order action calculi, which add higher-order features to the basic setting. We present type theories for action calculi and higher-order action calculi, and give the categorical models of the higher-order calculi. As applications, we give a semantic proof of the conservativity of higher-order action calculi over action calculi, and a precise connection with Moggi's computational lambda calculus and notions of computation.}
+}
+
+@Article{Gardner2007Linear,
+ Title = {{Linear Forwarders}},
+ Author = {Philippa Gardner and Cosimo Laneve and Lucian Wischik},
+ Journal = {Information and Computation},
+ Year = {2007},
+ Number = {10},
+ Pages = {1526--1550},
+ Volume = {205},
+
+ Abstract = {A linear forwarder is a process that receives one message on a channel and sends it on a different channel. We use linear forwarders to provide a distributed implementation of Milner?s asynchronous pi calculus. Such a distributed implementation is known to be difficult due to input capability, where a received name is used as the subject of a subsequent input. This allows the dynamic creation of large input processes in the wrong place, thus requiring comparatively large code migrations in order to avoid consensus problems. Linear forwarders constitute a small atom of input capability that is easy to move.
+We show that the full input capability can be simply encoded using linear for- warders. We also design a distributed machine, demonstrating the ease with which we can implement the pi calculus using linear forwarders. We also show that lin- ear forwarders allow for a simple encoding of distributed choice and have ?clean? behaviour in the presence of failures.}
+}
+
+@InProceedings{Gardner2003Linear,
+ Title = {{Linear Forwarders}},
+ Author = {Philippa Gardner and Cosimo Laneve and Lucian Wischik},
+ Booktitle = {Proceedings of the 14\textsuperscript{th} International Conference on Concurrency Theory ({CONCUR})},
+ Year = {2003},
+ Pages = {408--422},
+
+ Abstract = {A linear forwarder is a process that receives one message on a channel and sends it on a different channel. We use linear forwarders to provide a distributed implementation of Milner?s asynchronous pi calculus. Such a distributed implementation is known to be difficult due to input capability, where a received name is used as the subject of a subsequent input. This allows the dynamic creation of large input processes in the wrong place, thus requiring comparatively large code migrations in order to avoid consensus problems. Linear forwarders constitute a small atom of input capability that is easy to move.
+We show that the full input capability can be simply encoded using linear for- warders. We also design a distributed machine, demonstrating the ease with which we can implement the pi calculus using linear forwarders. We also show that linear forwarders allow for a simple encoding of distributed choice and have ?clean? behaviour in the presence of failures.}
+}
+
+@InProceedings{Gardner2002Fusion,
+ Title = {{The Fusion Machine}},
+ Author = {Philippa Gardner and Cosimo Laneve and Lucian Wischik},
+ Booktitle = {Proceedings of the 13\textsuperscript{th} International Conference on Concurrency Theory ({CONCUR}) 2002},
+ Year = {2002},
+ Pages = {418--433},
+
+ Abstract = {We present a new model for the distributed implementation of pi-like calculi, which permits strong correctness results that are simple to prove. We describe the distributed channel machine -- a distributed version of a machine proposed by Cardelli. The distributed channel machine groups pi processes at their channels (or locations), in contrast with the more common approach of incorporating additional location information within pi processes. We go on to describe the fusion machine. It uses a form of concurrent constraints called fusions -- equations on channel names -- to distribute fragments of these processes between remote channels. This fragmentation avoids the movement of large continuations between locations, and leads to a more efficient implementation model.}
+}
+
+@Article{Gardner2005Modelling,
+ Title = {{Modelling Dynamic Web Data}},
+ Author = {Philippa Gardner and Sergio Maffeis},
+ Journal = {Theoretical Computer Science},
+ Year = {2005},
+ Number = {1},
+ Pages = {104--131},
+ Volume = {342},
+
+ Abstract = {We introduce Xd?, a peer-to-peer model for reasoning about the dynamic behaviour of web data. It is based on an idealised model of semi-structured data, and an extension of the $\pi$-calculus with process mobility and with an operation for interacting with data. Our model can be used to reason about behaviour found in, for example, dynamic web page programming, applet interaction, and service orchestration. We study behavioural equivalences for Xd$\pi$, motivated by examples.}
+}
+
+@InProceedings{Gardner2003Modelling,
+ Title = {{Modelling Dynamic Web Data}},
+ Author = {Philippa Gardner and Sergio Maffeis},
+ Booktitle = {Proceedings of 9\textsuperscript{th} International Workshop on Database Programming Languages ({DBPL})},
+ Year = {2003},
+ Pages = {130--146},
+
+ Abstract = {We introduce Xd$\pi$, a peer-to-peer model for reasoning about the dynamic behaviour of web
+ data. It is based on an idealised model of semi- structured data, and an extension of the ?-calculus with process
+ mobility and with an operation for interacting with data. Our model can be used to reason about behaviour found
+ in, for example, dynamic web page program- ming, applet interaction, and service orchestration. We study
+ behavioural equivalences for Xd$\pi$, motivated by examples.}
+}
+
+@InProceedings{Gardner2012Towards,
+ Title = {{Towards a Program Logic for JavaScript}},
+ Author = {Philippa Gardner and Sergio Maffeis and Gareth Smith},
+ Booktitle = {Proceedings of the 39\textsuperscript{th} {ACM} {SIGPLAN-SIGACT} Symposium on Principles of Programming Languages ({POPL})},
+ Year = {2012},
+ Pages = {31--44},
+
+ Abstract = {JavaScript has become the most widely used language for client- side web programming. The dynamic nature of JavaScript makes understanding its code notoriously difficult, leading to buggy pro- grams and a lack of adequate static-analysis tools. We believe that logical reasoning has much to offer JavaScript: a simple description of program behaviour, a clear understanding of module boundaries, and the ability to verify security contracts.
+We introduce a program logic for reasoning about a broad subset of JavaScript, including challenging features such as prototype inheritance and with. We adapt ideas from separation logic to provide tractable reasoning about JavaScript code: reasoning about easy programs is easy; reasoning about hard programs is possible. We prove a strong soundness result. All libraries written in our subset and proved correct with respect to their specifications will be well-behaved, even when called by arbitrary JavaScript code.}
+}
+
+@InProceedings{Gardner2014Local,
+ Title = {{Local Reasoning for the {POSIX} File System}},
+ Author = {Philippa Gardner and Gian Ntzik and Adam Wright},
+ Booktitle = {Proceedings of the 23\textsuperscript{rd} European Symposium on Programming ({ESOP})},
+ Year = {2014},
+ Pages = {169--188},
+
+ Abstract = {We provide a program logic for specifying a core subset of the sequential POSIX file system, and for reasoning abstractly about client programs working with the file system.}
+}
+
+@Article{Gardner2014Abstract,
+ Title = {{Abstract Local Reasoning for Concurrent Libraries: Mind the Gap}},
+ Author = {Philippa Gardner and Azalea Raad and Mark J. Wheelhouse and Adam Wright},
+ Journal = {Proceedings of the 30\textsuperscript{th} Conference on the Mathematical Foundations of Programming Semantics ({MFPS})},
+ Year = {2014},
+ Pages = {147--166},
+ Volume = {308},
+
+ Abstract = {We study abstract local reasoning for concurrent libraries. There are two main approaches: provide a specification of a library by abstracting from concrete reasoning about an implementation; or provide a direct abstract library specification, justified by refining to an implementation. Both approaches have a significant gap in their reasoning, due to a mismatch between the abstract connectivity of the abstract data structures and the concrete connectivity of the concrete heap representations. We demonstrate this gap using structural separation logic (SSL) for specifying a concurrent tree library and concurrent abstract predicates (CAP) for reasoning about a concrete tree implementation. The gap between the abstract and concrete connectivity emerges as a mismatch between the SSL tree predicates and CAP heap predicates. This gap is closed by an interface function I which links the abstract and concrete connectivity. In the accompanying technical report, we generalise our SSL reasoning and results to arbitrary concurrent data libraries.}
+}
+
+@InProceedings{Gardner2015Trusted,
+ Title = {{A Trusted Mechanised Specification of JavaScript: One Year On}},
+ Author = {Philippa Gardner and Gareth Smith and Conrad Watt and Thomas Wood},
+ Booktitle = {Proceedings of the 27\textsuperscript{th} International Conference on Computer Aided Verification ({CAV})},
+ Year = {2015},
+ Pages = {3--10},
+
+ Abstract = {The JSCert project provides a Coq mechanised specification of the core JavaScript language. A key part of the project was to develop a methodology for establishing trust, by designing JSCert in such a way as to provide a strong connection with the JavaScript standard, and by developing JSRef, a reference interpreter which was proved correct with respect to JSCert and tested using the standard Test262 test suite. In this paper, we assess the previous state of the project at POPL?14 and the current state of the project at CAV?15. We evaluate the work of POPL?14, providing an analysis of the methodology as a whole and a more detailed analysis of the tests. We also describe recent work on extending JSRef to include Google?s V8 Array library, enabling us to cover more of the language and to pass more tests.}
+}
+
+@InProceedings{Gardner2008DOM,
+ Title = {{DOM: Towards a Formal Specification}},
+ Author = {Philippa Gardner and Gareth Smith and Mark J. Wheelhouse and Uri Zarfaty},
+ Booktitle = {Proceedings of the {ACM} {SIGPLAN} Workshop on Programming Language Technologies for XML ({PLAN-X})},
+ Year = {2008},
+
+ Abstract = {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 work with a minimal set of commands and obtain a complete reasoning for straight-line code. Our work transfers O?Hearn, Reynolds and 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 Zarfaty on local Hoare reasoning about a simple tree-update language to DOM, showing that our reasoning scales to DOM. Our reasoning not only formally specifies a significant subset of DOM Core Level 1, but can also be used to verify e.g. invariant properties of simple Javascript programs.}
+}
+
+@InProceedings{Gardner2008Local,
+ Title = {{Local Hoare Reasoning about {DOM}}},
+ Author = {Philippa Gardner and Gareth Smith and Mark J. Wheelhouse and Uri Zarfaty},
+ Booktitle = {Proceedings of the 27\textsuperscript{th} {ACM} {SIGMOD-SIGACT-SIGART} Symposium on Principles of Database Systems ({PODS})},
+ Year = {2008},
+ Pages = {261--270},
+
+ Abstract = {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 work with a minimal set of commands and obtain a complete reasoning for straight-line code. Our work transfers O?Hearn, Reynolds and 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 Zarfaty on local Hoare reasoning about simple tree update to this real-world DOM application. Our reasoning not only formally specifies a significant subset of DOM Core Level 1, but can also be used to verify, for example, invariant properties of simple Javascript programs.}
+}
+
+@InProceedings{Gardner2009Small,
+ Title = {{Small Specifications for Tree Update}},
+ Author = {Philippa Gardner and Mark J. Wheelhouse},
+ Booktitle = {Proceedings of the 6\textsuperscript{th} International Workshop on Web Services and Formal Methods ({WS-FM})},
+ Year = {2009},
+ Pages = {178--195},
+
+ 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.}
+}
+
+@InProceedings{Gardner2000Explicit,
+ Title = {{Explicit Fusions}},
+ Author = {Philippa Gardner and Lucian Wischik},
+ Booktitle = {Proceedings of the 25\textsuperscript{th} International Symposium on Mathematical Foundations of Computer Science ({MFCS})},
+ Year = {2000},
+ Pages = {373--382},
+
+ Abstract = {We introduce explicit fusions of names. An explicit fusion is a process that exists concurrently with the rest of the system and enables two names to be used interchangeably. Explicit fusions provide a small-step account of reaction in process calculi such as the pi calculus and the fusion calculus. In this respect they are similar to the explicit substitutions of Abadi, Cardelli and Curien, which do the same for the lambda calculus. In this paper, we give a technical foundation for explicit fusions. We present the pi-F calculus, a simple process calculus with explicit fusions, and define a strong bisimulation congruence. We study the embeddings of the fusion calculus and the pi calculus. The former is fully abstract with respect to bisimulation.}
+}
+
+@InProceedings{Gardner2007Introduction,
+ Title = {{An Introduction to Context Logic}},
+ Author = {Philippa Gardner and Uri Zarfaty},
+ Booktitle = {Proceedings of the 14\textsuperscript{th} International Workshop on Logic, Language, Information and Computation (WoLLIC)},
+ Year = {2007},
+ Pages = {189--202},
+
+ 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].}
+}
+
+@Article{LWPG2005Explicit,
+ Title = {{Explicit Fusions}},
+ Author = {{Lucian Wischik and Philippa Gardner}},
+ Journal = {Theoretical Computer Science},
+ Year = {2005},
+ Number = {3},
+ Pages = {606--630},
+ Volume = {340},
+
+ Abstract = {We introduce explicit fusions of names. An explicit fusion is a process that exists concurrently with the rest of the system and enables two names to be used interchangeably. Explicit fusions provide a small-step account of reaction in process calculi such as the pi calculus and the fusion calculus. In this respect they are similar to the explicit substitutions of Abadi, Cardelli and Curien, which do the same for the lambda calculus. In this paper, we give a technical foundation for explicit fusions. We present the pi-F calculus, a simple process calculus with explicit fusions, and define a strong bisimulation congruence. We study the embeddings of the fusion calculus and the pi calculus. The former is fully abstract with respect to bisimulation.}
+}
+
+@Article{Maffeis2008Behavioural,
+ Title = {{Behavioural Equivalences for Dynamic Web Data}},
+ Author = {Sergio Maffeis and Philippa Gardner},
+ Journal = {Logic and Algebraic Programming},
+ Year = {2008},
+ Number = {1},
+ Pages = {86--138},
+ Volume = {75},
+
+ Abstract = {We study behavioural equivalences for dynamic web data in Xdn, a model for reasoning about behaviour found in (for example) dynamic web page programming, applet interaction, and web-service orchestration. Xdn is based on an idealised model of semistructured data, and an extension of the 7r-calculus with locations and operations for interacting with data. The equivalences are nonstandard due to the integration of data and processes, and the presence of locations. }
+}
+
+@InProceedings{Maffeis2004Behavioural,
+ Title = {{Behavioural Equivalences for Dynamic Web Data}},
+ Author = {Sergio Maffeis and Philippa Gardner},
+ Booktitle = {Proceedings of 3\textsuperscript{rd} International Conference on Theoretical Computer Science {TCS}},
+ Year = {2004},
+ Pages = {535--548},
+
+ Abstract = {We study behavioural equivalences for dynamic web data in Xd$\pi$, a model for reasoning about behaviour found in (for example) dynamic web page programming, applet interaction, and web-service orchestration. Xd$\pi$ is based on an idealised model of semistructured data, and an extension of the 7r-calculus with locations and operations for interacting with data. The equivalences are nonstandard due to the integration of data and processes, and the presence of locations.}
+}
+
+@InProceedings{Ntzik2015Reasoning,
+ Title = {{Reasoning about the POSIX File System: Local Update and Global Pathnames}},
+ Author = {Gian Ntzik and Philippa Gardner},
+ Booktitle = {Proceedings of the 30\textsuperscript{th} Annual {ACM} {SIGPLAN} Conference on Object-Oriented Programming, Systems, Languages, and Applications ({OOPSLA})},
+ Year = {2015},
+ Note = {(Awaiting Publication)},
+
+ Abstract = {We introduce a program logic for specifying a core sequential subset of the POSIX file system and for reasoning abstractly about client programs working with the file system. The challenge is to reason about the combination of local directory update and global pathname traversal (including ?..? and symbolic links) which may overlap the directories be- ing updated. Existing reasoning techniques are either based on first-order logic and do not scale, or on separation logic and can only handle linear pathnames (no ?..? or symbolic links). We introduce fusion logic for reasoning about local update and global pathname traversal, introducing a novel effect frame rule to propagate the effect of a local update on overlapping pathnames. We apply our reasoning to the standard recursive remove utility (rm -r), discovering bugs in well-known implementations.}
+}
+
+@InProceedings{Ntzik2015Fault,
+ Title = {{Fault-tolerant Resource Reasoning}},
+ Author = {Gian Ntzik and Pedro da Rocha Pinto and Philippa Gardner},
+ Booktitle = {Proceedings of the 13\textsuperscript{th} Asian Symposium on Programming Languages and Systems ({APLAS})},
+ Year = {2015},
+ Note = {(Awaiting Publication)$^*$},
+
+ Abstract = {Separation logic has been successful at verifying that pro- grams do not crash due to illegal use of resources. The underlying assumption, however, is that machines do not fail. In practice, machines can fail unpredictably for various reasons, e.g. power loss, corrupting resources. Critical software, e.g. file systems, employ recovery methods to mitigate these effects. We introduce an extension of the Views framework to reason about such methods. We use concurrent separation logic as an instance of the framework to illustrate our reasoning, and explore programs using write-ahead logging, e.g. an ARIES recovery algorithm.}
+}
+
+@InProceedings{Raad2015CoLoSL,
+ Title = {{CoLoSL: Concurrent Local Subjective Logic}},
+ Author = {Azalea Raad and Jules Villard and Philippa Gardner},
+ Booktitle = {Proceedings of the 24\textsuperscript{th} European Symposium on Programming ({ESOP})},
+ Year = {2015},
+ Pages = {710--735},
+
+ Abstract = {A key difficulty in verifying shared-memory concurrent pro- grams is reasoning compositionally about each thread in isolation. Existing verification techniques for fine-grained concurrency typically require reasoning about either the entire shared state or disjoint parts of the shared state, impeding compositionality. This paper introduces the program logic CoLoSL, where each thread is verified with respect to its subjective view of the global shared state. This subjective view describes only that part of the state accessed by the thread. Subjective views may arbitrarily overlap with each other, and expand and contract depending on the resource required by the thread. This flexibility gives rise to small specifications and, hence, more compositional reasoning for concurrent programs. We demonstrate our reasoning on a range of examples, including a concurrent computation of a spanning tree of a graph.}
+}
+
+@InProceedings{Raza2009Automatic,
+ Title = {{Automatic Parallelization with Separation Logic}},
+ Author = {Mohammad Raza and Cristiano Calcagno and Philippa Gardner},
+ Booktitle = {Proceedings of the 18\textsuperscript{th} European Symposium on Programming ({ESOP})},
+ Year = {2009},
+ Pages = {348--362},
+
+ Abstract = {We present a separation logic framework which can express proper- ties of memory separation between different points in a program. We describe an algorithm based on this framework for determining independences between statements in a program which can be used for parallelization.}
+}
+
+@Article{Raza2009Footprints,
+ Title = {{Footprints in Local Reasoning}},
+ Author = {Mohammad Raza and Philippa Gardner},
+ Journal = {Logical Methods in Computer Science},
+ Year = {2009},
+ Number = {2},
+ Volume = {5},
+
+ Abstract = {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 investigate the conditions under which the footprints correspond to the smallest safe states, and present a heap model in which, unlike the standard model, this is the case for every program.}
+}
+
+@InProceedings{Raza2008Footprints,
+ Title = {{Footprints in Local Reasoning}},
+ Author = {Mohammad Raza and Philippa Gardner},
+ Booktitle = {Proceedings of the 11\textsuperscript{th} International Conference on Foundations of Software Science and Computational Structures ({FOSSACS})},
+ Year = {2008},
+ Pages = {201--215},
+
+ Abstract = {We present a separation logic framework which can express proper- ties of memory separation between different points in a program. We describe an algorithm based on this framework for determining independences between statements in a program which can be used for parallelization.}
+}
+
+@InProceedings{RochaPinto2011Simple,
+ Title = {{A Simple Abstraction for Complex Concurrent Indexes}},
+ Author = {Pedro da Rocha Pinto and Thomas Dinsdale{-}Young and Mike Dodds and Philippa Gardner and Mark J. Wheelhouse},
+ Booktitle = {Proceedings of the 26\textsuperscript{th} Annual {ACM} {SIGPLAN} Conference on Object-Oriented Programming, Systems, Languages, and Applications ({OOPSLA})},
+ Year = {2011},
+ Pages = {845--864},
+
+ Abstract = {Indexes are ubiquitous. Examples include associative arrays, dictionaries, maps and hashes used in applications such as databases, file systems and dynamic languages. Abstractly, a sequential index can be viewed as a partial function from keys to values. Values can be queried by their keys, and the index can be mutated by adding or removing mappings. Whilst appealingly simple, this abstract specification is in- sufficient for reasoning about indexes that are accessed con- currently.
+We present an abstract specification for concurrent indexes. We verify several representative concurrent client applications using our specification, demonstrating that clients can reason abstractly without having to consider specific underlying implementations. Our specification would, how- ever, mean nothing if it were not satisfied by standard implementations of concurrent indexes. We verify that our specification is satisfied by algorithms based on linked lists, hash tables and BLink trees. The complexity of these algorithms, in particular the BLink tree algorithm, can be completely hidden from the client?s view by our abstract specification.}
+}
+
+@InProceedings{RochaPinto2014TaDA,
+ Title = {{TaDA: A Logic for Time and Data Abstraction}},
+ Author = {Pedro da Rocha Pinto and Thomas Dinsdale{-}Young and Philippa Gardner},
+ Booktitle = {Proceedings of the 28\textsuperscript{th} European Conference on Object-Oriented Programming ({ECOOP})},
+ Year = {2014},
+ Pages = {207--231},
+
+ Abstract = {To avoid data races, concurrent operations should either be at distinct times or on distinct data. Atomicity is the abstraction that an operation takes effect at a single, discrete instant in time, with linearisability being a well-known correctness condition which asserts that concurrent operations appear to behave atomically. Disjointness is the abstraction that operations act on distinct data resource, with concur- rent separation logics enabling reasoning about threads that appear to operate independently on disjoint resources.
+Building on separation logic with concurrent abstract predicates (CAP), we introduce TaDA, a program logic which combines the benefits of abstract atomicity and abstract disjointness. We give several examples: an atomic lock module, a CAP example with a twist, which cannot be done using linearisability; an atomic MCAS module implemented using our lock module, a classic linearisability example which cannot be done us- ing CAP; and a double-ended queue module implemented using MCAS.}
+}
+
+@InProceedings{RochaPinto2015Steps,
+ Title = {{Steps in Modular Specifications for Concurrent Modules}},
+ Author = {Pedro da Rocha Pinto and Thomas Dinsdale-Young and Philippa Gardner},
+ Booktitle = {Proceedings of the 31\textsuperscript{st} Conference on the Mathematical Foundations of Programming Semantics},
+ Year = {2015},
+
+ Abstract = {The specification of a concurrent program module is a difficult problem. The specifications must be strong enough to enable reasoning about the intended clients without reference to the underlying module implementation. We survey a range of verification techniques for specifying concurrent modules, in particular highlighting four key concepts: auxiliary state, interference abstraction, resource ownership and atomicity. We show how these concepts combine to provide powerful approaches to specifying concurrent modules.}
+}
+
+@InProceedings{RochaPinto2016Modular,
+ Title = {Modular Termination Verification for Non-blocking Concurrency},
+ Author = {Pedro da Rocha Pinto and Thomas Dinsdale-Young and Philippa Gardner and Julian Sutherland},
+ Booktitle = {Proceedings of the 25\textsuperscript{th} European Symposium on Programming ({ESOP})},
+ Year = {2016},
+
+ Abstract = {We present Total-TaDA, a program logic for verifying the total correctness of concurrent programs: that such programs both terminate and produce the correct result. With Total-TaDA, we can specify constraints on a thread?s concurrent environment that are necessary to guarantee termination. This allows us to verify total correctness for non-blocking algorithms, e.g. a counter and a stack. Our specifications can express lock- and wait-freedom. More generally, they can express that one operation cannot impede the progress of another, a new non-blocking property we call non-impedance. Moreover, our approach is modular. We can verify the operations of a module independently, and build up modules on top of each other.}
+}
+
+@InProceedings{Wischik2004Strong,
+ Title = {{Strong Bisimulation for the Explicit Fusion Calculus}},
+ Author = {Lucian Wischik and Philippa Gardner},
+ Booktitle = {Proceedings of the 7\textsuperscript{th} International Conference on Foundations of Software Science and Computation Structures ({FOSSACS})},
+ Year = {2004},
+ Pages = {484--498},
+
+ Abstract = {The pi calculus holds the promise of compile-time checks for whether a given program will have the correct interactive behaviour.}
+}
--
GitLab