Selected Publications

2009

  • Small Specifications for Tree Update (with Wheelhouse), WS-FM.

  • Automatic Parallelization using Separation Logic (with Raza), ESOP.

  • Footprints in Local Reasoning (with Raza), Journal of Logical Methods in Computer Science, to appear.

  • Adjunct Elimination in Context Logic for Trees (with Cristiano Calcagno and Thomas Dinsale-Young), Journal of Information and Computation, to appear.

  • A Process Model with Rho GTP-binding Proteins in the Context Of Phagocytosis (with Cardelli, Caron, Kahramanogullari), Journal of Theoretical Computer Science, to appear.

  • Decidability and Expressivity Results for Context Logic (with Cristiano Calcagno and Dinsdale-Young), submitted.

    2008

  • Local Hoare Reasoning about DOM (with Gareth Smith, mark Wheelhouse and Uri Zarfaty), PODS.

  • Footprints in Local Reasoning (with Raza), FOSSACS.

  • Reasoning about High-level Tree Update and its Low-level Implementation (with Zarfaty), technical report based on a talk given at Separationfest in Queen Mary College for Reynolds.

    2007

  • Context Logic and Tree Update (Uri Zarfaty's thesis), Imperial, 2007.

  • Context Logic as Modal Logic: Completeness and Parametric Inexpressivity (with Cristiano Calcagno and Uri Zarfaty), POPL.

  • Local Reasoning about Data Update (with Cristiano Calcagno and Uri Zarfaty), in the festschrift "Computation, Meaning and Logic: Articles dedicated to Gordon Plotkin", ENTCS.

  • Manipulating Trees with Hidden Labels (with Luca Cardelli and Giorgio Ghelli), in the festschrift "Computation, Meaning and Logic: Articles dedicated to Gordon Plotkin", ENTCS.

  • Adjunct Elimination in Context Logic for Trees (with Calcagno and Dinsdale-Young), Asian Symposium of Programming Languages and Systems (APLAS).

  • Behaviour of Dynamic Web Data (with Maffeis), Journal of Logic and Algebraic Programming, special issue associated with Algebraic Process Calculi: the First Thenty Five Years and Beyond.

  • Linear Forwarders (with Laneve and Wischik), Journal of Information and Computation.

    2006

  • Local Reasoning about Tree Update (with Uri Zarfaty), MFPS 2006.

  • Expressiveness and Complexity of Graph Logic (with Anuj Dawar and Giorgio Ghelli), Journal of Information and Computation, 2006.

  • International Conference in Concurrency (editor with Yoshida), Journal of Theoretical Computer Science, special issue in association with CONCUR 2004.

    2005

  • Context Logic and Tree Update (with Cristiano Calcagno and Uri Zarfaty), POPL 2005.

    A Note on Context Logic, notes accompanying a lecture course for the Appsem 2005 summer school.

  • From Separation Logic to First-order Logic (with Cristiano Calcagno and Matthew Hague), FOSSACS 2005.

  • Ubiquitous Data(with Gavin Bierman and Peter Buneman), Ubinet workshop, 2005.

  • Modelling Dynamic Web Data (with Maffeis), Journal of Theoretical Computer Science.

  • Adjunt Elimination through Games in Static Ambient Logic (with Dawar and Ghelli), FSTTCS.

    2004

  • Spatial Adjunct Elimination Using Enrenfeuch's Games (with Anuj Dawar and Giorgio Ghelli), FSTTCS 2004.

  • Strong Bisimulation for the Explicit Fusion Calculus (with Lucian Wischik), FOSSACS 2004.

  • Explicit Fusions (with Wischik), Journal of Theoretical Computer Science.

  • Dynamic Web Data: Theory and Experiment, (with N. Yoshida, S.Maffeis and A. Ahern), Poster presented at EPSRC e-Science Meeting 2004 , Edinburgh.

  • Behavioural Equivalences for Dynamic Web Data(with S.Maffeis), IFIP-TCS 2004 .

    2003

  • Manipulating Trees with Hiding (with Luca Cardelli and Giorgio Ghelli), FOSSACS 2003.

  • Modelling Dynamic Web Data (with S.Maffeis), to appear in TCS. A preliminary paper appeared at DBPL'03.

  • Linear Forwarders (with Lucian Wischik and Cosimo Laneve), CONCUR.

  • Manipulating Trees with Hiding (with Cardelli and Ghelli), FOSSACS.

    2002

  • A Spatial Logic for Querying Graphs (with Luca Cardelli and Giorgio Ghelli), ICALP 2002.

  • The Fusion Machine (with Lucian Wischik and Cosimo Laneve), Concur 2002.

    2000

  • Explicit Fusions (with Lucian Wischik), journal paper accepted to TCS. Conference version appeared in MFPS 2000.

  • From Process Calculi to Process Frameworks, invited submission, Concur 2000.

    Before 2000, selected papers

  • Symmetric Action Calculi (with Lucian Wischik), manuscript, 1999.

  • From Action Calculi to Linear Logic (with A. Barber, M. Hasegawa and G. Plotkin), selected papers from the European Association for Computer Science Logic, 1998.

  • Higher-order and reflexive action calculi: their type theory and models (with M. Hasegawa), Theoretical Aspects of Computer Software, Japan, 1997.

  • Closed Action Calculi, Journal of Theoretical Computer Science, invited submission in association with the conference on Mathematical Foundations in Programming Semantics, 1999; a shorter version of this paper appears in Mathematical Foundations of Programming Semantics, New Orleans, 1995.

  • Equivalences between Logics and their Representing Type Theories, Journal of Mathematical Structures in Computer Science, 1995.

  • Discovering Needed Reductions Using Type Theory, Theoretical Aspects of Computer Software, Sendai, Japan, 1994.

  • Representing Logics in Type Theory, PhD Thesis, Edinburgh, supervised by Gordon Plotkin, 1992. Available as an Edinburgh technical report.

  • Unfold/Fold Transformations in Loic Prgramming (with J, Shepherdson), in the festschrift "Computational Proof: Essays in Honour of Alan Robinson", MIT Press, editors J-L. Lassez and G. Plotkin, 1991.