Publications and PhD Theses

2018

  1. JaVerT: JavaScript verification toolchain

    • José Fragoso Santos
    • Petar Maksimović
    • Daiva Naudžiūnienė
    • Thomas Wood
    • Philippa Gardner

    2018

    PACMPL, vol. 2(POPL), pp. 50:1–50:33

2017

  1. Verified trustworthy software systems

    • Philippa Gardner

    Sep 2017

    Philosophical Transactions of the Royal Society of London A: Mathematical, Physical and Engineering Sciences, vol. 375(2104)

  2. Towards Logic-based Verification of JavaScript Programs

    • José Fragoso Santos
    • Philippa Gardner
    • Petar Maksimović
    • Daiva Naudžiūnienė

    Aug 2017

    Proceedings of 26th Conference on Automated Deduction (CADE 26)

  3. Abstraction, Refinement and Concurrent Reasoning

    • Azalea Raad

    Jun 2017

    Ph.D. Thesis, Imperial College London

  4. Reasoning with Time and Data Abstractions

    • Pedro da Rocha Pinto

    May 2017

    Ph.D. Thesis, Imperial College London

  5. Abstract Specifications for Concurrent Maps

    • Shale Xiong
    • Pedro da Rocha Pinto
    • Gian Ntzik
    • Philippa Gardner

    Apr 2017

    Proceedings of the 26th European Symposium on Programming (ESOP’17), pp. 964–990

  6. Reasoning About POSIX File Systems

    • Gian Ntzik

    2017

    Ph.D. Thesis, Imperial College London

2016

  1. Modular Termination Verification for Non-blocking Concurrency

    • Pedro da Rocha Pinto
    • Thomas Dinsdale-Young
    • Philippa Gardner
    • Julian Sutherland

    Apr 2016

    Proceedings of the 25th European Symposium on Programming (ESOP’16), pp. 176–201

  2. DOM: Specification and Client Reasoning

    • Azalea Raad
    • José Fragoso Santos
    • Philippa Gardner

    2016

    Proceedings of the 13th Asian Symposium on Programming Languages and Systems (APLAS’16), pp. 401–422

  3. Verifying Concurrent Graph Algorithms

    • Azalea Raad
    • Aquinas Hobor
    • Jules Villard
    • Philippa Gardner

    2016

    Proceedings of the 13th Asian Symposium on Programming Languages and Systems (APLAS’16), pp. 314–334

2015

  1. Fault-tolerant Resource Reasoning

    • Gian Ntzik
    • Pedro da Rocha Pinto
    • Philippa Gardner

    Dec 2015

    Proceedings of the 13th Asian Symposium on Programming Languages and Systems (APLAS’15), pp. 169–188

  2. Reasoning about the POSIX File System: Local Update and Global Pathnames

    • Gian Ntzik
    • Philippa Gardner

    Oct 2015

    Proceedings of the 30th Annual ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA’15), pp. 201–220

  3. Steps in Modular Specifications for Concurrent Modules (Invited Tutorial Paper)

    • Pedro da Rocha Pinto
    • Thomas Dinsdale-Young
    • Philippa Gardner

    Jun 2015

    Electr. Notes Theor. Comput. Sci., vol. 319, pp. 3–18

  4. CoLoSL: Concurrent Local Subjective Logic

    • Azalea Raad
    • Jules Villard
    • Philippa Gardner

    2015

    Proceedings of the 24th European Symposium on Programming (ESOP’15), pp. 710–735

  5. A Trusted Mechanised Specification of JavaScript: One Year On

    • Philippa Gardner
    • Gareth Smith
    • Conrad Watt
    • Thomas Wood

    2015

    Proceedings of the 27th International Conference on Computer Aided Verification (CAV’15), pp. 3–10

