Philippa Gardner

TACAS Conference 2026 Conference Paper

Gillian Debugging: Swinging Through the (Compositional Symbolic Execution) Trees

• Nat Karmios
• Sacha-Élie Ayoun
• Philippa Gardner

TCS Journal 2012 Journal Article

Processes in space

• Luca Cardelli
• Philippa Gardner

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.

I&C Journal 2010 Journal Article

Adjunct elimination in Context Logic for trees

• Cristiano Calcagno
• Thomas Dinsdale-Young
• Philippa Gardner

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.

TCS Journal 2009 Journal Article

A process model of Rho GTP-binding proteins

• Luca Cardelli
• Emmanuelle Caron
• Philippa Gardner
• Ozan Kahramanoğulları
• Andrew Phillips

Rho GTP-binding proteins play a key role as molecular switches in many cellular activities. In response to extracellular stimuli and with the help of 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 GDI regulators 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 instances of the same parametric model.

I&C Journal 2007 Journal Article

Expressiveness and complexity of graph logic

• Anuj Dawar
• Philippa Gardner
• Giorgio Ghelli

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.

I&C Journal 2007 Journal Article

Linear forwarders

• Philippa Gardner
• Cosimo Laneve
• Lucian Wischik

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 forwarders. 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.

TCS Journal 2006 Journal Article

Editorial

• Philippa Gardner
• Nobuko Yoshida

TCS Journal 2005 Journal Article

Explicit fusions

• Lucian Wischik
• Philippa Gardner

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.

TCS Journal 2005 Journal Article

Modelling dynamic web data

• Philippa Gardner
• Sergio Maffeis

We introduce the X d π calculus, a peer-to-peer model for reasoning about dynamic web data. Web data is not just stored statically. Rather it is referenced indirectly, for example using hyperlinks, service calls, or scripts for dynamically accessing data, which require the complex coordination of data and processes between sites. The X d π calculus models this coordination by integrating the XML data structure with process orchestration techniques associated with the distributed pi-calculus. We study behavioural equivalences for X d π, to analyze the various possible patterns of data and process interaction.

MFCS Conference 2000 Conference Paper

Explicit Fusions

• Philippa Gardner
• Lucian Wischik

Abstract We introduce explicit fusions of names. To ‘fuse’ two names is to declare that they may be used interchangeably. An explicit fusion is one that can exist in parallel with some other process, allowing us to ask for instance how a process might behave in a context where x = y. We present the πF -calculus, a simple process calculus with explicit fusions. It is similar in many respects to the fusion calculus but has a simple local reaction relation. We give embeddings of the π-calculus and the fusion calculus. We provide a bisimulation congruence for the π F -calculus and compare it with hyper-equivalence in the fusion calculus.

TCS Journal 1999 Journal Article

Closed action calculi

• Philippa Gardner

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.

CSL Conference 1998 Conference Paper

From Action Calculi to Linear Logic

• Andrew G. Barber
• Philippa Gardner
• Masahito Hasegawa
• Gordon D. Plotkin

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.

LPAR Conference 1993 Conference Paper

A New Type Theory for Representing Logics

• Philippa Gardner

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.