images + bibs

_bibfiles/pgardner-conference-not-refereed.bib

+%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
+throughout the proof.}
+}
\ No newline at end of file

_bibfiles/pgardner-journal-refereed.bib

+@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.}, 
+}
+
+