2014

  1. TaDA: A Logic for Time and Data Abstraction

    • Pedro da Rocha Pinto
    • Thomas Dinsdale-Young
    • Philippa Gardner

    Jul 2014

    Proceedings of the 28th European Conference on Object-Oriented Programming (ECOOP’14), pp. 207–231

  2. A Trusted Mechanised JavaScript Specification

    • Martin Bodin
    • Arthur Charguéraud
    • Daniele Filaretti
    • Philippa Gardner
    • Sergio Maffeis
    • Daiva Naudžiūnienė
    • Alan Schmitt
    • Gareth Smith

    2014

    Proceedings of the 41st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL’14), pp. 87–100

  3. Local Reasoning for the POSIX File System

    • Philippa Gardner
    • Gian Ntzik
    • Adam Wright

    2014

    Proceedings of the 23rd European Symposium on Programming (ESOP’14), pp. 169–188

  4. Abstract Local Reasoning for Concurrent Libraries: Mind the Gap

    • Philippa Gardner
    • Azalea Raad
    • Mark J. Wheelhouse
    • Adam Wright

    2014

    Proceedings of the 30th Conference on the Mathematical Foundations of Programming Semantics (MFPS’14), vol. 308, pp. 147–166

2013

  1. Structural Separation Logic

    • Adam Douglas Wright

    Aug 2013

    Imperial College London

  2. JuS: Squeezing the Sense out of JavaScript Programs

    • Philipa Gardner
    • Daiva Naudžiűnienė
    • Gareth Smith

    Jul 2013

    2nd Annual Workshop on Tools for JavaScript Analysis (JSTools ’13)

  3. Views: Compositional Reasoning for Concurrent Programs

    • Thomas Dinsdale-Young
    • Lars Birkedal
    • Philippa Gardner
    • Matthew J. Parkinson
    • Hongseok Yang

    Jan 2013

    Proceedings of the 40th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL’13), pp. 287–300

2012

  1. Segment Logic

    • Mark James Wheelhouse

    Oct 2012

    Imperial College London

  2. Towards a Program Logic for JavaScript

    • Philippa Gardner
    • Sergio Maffeis
    • Gareth Smith

    Jan 2012

    Proceedings of the 39th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL’12), pp. 31–44

  3. Processes in space

    • Luca Cardelli
    • Philippa Gardner

    2012

    Theor. Comput. Sci., vol. 431, pp. 40–55

2011

  1. Abstract Data and Local Reasoning

    • Thomas Dinsdale-Young

    Nov 2011

    Imperial College London

  2. A Simple Abstraction for Complex Concurrent Indexes

    • Pedro da Rocha Pinto
    • Thomas Dinsdale-Young
    • Mike Dodds
    • Philippa Gardner
    • Mark J. Wheelhouse

    Oct 2011

    Proceedings of the 26th Annual ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA’11), pp. 845–864

  3. Local Reasoning about Web Programs

    • Gareth D. Smith

    Jun 2011

    Imperial College London

  4. Abstract Local Reasoning for Program Modules

    • Thomas Dinsdale-Young
    • Philippa Gardner
    • Mark J. Wheelhouse

    2011

    Proceedings of the 4th International Conference on Algebra and Coalgebra in Computer Science (CALCO’11), pp. 36–39

2010

  1. Resource Reasoning and Labelled Separation Logic

    • Mohammad Raza

    Oct 2010

    Imperial College London

  2. Resource Reasoning about Mashups

    • Philippa A Gardner
    • Gareth D Smith
    • Adam D Wright

    Aug 2010

    VSTTE Theory Workshop 2010

  3. Report on the EDBT/ICDT 2010 workshop on updates in XML

    • Michael Benedikt
    • Daniela Florescu
    • Philippa Gardner
    • Giovanna Guerrini
    • Marco Mesiti
    • Emmanuel Waller

    2010

    SIGMOD Record, vol. 39(1), pp. 54–57

  4. Processes in Space

    • Luca Cardelli
    • Philippa Gardner

    2010

    Programs, Proofs, Processes, 6th Conference on Computability in Europe, CiE 2010, Ponta Delgada, Azores, Portugal, June 30 - July 4, 2010. Proceedings, pp. 78–87

  5. Adjunct elimination in Context Logic for Trees

    • Cristiano Calcagno
    • Thomas Dinsdale-Young
    • Philippa Gardner

    2010

    Information and Computation, vol. 208(5), pp. 474–499

  6. Concurrent Abstract Predicates

    • Thomas Dinsdale-Young
    • Mike Dodds
    • Philippa Gardner
    • Matthew J. Parkinson
    • Viktor Vafeiadis

    2010

    Proceedings of the 24th European Conference on Object-Oriented Programming (ECOOP’10), pp. 504–528

  7. Abstraction and Refinement for Local Reasoning

    • Thomas Dinsdale-Young
    • Philippa Gardner
    • Mark J. Wheelhouse

    2010

    Proceedings of the 3rd International Conference on Verified Software: Theories, Tools, Experiments (VSTTE’10), pp. 199–215

  8. Reasoning About Client-side Web Programs: Invited Talk

    • Philippa Gardner

    2010

    Proceedings of the 2010 EDBT/ICDT Workshops

