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},
Booktitle={Proceedings of the 41\textsuperscript{st} Annual {ACM} {SIGPLAN-SIGACT} Symposium on Principles of Programming Languages ({POPL})},
Booktitle={Proceedings of the 41\textsuperscript{st} Annual {ACM} {SIGPLAN-SIGACT} Symposium on Principles of Programming Languages ({POPL'14})},
Year={2014},
Pages={87--100},
...
...
@@ -31,7 +31,7 @@ We present JSCert, a formalisation of the current ECMA standard in the Coq proof
@InProceedings{Calcagno2007Adjunct,
Title={{Adjunct Elimination in Context Logic for Trees}},
Author={Cristiano Calcagno and Thomas Dinsdale{-}Young and Philippa Gardner},
Booktitle={Proceedings of the 5\textsuperscript{th} Asian Symposium on Programming Languages and Systems ({APLAS})},
Booktitle={Proceedings of the 5\textsuperscript{th} Asian Symposium on Programming Languages and Systems ({APLAS'07})},
Year={2007},
Pages={255--270},
...
...
@@ -43,7 +43,7 @@ We present JSCert, a formalisation of the current ECMA standard in the Coq proof
@InProceedings{Calcagno2005From,
Title={{From Separation Logic to First-Order Logic}},
Author={Cristiano Calcagno and Philippa Gardner and Matthew Hague},
Booktitle={Proceedings of the 8\textsuperscript{th} International Conference on Foundations of Software Science and Computational Structures ({FOSSACS})},
Booktitle={Proceedings of the 8\textsuperscript{th} International Conference on Foundations of Software Science and Computational Structures ({FOSSACS'05})},
Year={2005},
Pages={395--409},
...
...
@@ -55,7 +55,7 @@ We present JSCert, a formalisation of the current ECMA standard in the Coq proof
@InProceedings{Calcagno2007Context,
Title={{Context Logic as Modal Logic: Completeness and Parametric Inexpressivity}},
Author={Cristiano Calcagno and Philippa Gardner and Uri Zarfaty},
Booktitle={Proceedings of the 34\textsuperscript{th} {ACM} {SIGPLAN-SIGACT} Symposium on Principles of Programming Languages ({POPL})},
Booktitle={Proceedings of the 34\textsuperscript{th} {ACM} {SIGPLAN-SIGACT} Symposium on Principles of Programming Languages ({POPL'07})},
Year={2007},
Pages={123--134},
...
...
@@ -80,7 +80,7 @@ We present JSCert, a formalisation of the current ECMA standard in the Coq proof
@InProceedings{Calcagno2005Context,
Title={{Context Logic and Tree Update}},
Author={Cristiano Calcagno and Philippa Gardner and Uri Zarfaty},
Booktitle={Proceedings of the 32\textsuperscript{nd} {ACM} {SIGPLAN-SIGACT} Symposium on Principles of Programming Languages ({POPL})},
Booktitle={Proceedings of the 32\textsuperscript{nd} {ACM} {SIGPLAN-SIGACT} Symposium on Principles of Programming Languages ({POPL'05})},
Year={2005},
Pages={271--282},
...
...
@@ -106,7 +106,7 @@ We present JSCert, a formalisation of the current ECMA standard in the Coq proof
@InProceedings{Cardelli2003Manipulating,
Title={{Manipulating Trees with Hidden Labels}},
Author={Luca Cardelli and Philippa Gardner and Giorgio Ghelli},
Booktitle={Proceedings of the 6\textsuperscript{th} International Conference on Foundations of Software Science and Computational Structures ({FOSSACS})},
Booktitle={Proceedings of the 6\textsuperscript{th} International Conference on Foundations of Software Science and Computational Structures ({FOSSACS'03})},
Year={2003},
Pages={216--232},
...
...
@@ -118,7 +118,7 @@ We present JSCert, a formalisation of the current ECMA standard in the Coq proof
@InProceedings{Cardelli2002Spatial,
Title={{A Spatial Logic for Querying Graphs}},
Author={Luca Cardelli and Philippa Gardner and Giorgio Ghelli},
Booktitle={Proceedings of the 29\textsuperscript{th} International Colloquium on Automata, Languages and Programming ({ICALP})},
Booktitle={Proceedings of the 29\textsuperscript{th} International Colloquium on Automata, Languages and Programming ({ICALP'02})},
Year={2002},
Pages={597--610},
...
...
@@ -144,7 +144,7 @@ We present JSCert, a formalisation of the current ECMA standard in the Coq proof
@InProceedings{Dawar2004Adjunct,
Title={{Adjunct Elimination Through Games in Static Ambient Logic}},
Author={Anuj Dawar and Philippa Gardner and Giorgio Ghelli},
Booktitle={Proceedings of the 24\textsuperscript{th} International Conference on Foundations of Software Technology and Theoretical Computer Science ({FSTTCS})},
Booktitle={Proceedings of the 24\textsuperscript{th} International Conference on Foundations of Software Technology and Theoretical Computer Science ({FSTTCS'04})},
Year={2004},
Pages={211--223},
...
...
@@ -156,7 +156,7 @@ We present JSCert, a formalisation of the current ECMA standard in the Coq proof
@InProceedings{Dinsdale-Young2013Views,
Title={{Views: Compositional Reasoning for Concurrent Programs}},
Author={Thomas Dinsdale{-}Young and Lars Birkedal and Philippa Gardner and Matthew J. Parkinson and Hongseok Yang},
Booktitle={Proceedings of the 40\textsuperscript{th} Annual {ACM} {SIGPLAN-SIGACT} Symposium on Principles of Programming Languages ({POPL})},
Booktitle={Proceedings of the 40\textsuperscript{th} Annual {ACM} {SIGPLAN-SIGACT} Symposium on Principles of Programming Languages ({POPL'13})},
Year={2013},
Pages={287--300},
...
...
@@ -169,7 +169,7 @@ In this paper, we present the 'Concurrent Views Framework', a metatheory of conc
@InProceedings{Dinsdale-Young2010Concurrent,
Title={{Concurrent Abstract Predicates}},
Author={Thomas Dinsdale{-}Young and Mike Dodds and Philippa Gardner and Matthew J. Parkinson and Viktor Vafeiadis},
Booktitle={Proceedings of the 24\textsuperscript{th} European Conference on Object-Oriented Programming ({ECOOP})},
Booktitle={Proceedings of the 24\textsuperscript{th} European Conference on Object-Oriented Programming ({ECOOP'10})},
Year={2010},
Pages={504--528},
...
...
@@ -181,7 +181,7 @@ In this paper, we present the 'Concurrent Views Framework', a metatheory of conc
@InProceedings{Dinsdale-Young2011Abstract,
Title={{Abstract Local Reasoning for Program Modules}},
Author={Thomas Dinsdale{-}Young and Philippa Gardner and Mark J. Wheelhouse},
Booktitle={Proceedings of the 4\textsuperscript{th} International Conference on Algebra and Coalgebra in Computer Science ({CALCO})},
Booktitle={Proceedings of the 4\textsuperscript{th} International Conference on Algebra and Coalgebra in Computer Science ({CALCO'11})},
Year={2011},
Pages={36--39},
...
...
@@ -194,7 +194,7 @@ throughout the proof.}
@InProceedings{Dinsdale-Young2010Abstraction,
Title={{Abstraction and Refinement for Local Reasoning}},
Author={Thomas Dinsdale{-}Young and Philippa Gardner and Mark J. Wheelhouse},
Booktitle={Proceedings of the 3\textsuperscript{rd} International Conference on Verified Software: Theories, Tools, Experiments ({VSTTE})},
Booktitle={Proceedings of the 3\textsuperscript{rd} International Conference on Verified Software: Theories, Tools, Experiments ({VSTTE'10})},
Year={2010},
Pages={199--215},
...
...
@@ -206,7 +206,7 @@ throughout the proof.}
@InProceedings{Gardner2010Reasoning,
Title={{Reasoning About Client-side Web Programs: Invited Talk}},
Author={Philippa Gardner},
Booktitle={Proceedings of the {EDBT/ICDT} Workshops},
Booktitle={Proceedings of the 2010 {EDBT/ICDT} Workshops},
Year={2010},
doi={10.1145/1754239.1754261},
...
...
@@ -232,7 +232,7 @@ throughout the proof.}
@InProceedings{Gardner2003Modelling,
Title={{Modelling Dynamic Web Data}},
Author={Philippa Gardner and Sergio Maffeis},
Booktitle={Proceedings of 9\textsuperscript{th} International Workshop on Database Programming Languages ({DBPL})},
Booktitle={Proceedings of 9\textsuperscript{th} International Workshop on Database Programming Languages ({DBPL'03})},
Year={2003},
Pages={130--146},
...
...
@@ -248,7 +248,7 @@ throughout the proof.}
@InProceedings{Gardner2012Towards,
Title={{Towards a Program Logic for JavaScript}},
Author={Philippa Gardner and Sergio Maffeis and Gareth Smith},
Booktitle={Proceedings of the 39\textsuperscript{th} {ACM} {SIGPLAN-SIGACT} Symposium on Principles of Programming Languages ({POPL})},
Booktitle={Proceedings of the 39\textsuperscript{th} {ACM} {SIGPLAN-SIGACT} Symposium on Principles of Programming Languages ({POPL'12})},
Year={2012},
Pages={31--44},
...
...
@@ -261,7 +261,7 @@ We introduce a program logic for reasoning about a broad subset of JavaScript, i
@InProceedings{Gardner2014Local,
Title={{Local Reasoning for the {POSIX} File System}},
Author={Philippa Gardner and Gian Ntzik and Adam Wright},
Booktitle={Proceedings of the 23\textsuperscript{rd} European Symposium on Programming ({ESOP})},
Booktitle={Proceedings of the 23\textsuperscript{rd} European Symposium on Programming ({ESOP'14})},
Year={2014},
Pages={169--188},
...
...
@@ -273,7 +273,7 @@ We introduce a program logic for reasoning about a broad subset of JavaScript, i
@Article{Gardner2014Abstract,
Title={{Abstract Local Reasoning for Concurrent Libraries: Mind the Gap}},
Author={Philippa Gardner and Azalea Raad and Mark J. Wheelhouse and Adam Wright},
Journal={Proceedings of the 30\textsuperscript{th} Conference on the Mathematical Foundations of Programming Semantics ({MFPS})},
Journal={Proceedings of the 30\textsuperscript{th} Conference on the Mathematical Foundations of Programming Semantics ({MFPS'14})},
Year={2014},
Pages={147--166},
Volume={308},
...
...
@@ -286,7 +286,7 @@ We introduce a program logic for reasoning about a broad subset of JavaScript, i
@InProceedings{Gardner2015Trusted,
Title={{A Trusted Mechanised Specification of JavaScript: One Year On}},
Author={Philippa Gardner and Gareth Smith and Conrad Watt and Thomas Wood},
Booktitle={Proceedings of the 27\textsuperscript{th} International Conference on Computer Aided Verification ({CAV})},
Booktitle={Proceedings of the 27\textsuperscript{th} International Conference on Computer Aided Verification ({CAV'15})},
Year={2015},
Pages={3--10},
...
...
@@ -298,7 +298,7 @@ We introduce a program logic for reasoning about a broad subset of JavaScript, i
@InProceedings{Gardner2008DOM,
Title={{DOM: Towards a Formal Specification}},
Author={Philippa Gardner and Gareth Smith and Mark J. Wheelhouse and Uri Zarfaty},
Booktitle={Proceedings of the {ACM} {SIGPLAN} Workshop on Programming Language Technologies for XML ({PLAN-X})},
Booktitle={Proceedings of the {ACM} {SIGPLAN} Workshop on Programming Language Technologies for XML ({PLAN-X'08})},
Year={2008},
Project={ web },
...
...
@@ -309,7 +309,7 @@ We introduce a program logic for reasoning about a broad subset of JavaScript, i
@InProceedings{Gardner2008Local,
Title={{Local Hoare Reasoning about {DOM}}},
Author={Philippa Gardner and Gareth Smith and Mark J. Wheelhouse and Uri Zarfaty},
Booktitle={Proceedings of the 27\textsuperscript{th} {ACM} {SIGMOD-SIGACT-SIGART} Symposium on Principles of Database Systems ({PODS})},
Booktitle={Proceedings of the 27\textsuperscript{th} {ACM} {SIGMOD-SIGACT-SIGART} Symposium on Principles of Database Systems ({PODS'08})},
Year={2008},
Pages={261--270},
...
...
@@ -321,7 +321,7 @@ We introduce a program logic for reasoning about a broad subset of JavaScript, i
@InProceedings{Gardner2009Small,
Title={{Small Specifications for Tree Update}},
Author={Philippa Gardner and Mark J. Wheelhouse},
Booktitle={Proceedings of the 6\textsuperscript{th} International Workshop on Web Services and Formal Methods ({WS-FM})},
Booktitle={Proceedings of the 6\textsuperscript{th} International Workshop on Web Services and Formal Methods ({WS-FM'09})},
Year={2009},
Pages={178--195},
...
...
@@ -333,7 +333,7 @@ We introduce a program logic for reasoning about a broad subset of JavaScript, i
@InProceedings{Gardner2007Introduction,
Title={{An Introduction to Context Logic}},
Author={Philippa Gardner and Uri Zarfaty},
Booktitle={Proceedings of the 14\textsuperscript{th} International Workshop on Logic, Language, Information and Computation (WoLLIC)},
Booktitle={Proceedings of the 14\textsuperscript{th} International Workshop on Logic, Language, Information and Computation (WoLLIC'07)},
Year={2007},
Pages={189--202},
...
...
@@ -359,7 +359,7 @@ We introduce a program logic for reasoning about a broad subset of JavaScript, i
@InProceedings{Maffeis2004Behavioural,
Title={{Behavioural Equivalences for Dynamic Web Data}},
Author={Sergio Maffeis and Philippa Gardner},
Booktitle={Proceedings of 3\textsuperscript{rd} International Conference on Theoretical Computer Science {(TCS)}},
Booktitle={Proceedings of 3\textsuperscript{rd} International Conference on Theoretical Computer Science {(TCS'04)}},
Year={2004},
Pages={535--548},
...
...
@@ -371,9 +371,10 @@ We introduce a program logic for reasoning about a broad subset of JavaScript, i
@InProceedings{Ntzik2015Reasoning,
Title={{Reasoning about the POSIX File System: Local Update and Global Pathnames}},
Author={Gian Ntzik and Philippa Gardner},
Booktitle={Proceedings of the 30\textsuperscript{th} Annual {ACM} {SIGPLAN} Conference on Object-Oriented Programming, Systems, Languages, and Applications ({OOPSLA})},
Booktitle={Proceedings of the 30\textsuperscript{th} Annual {ACM} {SIGPLAN} Conference on Object-Oriented Programming, Systems, Languages, and Applications ({OOPSLA'15})},
Year={2015},
Month={October},
Pages={201--220},
Project={ concurrency },
...
...
@@ -383,7 +384,7 @@ We introduce a program logic for reasoning about a broad subset of JavaScript, i
@InProceedings{Ntzik2015Fault,
Title={{Fault-tolerant Resource Reasoning}},
Author={Gian Ntzik and Pedro {da Rocha Pinto} and Philippa Gardner},
Booktitle={Proceedings of the 13\textsuperscript{th} Asian Symposium on Programming Languages and Systems ({APLAS})},
Booktitle={Proceedings of the 13\textsuperscript{th} Asian Symposium on Programming Languages and Systems ({APLAS'15})},
Year={2015},
Month={December},
Pages={169--188},
...
...
@@ -398,7 +399,7 @@ We introduce a program logic for reasoning about a broad subset of JavaScript, i
@InProceedings{Raad2015CoLoSL,
Title={{CoLoSL: Concurrent Local Subjective Logic}},
Author={Azalea Raad and Jules Villard and Philippa Gardner},
Booktitle={Proceedings of the 24\textsuperscript{th} European Symposium on Programming ({ESOP})},
Booktitle={Proceedings of the 24\textsuperscript{th} European Symposium on Programming ({ESOP'15})},
Year={2015},
Pages={710--735},
...
...
@@ -410,7 +411,7 @@ We introduce a program logic for reasoning about a broad subset of JavaScript, i
@InProceedings{Raza2009Automatic,
Title={{Automatic Parallelization with Separation Logic}},
Author={Mohammad Raza and Cristiano Calcagno and Philippa Gardner},
Booktitle={Proceedings of the 18\textsuperscript{th} European Symposium on Programming ({ESOP})},
Booktitle={Proceedings of the 18\textsuperscript{th} European Symposium on Programming ({ESOP'09})},
Year={2009},
Pages={348--362},
...
...
@@ -437,7 +438,7 @@ We introduce a program logic for reasoning about a broad subset of JavaScript, i
@InProceedings{Raza2008Footprints,
Title={{Footprints in Local Reasoning}},
Author={Mohammad Raza and Philippa Gardner},
Booktitle={Proceedings of the 11\textsuperscript{th} International Conference on Foundations of Software Science and Computational Structures ({FOSSACS})},
Booktitle={Proceedings of the 11\textsuperscript{th} International Conference on Foundations of Software Science and Computational Structures ({FOSSACS'08})},
Year={2008},
Pages={201--215},
...
...
@@ -449,7 +450,7 @@ We introduce a program logic for reasoning about a broad subset of JavaScript, i
@InProceedings{daRochaPinto2011Simple,
Title={{A Simple Abstraction for Complex Concurrent Indexes}},
Author={Pedro {da Rocha Pinto} and Thomas Dinsdale{-}Young and Mike Dodds and Philippa Gardner and Mark J. Wheelhouse},
Booktitle={Proceedings of the 26\textsuperscript{th} Annual {ACM} {SIGPLAN} Conference on Object-Oriented Programming, Systems, Languages, and Applications ({OOPSLA})},
Booktitle={Proceedings of the 26\textsuperscript{th} Annual {ACM} {SIGPLAN} Conference on Object-Oriented Programming, Systems, Languages, and Applications ({OOPSLA'11})},
Year={2011},
Month={October},
Pages={845--864},
...
...
@@ -465,7 +466,7 @@ We present an abstract specification for concurrent indexes. We verify several r
@InProceedings{daRochaPinto2014TaDA,
Title={{TaDA: A Logic for Time and Data Abstraction}},
Author={Pedro {da Rocha Pinto} and Thomas Dinsdale{-}Young and Philippa Gardner},
Booktitle={Proceedings of the 28\textsuperscript{th} European Conference on Object-Oriented Programming ({ECOOP})},
Booktitle={Proceedings of the 28\textsuperscript{th} European Conference on Object-Oriented Programming ({ECOOP'14})},
Year={2014},
Month={July},
Pages={207--231},
...
...
@@ -481,7 +482,7 @@ Building on separation logic with concurrent abstract predicates (CAP), we intro
@InProceedings{daRochaPinto2015Steps,
Title={{Steps in Modular Specifications for Concurrent Modules (Invited Tutorial Paper)}},
Author={Pedro {da Rocha Pinto} and Thomas Dinsdale-Young and Philippa Gardner},
Booktitle={Proceedings of the 31\textsuperscript{st} Conference on the Mathematical Foundations of Programming Semantics ({MFPS})},
Booktitle={Proceedings of the 31\textsuperscript{st} Conference on the Mathematical Foundations of Programming Semantics ({MFPS'15})},
Year={2015},
Month={June},
Pages={3--18},
...
...
@@ -496,7 +497,7 @@ Building on separation logic with concurrent abstract predicates (CAP), we intro
@InProceedings{daRochaPinto2016Modular,
Title={Modular Termination Verification for Non-blocking Concurrency},
Author={Pedro {da Rocha Pinto} and Thomas Dinsdale-Young and Philippa Gardner and Julian Sutherland},
Booktitle={Proceedings of the 25\textsuperscript{th} European Symposium on Programming ({ESOP})},
Booktitle={Proceedings of the 25\textsuperscript{th} European Symposium on Programming ({ESOP'16})},
Year={2016},
Month={April},
Pages={176--201},
...
...
@@ -511,7 +512,7 @@ Building on separation logic with concurrent abstract predicates (CAP), we intro
@inproceedings{Raad2016Verifying,
Title={Verifying Concurrent Graph Algorithms},
Author={Azalea Raad and Aquinas Hobor and Jules Villard and Philippa Gardner},
Booktitle={Proceedings of the 13th Asian Symposium on Programming Languages and Systems (APLAS)},
Booktitle={Proceedings of the 13th Asian Symposium on Programming Languages and Systems (APLAS'16)},
