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.}
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},
...
...
@@ -247,104 +237,6 @@ throughout the proof.}
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},