2009

  1. A Process Model of Actin Polymerisation

    • Luca Cardelli
    • Emmanuelle Caron
    • Philippa Gardner
    • Ozan Kahramanogullari
    • Andrew Phillips

    2009

    Electr. Notes Theor. Comput. Sci., vol. 229(1), pp. 127–144

  2. Small Specifications for Tree Update

    • Philippa Gardner
    • Mark J. Wheelhouse

    2009

    Proceedings of the 6th International Workshop on Web Services and Formal Methods (WS-FM’09), pp. 178–195

  3. Automatic Parallelization with Separation Logic

    • Mohammad Raza
    • Cristiano Calcagno
    • Philippa Gardner

    2009

    Proceedings of the 18th European Symposium on Programming (ESOP’09), pp. 348–362

  4. Footprints in Local Reasoning

    • Mohammad Raza
    • Philippa Gardner

    2009

    Logical Methods in Computer Science, vol. 5(2)

  5. Decidability of Context Logic

    • Christiano Calcagno
    • Thomas Dinsdale-Young
    • Philippa Gardner

    2009

  6. A process model of Rho GTP-binding proteins

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

    2009

    Theoretical Computer Science, vol. 410(33), pp. 3166–3185

2008

  1. Behavioural Equivalences for Dynamic Web Data

    • Sergio Maffeis
    • Philippa Gardner

    Feb 2008

    Logic and Algebraic Programming, vol. 75(1), pp. 86–138

  2. A Process Model of Rho GTP-binding Proteins in the Context of Phagocytosis

    • Luca Cardelli
    • Philippa Gardner
    • Ozan Kahramanogullari

    2008

    Electr. Notes Theor. Comput. Sci., vol. 194(3), pp. 87–102

  3. DOM: Towards a Formal Specification

    • Philippa Gardner
    • Gareth Smith
    • Mark J. Wheelhouse
    • Uri Zarfaty

    2008

    Proceedings of the ACM SIGPLAN Workshop on Programming Language Technologies for XML (PLAN-X’08)

  4. Local Hoare Reasoning about DOM

    • Philippa Gardner
    • Gareth Smith
    • Mark J. Wheelhouse
    • Uri Zarfaty

    2008

    Proceedings of the 27th ACM SIGMOD-SIGACT-SIGART Symposium on Principles of Database Systems (PODS’08), pp. 261–270

  5. Footprints in Local Reasoning

    • Mohammad Raza
    • Philippa Gardner

    2008

    Proceedings of the 11th International Conference on Foundations of Software Science and Computational Structures (FOSSACS’08), pp. 201–215

  6. Reasoning about High-Level Tree Update and its Low-Level Implementation

    • Philippa Gardner
    • Uri Zarfaty

    2008

