default search action
Philippa Gardner
Person information
- affiliation: Imperial College London, UK
Refine list
refinements active!
zoomed in on ?? of ?? records
view refined list in
export refined list as
showing all ?? records
2020 – today
- 2024
- [j22]Andreas Lööw, Daniele Nantes-Sobrinho, Sacha-Élie Ayoun, Caroline Cronjäger, Nat Karmios, Petar Maksimovic, Philippa Gardner:
Compositional Symbolic Execution for Correctness and Incorrectness Reasoning (Artifact). Dagstuhl Artifacts Ser. 10(2): 13:1-13:2 (2024) - [j21]Dongjun Youn
, Wonho Shin
Bringing the WebAssembly Standard up to Speed with SpecTec. Proc. ACM Program. Lang. 8(PLDI): 1559-1584 (2024) - [c68]Andreas Lööw, Daniele Nantes-Sobrinho
Compositional Symbolic Execution for Correctness and Incorrectness Reasoning. ECOOP 2024: 25:1-25:28 - [c67]Andreas Lööw, Daniele Nantes-Sobrinho
Matching Plans for Frame Inference in Compositional Reasoning. ECOOP 2024: 26:1-26:20 - [i12]Sacha-Élie Ayoun, Xavier Denis, Petar Maksimovic, Philippa Gardner:
A hybrid approach to semi-automated Rust verification. CoRR abs/2403.15122 (2024) - [i11]Andreas Lööw, Daniele Nantes-Sobrinho, Sacha-Élie Ayoun, Caroline Cronjäger, Petar Maksimovic, Philippa Gardner:
Compositional Symbolic Execution for Correctness and Incorrectness Reasoning (Extended Version). CoRR abs/2407.10838 (2024) - 2023
- [j20]Xiaojia Rao
Iris-Wasm: Robust and Modular Verification of WebAssembly Programs. Proc. ACM Program. Lang. 7(PLDI): 1096-1120 (2023) - [c66]Nat Karmios
Symbolic Debugging with Gillian. DEBT@ISSTA 2023: 1-2 - [c65]Petar Maksimovic, Caroline Cronjäger, Andreas Lööw, Julian Sutherland, Philippa Gardner:
Exact Separation Logic: Towards Bridging the Gap Between Verification and Bug-Finding. ECOOP 2023: 19:1-19:27 - [i10]Joachim Breitner, Philippa Gardner, Jaehyun Lee, Sam Lindley, Matija Pretnar, Xiaojia Rao, Andreas Rossberg, Sukyoung Ryu, Wonho Shin, Conrad Watt, Dongjun Youn:
Wasm SpecTec: Engineering a Formal Language Standard. CoRR abs/2311.07223 (2023) - 2022
- [c64]Philippa Gardner:
Concurrent Separation Logics: Logical Abstraction, Logical Atomicity and Environment Liveness Conditions (Invited Talk). CONCUR 2022: 2:1-2:1 - [i9]Petar Maksimovic, Caroline Cronjäger, Julian Sutherland, Andreas Lööw, Sacha-Élie Ayoun, Philippa Gardner:
Exact Separation Logic. CoRR abs/2208.07200 (2022) - 2021
- [j19]Emanuele D'Osualdo
TaDA Live: Compositional Reasoning for Termination of Fine-grained Concurrent Programs. ACM Trans. Program. Lang. Syst. 43(4): 16:1-16:134 (2021) - [c63]Petar Maksimovic, Sacha-Élie Ayoun, José Fragoso Santos, Philippa Gardner:
Gillian, Part II: Real-World Verification for JavaScript and C. CAV (2) 2021: 827-850 - [c62]Conrad Watt, Xiaojia Rao, Jean Pichon-Pharabod, Martin Bodin
Two Mechanisations of WebAssembly 1.0. FM 2021: 61-79 - [i8]Petar Maksimovic, José Fragoso Santos, Sacha-Élie Ayoun, Philippa Gardner:
Gillian: A Multi-Language Platform for Unified Symbolic Analysis. CoRR abs/2105.14769 (2021) - 2020
- [j18]Gabriela Sampaio, José Fragoso Santos, Petar Maksimovic, Philippa Gardner:
A Trusted Infrastructure for Symbolic Analysis of Event-Driven Web Applications (Artifact). Dagstuhl Artifacts Ser. 6(2): 05:1-05:3 (2020) - [c61]Shale Xiong, Andrea Cerone, Azalea Raad, Philippa Gardner:
Data Consistency in Transactional Storage Systems: A Centralised Semantics. ECOOP 2020: 21:1-21:31 - [c60]Gabriela Sampaio, José Fragoso Santos, Petar Maksimovic, Philippa Gardner:
A Trusted Infrastructure for Symbolic Analysis of Event-Driven Web Applications. ECOOP 2020: 28:1-28:29 - [c59]José Fragoso Santos, Petar Maksimovic, Sacha-Élie Ayoun, Philippa Gardner:
Gillian, part i: a multi-language platform for symbolic execution. PLDI 2020: 927-942 - [i7]José Fragoso Santos, Petar Maksimovic
Gillian: Compositional Symbolic Execution for All. CoRR abs/2001.05059 (2020)
2010 – 2019
- 2019
- [j17]Martin Bodin
Skeletal semantics and their interpretations. Proc. ACM Program. Lang. 3(POPL): 44:1-44:31 (2019) - [j16]José Fragoso Santos
JaVerT 2.0: compositional symbolic execution for JavaScript. Proc. ACM Program. Lang. 3(POPL): 66:1-66:31 (2019) - [c58]Conrad Watt, Petar Maksimovic
A Program Logic for First-Order Encapsulated WebAssembly. ECOOP 2019: 9:1-9:30 - [i6]Emanuele D'Osualdo, Azadeh Farzan, Philippa Gardner, Julian Sutherland:
TaDA Live: Compositional Reasoning for Termination of Fine-grained Concurrent Programs. CoRR abs/1901.05750 (2019) - [i5]Shale Xiong, Andrea Cerone, Azalea Raad, Philippa Gardner:
Data Consistency in Transactional Storage Systems: a Centralised Approach. CoRR abs/1901.10615 (2019) - 2018
- [j15]Thomas Dinsdale-Young, Pedro da Rocha Pinto
A perspective on specifying and verifying concurrent modules. J. Log. Algebraic Methods Program. 98: 1-25 (2018) - [j14]José Fragoso Santos
JaVerT: JavaScript verification toolchain. Proc. ACM Program. Lang. 2(POPL): 50:1-50:33 (2018) - [c57]Gian Ntzik, Pedro da Rocha Pinto
A Concurrent Specification of POSIX File Systems. ECOOP 2018: 4:1-4:28 - [c56]Philippa Gardner:
JaVerT: JavaScript Verification and Testing Framework: Invited Talk. PPDP 2018: 1:1-1:4 - [c55]José Fragoso Santos
Symbolic Execution for JavaScript. PPDP 2018: 11:1-11:14 - [i4]Martin Bodin, Philippa Gardner, Thomas P. Jensen, Alan Schmitt:
Skeletal Semantics and their Interpretations. CoRR abs/1809.09749 (2018) - [i3]Conrad Watt, Petar Maksimovic
A Program Logic for First-Order Encapsulated WebAssembly. CoRR abs/1811.03479 (2018) - 2017
- [c54]José Fragoso Santos
Towards Logic-Based Verification of JavaScript Programs. CADE 2017: 8-25 - [c53]Shale Xiong, Pedro da Rocha Pinto
Abstract Specifications for Concurrent Maps. ESOP 2017: 964-990 - 2016
- [c52]Azalea Raad, Aquinas Hobor, Jules Villard
Verifying Concurrent Graph Algorithms. APLAS 2016: 314-334 - [c51]Azalea Raad, José Fragoso Santos
DOM: Specification and Client Reasoning. APLAS 2016: 401-422 - [c50]Pedro da Rocha Pinto
Modular Termination Verification for Non-blocking Concurrency. ESOP 2016: 176-201 - 2015
- [c49]Gian Ntzik
Fault-Tolerant Resource Reasoning. APLAS 2015: 169-188 - [c48]Philippa Gardner, Gareth Smith, Conrad Watt, Thomas Wood
A Trusted Mechanised Specification of JavaScript: One Year On. CAV (1) 2015: 3-10 - [c47]Azalea Raad, Jules Villard
CoLoSL: Concurrent Local Subjective Logic. ESOP 2015: 710-735 - [c46]Gian Ntzik
Reasoning about the POSIX file system: local update and global pathnames. OOPSLA 2015: 201-220 - [c45]Pedro da Rocha Pinto
Steps in Modular Specifications for Concurrent Modules (Invited Tutorial Paper). MFPS 2015: 3-18 - [i2]Lars Birkedal, Derek Dreyer, Philippa Gardner, Zhong Shao
Compositional Verification Methods for Next-Generation Concurrency (Dagstuhl Seminar 15191). Dagstuhl Reports 5(5): 1-23 (2015) - 2014
- [c44]Pedro da Rocha Pinto
TaDA: A Logic for Time and Data Abstraction. ECOOP 2014: 207-231 - [c43]Philippa Gardner, Gian Ntzik
Local Reasoning for the POSIX File System. ESOP 2014: 169-188 - [c42]Martin Bodin
A trusted mechanised JavaScript specification. POPL 2014: 87-100 - [c41]Philippa Gardner, Azalea Raad, Mark J. Wheelhouse, Adam Wright:
Abstract Local Reasoning for Concurrent Libraries: Mind the Gap. MFPS 2014: 147-166 - 2013
- [c40]Thomas Dinsdale-Young, Lars Birkedal, Philippa Gardner, Matthew J. Parkinson, Hongseok Yang:
Views: compositional reasoning for concurrent programs. POPL 2013: 287-300 - [e4]Matthias Felleisen, Philippa Gardner:
Programming Languages and Systems - 22nd European Symposium on Programming, ESOP 2013, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2013, Rome, Italy, March 16-24, 2013. Proceedings. Lecture Notes in Computer Science 7792, Springer 2013, ISBN 978-3-642-37035-9 [contents] - 2012
- [j13]Luca Cardelli
Processes in space. Theor. Comput. Sci. 431: 40-55 (2012) - [c39]Philippa Gardner, Sergio Maffeis
Towards a program logic for JavaScript. POPL 2012: 31-44 - 2011
- [c38]Thomas Dinsdale-Young, Philippa Gardner, Mark J. Wheelhouse
Abstract Local Reasoning for Program Modules. CALCO 2011: 36-39 - [c37]Pedro da Rocha Pinto
A simple abstraction for complex concurrent indexes. OOPSLA 2011: 845-864 - 2010
- [j12]Cristiano Calcagno, Thomas Dinsdale-Young, Philippa Gardner:
Adjunct elimination in Context Logic for trees. Inf. Comput. 208(5): 474-499 (2010) - [j11]Michael Benedikt
Report on the EDBT/ICDT 2010 workshop on updates in XML. SIGMOD Rec. 39(1): 54-57 (2010) - [c36]Luca Cardelli
Processes in Space. CiE 2010: 78-87 - [c35]Thomas Dinsdale-Young, Mike Dodds, Philippa Gardner, Matthew J. Parkinson, Viktor Vafeiadis
Concurrent Abstract Predicates. ECOOP 2010: 504-528 - [c34]Philippa Gardner:
Reasoning about client-side web programs: invited talk. EDBT/ICDT Workshops 2010 - [c33]Thomas Dinsdale-Young, Philippa Gardner, Mark J. Wheelhouse:
Abstraction and Refinement for Local Reasoning. VSTTE 2010: 199-215
2000 – 2009
- 2009
- [j10]Mohammad Raza, Philippa Gardner:
Footprints in Local Reasoning. Log. Methods Comput. Sci. 5(2) (2009) - [j9]Luca Cardelli
A process model of Rho GTP-binding proteins. Theor. Comput. Sci. 410(33-34): 3166-3185 (2009) - [c32]Mohammad Raza, Cristiano Calcagno, Philippa Gardner:
Automatic Parallelization with Separation Logic. ESOP 2009: 348-362 - [c31]Philippa Gardner, Mark J. Wheelhouse:
Small Specifications for Tree Update. WS-FM 2009: 178-195 - [e3]Philippa Gardner, Floris Geerts
Database Programming Languages - DBPL 2009, 12th International Symposium, Lyon, France, August 24, 2009. Proceedings. Lecture Notes in Computer Science 5708, Springer 2009, ISBN 978-3-642-03792-4 [contents] - 2008
- [j8]Sergio Maffeis
Behavioural equivalences for dynamic Web data. J. Log. Algebraic Methods Program. 75(1): 86-138 (2008) - [c30]Mohammad Raza, Philippa Gardner:
Footprints in Local Reasoning. FoSSaCS 2008: 201-215 - [c29]Philippa Gardner, Gareth Smith, Mark J. Wheelhouse, Uri Zarfaty:
DOM: Towards a Formal Specification. PLAN-X 2008 - [c28]Philippa Gardner, Gareth Smith, Mark J. Wheelhouse
Local Hoare reasoning about DOM. PODS 2008: 261-270 - [c27]Luca Cardelli
A Process Model of Actin Polymerisation. FBTC@ICALP 2008: 127-144 - 2007
- [j7]Anuj Dawar
Expressiveness and complexity of graph logic. Inf. Comput. 205(3): 263-310 (2007) - [j6]Philippa Gardner, Cosimo Laneve
Linear forwarders. Inf. Comput. 205(10): 1526-1550 (2007) - [c26]Cristiano Calcagno, Thomas Dinsdale-Young, Philippa Gardner:
Adjunct Elimination in Context Logic for Trees. APLAS 2007: 255-270 - [c25]Cristiano Calcagno, Philippa Gardner, Uri Zarfaty:
Context logic as modal logic: completeness and parametric inexpressivity. POPL 2007: 123-134 - [c24]Philippa Gardner, Uri Zarfaty:
An Introduction to Context Logic. WoLLIC 2007: 189-202 - [c23]Luca Cardelli
A Process Model of Rho GTP-binding Proteins in the Context of Phagocytosis. FBTC@CONCUR 2007: 87-102 - [c22]Cristiano Calcagno, Philippa Gardner, Uri Zarfaty:
Local Reasoning about Data Update. Computation, Meaning, and Logic 2007: 133-175 - [c21]Luca Cardelli
Manipulating Trees with Hidden Labels. Computation, Meaning, and Logic 2007: 177-201 - 2006
- [j5]Philippa Gardner, Nobuko Yoshida
Editorial. Theor. Comput. Sci. 358(2-3): 149 (2006) - [c20]Uri Zarfaty, Philippa Gardner:
Local Reasoning About Tree Update. MFPS 2006: 399-424 - 2005
- [j4]Lucian Wischik, Philippa Gardner:
Explicit fusions. Theor. Comput. Sci. 340(3): 606-630 (2005) - [j3]Philippa Gardner, Sergio Maffeis
Modelling dynamic web data. Theor. Comput. Sci. 342(1): 104-131 (2005) - [c19]Cristiano Calcagno, Philippa Gardner, Matthew Hague:
From Separation Logic to First-Order Logic. FoSSaCS 2005: 395-409 - [c18]Cristiano Calcagno, Philippa Gardner, Uri Zarfaty:
Context logic and tree update. POPL 2005: 271-282 - [e2]Barbara König, Ugo Montanari, Philippa Gardner:
Graph Transformations and Process Algebras for Modeling Distributed and Mobile Systems, 6.-11. June 2004. Dagstuhl Seminar Proceedings 04241, IBFI, Schloss Dagstuhl, Germany 2005 [contents] - 2004
- [c17]Lucian Wischik, Philippa Gardner:
Strong Bisimulation for the Explicit Fusion Calculus. FoSSaCS 2004: 484-498 - [c16]Anuj Dawar
Adjunct Elimination Through Games in Static Ambient Logic. FSTTCS 2004: 211-223 - [c15]Sergio Maffeis
Behavioural Equivalences for Dynamic Web Data. IFIP TCS 2004: 535-548 - [e1]Philippa Gardner, Nobuko Yoshida
CONCUR 2004 - Concurrency Theory, 15th International Conference, London, UK, August 31 - September 3, 2004, Proceedings. Lecture Notes in Computer Science 3170, Springer 2004, ISBN 3-540-22940-X [contents] - [i1]Barbara König, Ugo Montanari, Philippa Gardner:
04241 Abstracts Collection - Graph Transformations and Process Algebras for Modeling Distributed and Mobile Systems. Graph Transformations and Process Algebras for Modeling Distributed and Mobile Systems 2004 - 2003
- [c14]Philippa Gardner, Cosimo Laneve
Linear Forwarders. CONCUR 2003: 408-422 - [c13]Philippa Gardner, Sergio Maffeis
Modelling Dynamic Web Data. DBPL 2003: 130-146 - [c12]Luca Cardelli, Philippa Gardner, Giorgio Ghelli:
Manipulating Trees with Hidden Labels. FoSSaCS 2003: 216-232 - 2002
- [c11]Philippa Gardner, Cosimo Laneve
The Fusion Machine. CONCUR 2002: 418-433 - [c10]Luca Cardelli, Philippa Gardner, Giorgio Ghelli:
A Spatial Logic for Querying Graphs. ICALP 2002: 597-610 - 2000
- [c9]Philippa Gardner:
From Process Calculi to Process Frameworks. CONCUR 2000: 69-88 - [c8]Philippa Gardner, Lucian Wischik:
Explicit Fusions. MFCS 2000: 373-382
1990 – 1999
- 1999
- [j2]Philippa Gardner:
Closed Action Calculi. Theor. Comput. Sci. 228(1-2): 77-103 (1999) - 1997
- [c7]Andrew G. Barber, Philippa Gardner, Masahito Hasegawa
From Action Calculi to Linear Logic. CSL 1997: 78-97 - [c6]Philippa Gardner, Masahito Hasegawa
Types and Models for Higher-Order Action Calculi. TACS 1997: 583-603 - [c5]Philippa Gardner:
A Type-theoretic Description of Action Calculi. HOOTS 1997: 52 - 1995
- [j1]Philippa Gardner:
Equivalences between Logics and Their Representing Type Theories. Math. Struct. Comput. Sci. 5(3): 323-349 (1995) - [c4]Philippa Gardner:
A name-free account of action calculi. MFPS 1995: 214-231 - 1994
- [c3]Philippa Gardner:
Discovering Needed Reductions Using Type Theory. TACS 1994: 555-574 - 1993
- [c2]Philippa Gardner:
A New Type Theory for Representing Logics. LPAR 1993: 146-157 - 1992
- [b1]Philippa Gardner:
Representing logics in type theory. University of Edinburgh, UK, 1992 - 1991
- [c1]Philippa Gardner, John C. Shepherdson:
Unfold/Fold Transformations of Logic Programs. Computational Logic - Essays in Honor of Alan Robinson 1991: 565-583
Coauthor Index
manage site settings
To protect your privacy, all features that rely on external API calls from your browser are turned off by default. You need to opt-in for them to become active. All settings here will be stored as cookies with your web browser. For more information see our F.A.Q.
Unpaywalled article links
Add open access links from to the list of external document links (if available).
Privacy notice: By enabling the option above, your browser will contact the API of unpaywall.org to load hyperlinks to open access articles. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Unpaywall privacy policy.
Archived links via Wayback Machine
For web page which are no longer available, try to retrieve content from the of the Internet Archive (if available).
Privacy notice: By enabling the option above, your browser will contact the API of archive.org to check for archived content of web pages that are no longer available. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Internet Archive privacy policy.
Reference lists
Add a list of references from ,
, and
to record detail pages.
load references from crossref.org and opencitations.net
Privacy notice: By enabling the option above, your browser will contact the APIs of crossref.org, opencitations.net, and semanticscholar.org to load article reference information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Crossref privacy policy and the OpenCitations privacy policy, as well as the AI2 Privacy Policy covering Semantic Scholar.
Citation data
Add a list of citing articles from and
to record detail pages.
load citations from opencitations.net
Privacy notice: By enabling the option above, your browser will contact the API of opencitations.net and semanticscholar.org to load citation information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the OpenCitations privacy policy as well as the AI2 Privacy Policy covering Semantic Scholar.
OpenAlex data
Load additional information about publications from .
Privacy notice: By enabling the option above, your browser will contact the API of openalex.org to load additional information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the information given by OpenAlex.
last updated on 2024-10-11 18:23 CEST by the dblp team
all metadata released as open data under CC0 1.0 license
see also: Terms of Use | Privacy Policy | Imprint
dblp was originally created in 1993 at:
since 2018, dblp has been operated and maintained by:
the dblp computer science bibliography is funded and supported by: