Publications
122 results found
Gardner P, Dawar A, Ghelli G, 2005, Expressiveness and complexity of graph logic, CONFERENCE TITLE OR JOURNAL NAME IS NEEDED
Calcagno C, Gardner P, Zarfaty U, 2005, Context logic and tree update, Symposium on Principles of Programming Languages, Pages: 271-282, ISSN: 0362-1340
Calcagno C, Gardner P, Hague M, et al., 2005, From separation logic to first-order logic, Berlin, 8th international conference on foundations of software science and computation structures, Edinburgh, Scotland, 4 - 8 April 2005, Publisher: Springer-Verlag Berlin, Pages: 395-409
Dawar A, Gardner P, Ghelli G, 2004, Expressiveness and complexity of graph logic, Departmental Technical Report: 04/3, Publisher: Department of Computing, Imperial College London, 04/3
We investigate the complexity and expressive power of the spatial logic for queryinggraphs introduced by Cardelli, Gardner and Ghelli (ICALP 2002).We show that the model-checkingcomplexity of versions of this logic with and without recursion is PSPACE-complete. In terms ofexpressive power, the version without recursion is a fragment of the monadic second-order logicof graphs and we show that it can express complete problems at every level of the polynomialhierarchy. We also show that it can define all regular languages, when interpretation is restricted tostrings. The expressive power of the logic with recursion is much greater as it can express propertiesthat are PSPACE-complete and therefore unlikely to be definable in second-order logic.
Dawar A, Gardner P, Ghelli G, 2004, Adjunct elimination through games in static ambient logic (extended abstract), Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), Vol: 3328, Pages: 211-223, ISSN: 0302-9743
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. © Springer-Verlag Berlin Heidelberg 2004.
Gardelli L, Gardner P, Ghelli G, 2004, Manipulating trees with hidden labels, Departmental Technical Report: 04/4, Publisher: Department of Computing, Imperial College London, 04/4
We define an operational semantics and a type system for manipulatingsemistructured data that contains hidden information. The data model is simple labeledtrees with a hiding operator. Data manipulation is based on pattern matching,with types that track the use of hidden labels.
Dawar A, Gardner P, Ghelli G, 2004, Adjunct elimination through games in static ambient logic, 24th International Conference on Foundations of Software Technology and Theoretical Computer Science, Publisher: SPRINGER-VERLAG BERLIN, Pages: 211-223, ISSN: 0302-9743
- Author Web Link
- Cite
- Citations: 11
Gardner P, Maffeis S, Gardner P, et al., 2004, Modelling dynamic web data, Berlin, 9th international workshop on data bases and programming languages Potsdam, Germany, 2003, Publisher: Springer-Verlag, Pages: 130-146
Berger M, 2004, Basic theory of reduction congruence for two timed asynchronous Pi-calculi, Berlin, 15th international conference on concurrency theory, Royal Society, London, England, Publisher: Springer-Verlag, Pages: 115-130
Wischik L, Gardner P, 2004, Strong bisimulation for the explicit fusion calculus, Berlin, 7th international conference on foundations of software science and computation structures, Barcelona, Spain, Publisher: Springer-Verlag, Pages: 484-498
Maffeis S, Gardner P, Maffeis S, et al., 2004, Behavioural equivalences for dynamic web data, Dordrecht, IFIP WCC-TCS'04 3rd international conference on theoretical computer science held at the 18th world computer congress, Toulouse, France, 22 - 27 August 2004, Publisher: Springer, Pages: 535-548
Gardner P, Yoshida N, Gardner P, et al., 2004, CONCUR 2004 - concurrency theory: 15th international conference, London, UK, 31 August - 3 September 2004, London, Publisher: Springer, ISBN: 9783540229407
Gardner P, Maffeis S, 2003, Modelling dynamic web data, Departmental Technical Report: 03/14, Publisher: Department of Computing, Imperial College London, 03/14
We introduce Xd¼, a peer-to-peer model for reasoning about the dynamicbehaviour of web data. It is based on an idealised model of semistructureddata, and an extension of the ¼-calculus with process mobilityand with operations for interacting with data. Our model can be usedto reason about behaviour found in, for example, dynamic web page programming,applet interaction, and service orchestration. We study behaviouralequivalences for Xd¼, motivated by examples.
Cardelli L, Gardner P, Ghelli G, et al., 2003, Manipulating trees with hidden labels, Berlin, Joint European conference on theory and practice of software (ETAPS 2003), Warsaw, Poland, Publisher: Springer, Pages: 216-232, ISSN: 0302-9743
Gardner P, Laneve C, Wischik L, 2003, Linear forwarders, Berlin, 14th international conference on concurrency theory, Marseille, France, 2003, Publisher: Springer-Verlag, Pages: 415-430
Gardner P, Maffeis S, 2003, Modelling dynamic web data, Departmental technical report, 2003/14, Publisher: Imperial College of Science, Technology and Medicine, Department of Computing, 14
Gardner P, Laneve C, Wischik L, 2002, The fusion machine, Pages: 418-433, ISSN: 0302-9743
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. © Springer-Verlag Berlin Heidelberg 2002.
Gardner P, Laneve C, Wischik L, 2002, The fusion machine (Extended abstract), Berlin, 13th international conference on concurrency theory, CONCUR 2002, Brno, Czech Republic, 2002, Publisher: Springer Verlag, Pages: 418-433
Cardelli L, Gardner P, Ghelli G, 2002, A spatial logic for querying graphs, Berlin, 29th international colloquium on automata, languages and programming, Malaga, Spain, 2002, Publisher: Springer-Verlag, Pages: 597-610
Cardelli L, Gardner P, Ghelli G, 2002, A spatial logic for querying graphs, Berlin, 29th international colloquium on automata, languages and programming, Malaga, Spain, 2002, Publisher: Springer-Verlag, Pages: 597-610
Gardner P, Wischik L, 2000, Explicit fusions, Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), Vol: 1893, Pages: 373-382, ISSN: 0302-9743
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.
Gardner PA, Wischik L, 2000, Explicit Fusions, Mathematical Foundations of Programming Semantics MFPS 2000
Gardner P, 1999, Closed action calculi, Theoretical Computer Science, Vol: 228, Pages: 77-103, ISSN: 0304-3975
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. © 1999 Published by Elsevier Science B.V. All rights reserved.
Gardner P, 1998, A type-theoretic description of action calculi, ISSN: 1571-0661
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. © Elsevier B.V.
Barber A, Gardner P, Hasegawa M, et al., 1998, From action calculi to linear logic, Pages: 78-97, ISSN: 0302-9743
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.
Gardner P, Hasegawa M, 1997, Types and models for higher-order action calculi, Pages: 583-603, ISSN: 0302-9743
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.
Gardner P, 1995, Equivalences Between Logics and Their Representing Type Theories, Mathematical Structures in Computer Science, Vol: 5, Pages: 323-349, ISSN: 0960-1295
- Cite
- Citations: 3
Gardner P, 1995, A Name-free Account of Action Calculi, Electronic Notes in Theoretical Computer Science, Vol: 1, Pages: 214-231, ISSN: 1571-0661
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. © 2000.
This data is extracted from the Web of Science and reproduced under a licence from Thomson Reuters. You may not copy or re-distribute this data in whole or in part without the written consent of the Science business of Thomson Reuters.