2007

  1. Adjunct Elimination in Context Logic for Trees

    • Cristiano Calcagno
    • Thomas Dinsdale-Young
    • Philippa Gardner

    Nov 2007

    Proceedings of the 5th Asian Symposium on Programming Languages and Systems (APLAS’07), pp. 255–270

  2. Local Reasoning about Data Update

    • Cristiano Calcagno
    • Philippa Gardner
    • Uri Zarfaty

    Apr 2007

    Electronic Notes on Theoretical Computer Science, vol. 172, pp. 133–175

  3. Manipulating Trees with Hidden Labels

    • Luca Cardelli
    • Philippa Gardner
    • Giorgio Ghelli

    Apr 2007

    Electronic Notes in Theoretical Computer Science, vol. 172, pp. 177–201

  4. Linear forwarders

    • Philippa Gardner
    • Cosimo Laneve
    • Lucian Wischik

    Feb 2007

    Inf. Comput., vol. 205(10), pp. 1526–1550

  5. Expressiveness and Complexity of Graph Logic

    • Anuj Dawar
    • Philippa Gardner
    • Giorgio Ghelli

    Feb 2007

    Information and Computation, vol. 205(3), pp. 263–310

  6. Context Logic as Modal Logic: Completeness and Parametric Inexpressivity

    • Cristiano Calcagno
    • Philippa Gardner
    • Uri Zarfaty

    Jan 2007

    Proceedings of the 34th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL’07), pp. 123–134

  7. An Introduction to Context Logic

    • Philippa Gardner
    • Uri Zarfaty

    2007

    Proceedings of the 14th International Workshop on Logic, Language, Information and Computation (WoLLIC’07), pp. 189–202

  8. Context logic and tree update

    • Uri D Zarfaty

    2007

    Imperial College London

2006

  1. Local Reasoning About Tree Update

    • Uri Zarfaty
    • Philippa Gardner

    May 2006

    Electr. Notes Theor. Comput. Sci., vol. 158, pp. 399–424

  2. Editorial

    • Philippa Gardner
    • Nobuko Yoshida

    2006

    Theor. Comput. Sci., vol. 358(2-3), pp. 149

2005

  1. Modelling Dynamic Web Data

    • Philippa Gardner
    • Sergio Maffeis

    Sep 2005

    Theoretical Computer Science, vol. 342(1), pp. 104–131

  2. A Note on Context Logic

    • Philippa Gardner

    Sep 2005

  3. Explicit fusions

    • Lucian Wischik
    • Philippa Gardner

    Aug 2005

    Theor. Comput. Sci., vol. 340(3), pp. 606–630

  4. From Separation Logic to First-Order Logic

    • Cristiano Calcagno
    • Philippa Gardner
    • Matthew Hague

    Apr 2005

    Proceedings of the 8th International Conference on Foundations of Software Science and Computational Structures (FOSSACS’05), pp. 395–409

  5. Context Logic and Tree Update

    • Cristiano Calcagno
    • Philippa Gardner
    • Uri Zarfaty

    Jan 2005

    Proceedings of the 32nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL’05), pp. 271–282

2004

  1. Adjunct Elimination Through Games in Static Ambient Logic

    • Anuj Dawar
    • Philippa Gardner
    • Giorgio Ghelli

    Dec 2004

    Proceedings of the 24th International Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS’04), pp. 211–223

  2. Behavioural Equivalences for Dynamic Web Data

    • Sergio Maffeis
    • Philippa Gardner

    Aug 2004

    Proceedings of 3rd International Conference on Theoretical Computer Science (TCS’04), pp. 535–548

  3. Strong Bisimulation for the Explicit Fusion Calculus

    • Lucian Wischik
    • Philippa Gardner

    Mar 2004

    Foundations of Software Science and Computation Structures, 7th International Conference, FOSSACS 2004, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2004, Barcelona, Spain, March 29 - April 2, 2004, Proceedings, pp. 484–498

  4. 04241 Abstracts Collection - Graph Transformations and Process Algebras for Modeling Distributed and Mobile Systems

    • Barbara König
    • Ugo Montanari
    • Philippa Gardner

    2004

    Graph Transformations and Process Algebras for Modeling Distributed and Mobile Systems, 6.-11. June 2004

2003

  1. Linear Forwarders

    • Philippa Gardner
    • Cosimo Laneve
    • Lucian Wischik

    Sep 2003

    CONCUR 2003 - Concurrency Theory, 14th International Conference, Marseille, France, September 3-5, 2003, Proceedings, pp. 408–422

  2. Modelling Dynamic Web Data

    • Philippa Gardner
    • Sergio Maffeis

    Sep 2003

    Proceedings of 9th International Workshop on Database Programming Languages (DBPL’03), pp. 130–146

  3. Ubiquitous Data

    • Gavin Bierman
    • Peter Buneman
    • Philipa Gardner

    Sep 2003

  4. Manipulating Trees with Hidden Labels

    • Luca Cardelli
    • Philippa Gardner
    • Giorgio Ghelli

    Apr 2003

    Proceedings of the 6th International Conference on Foundations of Software Science and Computational Structures (FOSSACS’03), pp. 216–232

2002

  1. The Fusion Machine

    • Philippa Gardner
    • Cosimo Laneve
    • Lucian Wischik

    Aug 2002

    CONCUR 2002 - Concurrency Theory, 13th International Conference, Brno, Czech Republic, August 20-23, 2002, Proceedings, pp. 418–433

  2. A Spatial Logic for Querying Graphs

    • Luca Cardelli
    • Philippa Gardner
    • Giorgio Ghelli

    Jul 2002

    Proceedings of the 29th International Colloquium on Automata, Languages and Programming (ICALP’02), pp. 597–610

2000

  1. Explicit Fusions

    • Philippa Gardner
    • Lucian Wischik

    Aug 2000

    Mathematical Foundations of Computer Science 2000, 25th International Symposium, MFCS 2000, Bratislava, Slovakia, August 28 - September 1, 2000, Proceedings, pp. 373–382

  2. From Process Calculi to Process Frameworks

    • Philippa Gardner

    2000

    CONCUR 2000 - Concurrency Theory, 11th International Conference, University Park, PA, USA, August 22-25, 2000, Proceedings, pp. 69–88

1999

  1. Symmetric Action Calculi

    • Philippa Gardner
    • Lucian J. Wischik

    Feb 1999

  2. Closed Action Calculi

    • Philippa Gardner

    1999

    Theor. Comput. Sci., vol. 228(1-2), pp. 77–103

1997

  1. A Type-theoretic Description of Action Calculi

    • Philippa Gardner

    1997

    Electr. Notes Theor. Comput. Sci., vol. 10, pp. 52

  2. From Action Calculi to Linear Logic

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

    1997

    Computer Science Logic, 11th International Workshop, CSL ’97, Annual Conference of the EACSL, Aarhus, Denmark, August 23-29, 1997, Selected Papers, pp. 78–97

  3. Types and Models for Higher-Order Action Calculi

    • Philippa Gardner
    • Masahito Hasegawa

    1997

    Theoretical Aspects of Computer Software, Third International Symposium, TACS ’97, Sendai, Japan, September 23-26, 1997, Proceedings, pp. 583–603

1995

  1. A Name-free Account of Action Calculi

    • Philippa Gardner

    1995

    Electr. Notes Theor. Comput. Sci., vol. 1, pp. 214–231

  2. Equivalences between Logics and Their Representing Type Theories

    • Philippa Gardner

    1995

    Mathematical Structures in Computer Science, vol. 5(3), pp. 323–349

1994

  1. Discovering Needed Reductions Using Type Theory

    • Philippa Gardner

    1994

    Theoretical Aspects of Computer Software, International Conference TACS ’94, Sendai, Japan, April 19-22, 1994, Proceedings, pp. 555–574

1993

  1. A new type theory for representing logics

    • Philippa Gardner

    Jul 1993

    Logic Programming and Automated Reasoning, 4th International Conference, LPAR’93, St. Petersburg, Russia, July 13–20, 1993 Proceedings, pp. 146–157

1992

  1. Representing logics in type theory

    • Philippa Gardner

    Jan 1992

    Ph.D. Thesis, University of Edinburgh, UK

1991

  1. Unfold/Fold Transformations of Logic Programs

    • Philippa Gardner
    • John C. Shepherdson

    1991

    Computational Logic - Essays in Honor of Alan Robinson, pp. 565–583