Publications and PhD Theses

2022

File Info
A Trusted Infrastructure for Symbolic Analysis of Event-based Web APIs
- Gabriela Sampaio
Mar 2022

Ph.D. Thesis, Imperial College London
File Info
Exact Separation Logic (submitted)
- Petar Maksimovic
- Caroline Cronjäger
- Julian Sutherland
- Andreas Lööw
- Sacha-Élie Ayoun
- Philippa Gardner
2022

2021

File Info
TaDA Live: Compositional Reasoning for Termination of Fine-grained Concurrent Programs
- Emanuele D’Osualdo
- Azadeh Farzan
- Philippa Gardner
- Julian Sutherland
2021

ACM Transactions on Programming Languages and Systems (TOPLAS), submitted Jan 2020; accepted 2021., vol. 43(4)
File Info
Gillian, Part II: Real-World Verification for JavaScript and C
- Petar Maksimovic
- Sacha-Élie Ayoun
- José Fragoso Santos
- Philippa Gardner
2021

Proceedings of the 33^rd Computer Aided Verification International Conference, CAV 2021, Virtual Event, July 20-23, 2021, Part II, pp. 827–850
File Info
Two Mechanisations of WebAssembly 1.0
- Conrad Watt
- Xiaojia Rao
- Jean Pichon-Pharabod
- Martin Bodin
- Philippa Gardner
2021

Proceedings of the 24^th international symposium of Formal Methods (FM21), Beijing, China; November 20-25, 2021, pp. 61–79

2020

File Info
Gillian, Part I: A Multi-language Platform for Symbolic Execution
- José Fragoso Santos
- Petar Maksimovic
- Sacha-Élie Ayoun
- Philippa Gardner
2020

Proceedings of the 41^st ACM SIGPLAN International Conference on Programming Language Design and Implementation (PLDI ’20), June 15–20, 2020, London, UK
File Info
Parametric Operational Semantics for Consistency Models
- Shale Xiong
2020

Ph.D. Thesis, Imperial College London
File Info
Data Consistency in Transactional Storage Systems: a Centralised Approach
- Shale Xiong
- Andrea Cerone
- Azalea Raad
- Philippa Gardner
2020

Proceedings of the 34^th European Conference on Object-Oriented Programming (ECOOP 2020)
File Info
A Trusted Infrastructure for Symbolic Analysis of Event-Driven Web Applications
- Gabriela Sampaio
- José Fragoso Santos
- Petar Maksimovic
- Philippa Gardner
2020

Proceedings of the 34^th European Conference on Object-Oriented Programming (ECOOP 2020)

2019

File Info
JaVerT 2.0: Compositional Symbolic Execution for JavaScript
- José Fragoso Santos
- Petar Maksimovic
- Gabriela Sampaio
- Philippa Gardner
2019

Proceedings of the 46^th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL’19), vol. 3( POPL)
File Info
Skeletal Semantics and their Interpretations
- Martin Bodin
- Philippa Gardner
- Thomas Jensen
- Alan Schmitt
2019

Proceedings of the 46^th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL’19)
File Info
A Program Logic for First-Order Encapsulated WebAssembly
- Conrad Watt
- Petar Maksimovic
- Neelakantan R. Krishnaswami
- Philippa Gardner
2019

Proceedings of the 33^rd European Conference on Object-Oriented Programming (ECOOP 2019), pp. 9:1–9:30

2018

File Info
Symbolic Execution for JavaScript
- José Fragoso Santos
- Petar Maksimovic
- Théotime Grohens
- Julian Dolby
- Philippa Gardner
Sep 2018

Proceedings of the 20th International Symposium on Principles and Practice of Declarative Programming, PPDP 2018, Frankfurt am Main, Germany, September 03-05, 2018, pp. 11:1–11:14
File Info
JaVerT: JavaScript Verification and Testing Framework: Invited Talk
- Philippa Gardner
Sep 2018

Proceedings of the 20^thh International Symposium on Principles and Practice of Declarative Programming, PPDP 2018, Frankfurt am Main, Germany, September 03-05, 2018, pp. 1:1–1:4
File Info
A Perspective on Specifying and Verifying Concurrent Modules
- Thomas Dinsdale-Young
- Pedro da Rocha Pinto
- Philippa Gardner
Aug 2018

Journal of Logical and Algebraic Methods in Programming, vol. 98, pp. 1–25
File Info
A Concurrent Specification of POSIX File Systems
- Gian Ntzik
- Pedro da Rocha Pinto
- Julian Sutherland
- Philippa Gardner
Jul 2018

Proceedings of the 32^nd European Conference on Object-Oriented Programming (ECOOP 2018).
File Info
JaVerT: JavaScript Verification Toolchain
- José Fragoso Santos
- Petar Maksimovic
- Daiva Naudziuniene
- Thomas Wood
- Philippa Gardner
2018

Proceedings of the 45^th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL’18), pp. 50:1–50:33
File Info
An Infrastructure for Tractable Verification of JavaScript Programs
- Daiva Naudziuniene
2018

Ph.D. Thesis, Imperial College London

2017

File Info
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)
File Info
Towards Logic-based Verification of JavaScript Programs
- José Fragoso Santos
- Philippa Gardner
- Petar Maksimovic
- Daiva Naudziuniene
Aug 2017

Proceedings of 26^th Conference on Automated Deduction (CADE 26)
File Info
Abstraction, Refinement and Concurrent Reasoning
- Azalea Raad
Jun 2017

Ph.D. Thesis, Imperial College London
File Info
Reasoning with Time and Data Abstractions
- Pedro da Rocha Pinto
May 2017

Ph.D. Thesis, Imperial College London
File Info
Abstract Specifications for Concurrent Maps
- Shale Xiong
- Pedro da Rocha Pinto
- Gian Ntzik
- Philippa Gardner
Apr 2017

Proceedings of the 26^th European Symposium on Programming (ESOP’17), pp. 964–990
File Info
Reasoning About POSIX File Systems
- Gian Ntzik
2017

Ph.D. Thesis, Imperial College London

2016

File Info
Modular Termination Verification for Non-blocking Concurrency
- Pedro da Rocha Pinto
- Thomas Dinsdale-Young
- Philippa Gardner
- Julian Sutherland
Apr 2016

Proceedings of the 25^th European Symposium on Programming (ESOP’16), pp. 176–201
File Info
DOM: Specification and Client Reasoning
- Azalea Raad
- José Fragoso Santos
- Philippa Gardner
2016

Proceedings of the 13^th Asian Symposium on Programming Languages and Systems (APLAS’16), pp. 401–422
File Info
Verifying Concurrent Graph Algorithms
- Azalea Raad
- Aquinas Hobor
- Jules Villard
- Philippa Gardner
2016

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

2015

File Info
Fault-tolerant Resource Reasoning
- Gian Ntzik
- Pedro da Rocha Pinto
- Philippa Gardner
Dec 2015

Proceedings of the 13^th Asian Symposium on Programming Languages and Systems (APLAS’15), pp. 169–188
File Info
Reasoning about the POSIX File System: Local Update and Global Pathnames
- Gian Ntzik
- Philippa Gardner
Oct 2015

Proceedings of the 30^th Annual ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA’15), pp. 201–220
File Info
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
File Info
CoLoSL: Concurrent Local Subjective Logic
- Azalea Raad
- Jules Villard
- Philippa Gardner
2015

Proceedings of the 24^th European Symposium on Programming (ESOP’15), pp. 710–735
File Info
A Trusted Mechanised Specification of JavaScript: One Year On
- Philippa Gardner
- Gareth Smith
- Conrad Watt
- Thomas Wood
2015

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

2014

File Info
TaDA: A Logic for Time and Data Abstraction
- Pedro da Rocha Pinto
- Thomas Dinsdale-Young
- Philippa Gardner
Jul 2014

Proceedings of the 28^th European Conference on Object-Oriented Programming (ECOOP’14), pp. 207–231
File Info
A Trusted Mechanised JavaScript Specification
- Martin Bodin
- Arthur Charguéraud
- Daniele Filaretti
- Philippa Gardner
- Sergio Maffeis
- Daiva Naudziuniene
- Alan Schmitt
- Gareth Smith
2014

Proceedings of the 41^st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL’14), pp. 87–100
File Info
Local Reasoning for the POSIX File System
- Philippa Gardner
- Gian Ntzik
- Adam Wright
2014

Proceedings of the 23^rd European Symposium on Programming (ESOP’14), pp. 169–188
File Info
Abstract Local Reasoning for Concurrent Libraries: Mind the Gap
- Philippa Gardner
- Azalea Raad
- Mark J. Wheelhouse
- Adam Wright
2014

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

2013

File Info
Structural Separation Logic
- Adam Douglas Wright
Aug 2013

Ph.D. Thesis, Imperial College London
File Info
JuS: Squeezing the Sense out of JavaScript Programs
- Philipa Gardner
- Daiva Naudziuniene
- Gareth Smith
Jul 2013

2nd Annual Workshop on Tools for JavaScript Analysis (JSTools ’13)
File Info
Views: Compositional Reasoning for Concurrent Programs
- Thomas Dinsdale-Young
- Lars Birkedal
- Philippa Gardner
- Matthew J. Parkinson
- Hongseok Yang
Jan 2013

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

2012

File Info
Segment Logic
- Mark James Wheelhouse
Oct 2012

Ph.D. Thesis, Imperial College London
File Info
Towards a Program Logic for JavaScript
- Philippa Gardner
- Sergio Maffeis
- Gareth Smith
Jan 2012

Proceedings of the 39^th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL’12), pp. 31–44
Info
Processes in Space
- Luca Cardelli
- Philippa Gardner
2012

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

2011

File Info
Abstract Data and Local Reasoning
- Thomas Dinsdale-Young
Nov 2011

Ph.D. Thesis, Imperial College London
File Info
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 26^th Annual ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA’11), pp. 845–864
File Info
Local Reasoning about Web Programs
- Gareth D. Smith
Jun 2011

Ph.D. Thesis, Imperial College London
Info
- Thomas Dinsdale-Young
- Philippa Gardner
- Mark Wheelhouse
May 2011
File Info
Abstract Local Reasoning for Program Modules
- Thomas Dinsdale-Young
- Philippa Gardner
- Mark J. Wheelhouse
2011

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

2010

File Info
Resource Reasoning and Labelled Separation Logic
- Mohammad Raza
Oct 2010

Imperial College London
File Info
Resource Reasoning about Mashups
- Philippa A Gardner
- Gareth D Smith
- Adam D Wright
Aug 2010

VSTTE Theory Workshop 2010
Info
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
Info
Processes in Space
- Luca Cardelli
- Philippa Gardner
2010

Programs, Proofs, Processes, 6^th Conference on Computability in Europe, CiE 2010, Ponta Delgada, Azores, Portugal, June 30 - July 4, 2010. Proceedings, pp. 78–87
File Info
Adjunct elimination in Context Logic for Trees
- Cristiano Calcagno
- Thomas Dinsdale-Young
- Philippa Gardner
2010

Information and Computation, vol. 208(5), pp. 474–499
File Info
Concurrent Abstract Predicates
- Thomas Dinsdale-Young
- Mike Dodds
- Philippa Gardner
- Matthew J. Parkinson
- Viktor Vafeiadis
2010

Proceedings of the 24^th European Conference on Object-Oriented Programming (ECOOP’10), pp. 504–528
File Info
Abstraction and Refinement for Local Reasoning
- Thomas Dinsdale-Young
- Philippa Gardner
- Mark J. Wheelhouse
2010

Proceedings of the 3^rd International Conference on Verified Software: Theories, Tools, Experiments (VSTTE’10), pp. 199–215
File Info
Reasoning About Client-side Web Programs: Invited Talk
- Philippa Gardner
2010

Proceedings of the 2010 EDBT/ICDT Workshops

2009

Info
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
File Info
Small Specifications for Tree Update
- Philippa Gardner
- Mark J. Wheelhouse
2009

Proceedings of the 6^th International Workshop on Web Services and Formal Methods (WS-FM’09), pp. 178–195
File Info
Automatic Parallelization with Separation Logic
- Mohammad Raza
- Cristiano Calcagno
- Philippa Gardner
2009

Proceedings of the 18^th European Symposium on Programming (ESOP’09), pp. 348–362
Info
Footprints in Local Reasoning
- Mohammad Raza
- Philippa Gardner
2009

Logical Methods in Computer Science, vol. 5(2)
File Info
Decidability of Context Logic
- Christiano Calcagno
- Thomas Dinsdale-Young
- Philippa Gardner
2009
File Info
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

File Info
Behavioural Equivalences for Dynamic Web Data
- Sergio Maffeis
- Philippa Gardner
Feb 2008

Logic and Algebraic Programming, vol. 75(1), pp. 86–138
Info
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
File Info
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)
File Info
Local Hoare Reasoning about DOM
- Philippa Gardner
- Gareth Smith
- Mark J. Wheelhouse
- Uri Zarfaty
2008

Proceedings of the 27^th ACM SIGMOD-SIGACT-SIGART Symposium on Principles of Database Systems (PODS’08), pp. 261–270
Info
Footprints in Local Reasoning
- Mohammad Raza
- Philippa Gardner
2008

Proceedings of the 11^th International Conference on Foundations of Software Science and Computational Structures (FOSSACS’08), pp. 201–215
File Info
Reasoning about High-Level Tree Update and its Low-Level Implementation
- Philippa Gardner
- Uri Zarfaty
2008

2007

File Info
Adjunct Elimination in Context Logic for Trees
- Cristiano Calcagno
- Thomas Dinsdale-Young
- Philippa Gardner
Nov 2007

Proceedings of the 5^th Asian Symposium on Programming Languages and Systems (APLAS’07), pp. 255–270
File Info
Local Reasoning about Data Update
- Cristiano Calcagno
- Philippa Gardner
- Uri Zarfaty
Apr 2007

Electronic Notes on Theoretical Computer Science, vol. 172, pp. 133–175
File Info
Manipulating Trees with Hidden Labels
- Luca Cardelli
- Philippa Gardner
- Giorgio Ghelli
Apr 2007

Electronic Notes in Theoretical Computer Science, vol. 172, pp. 177–201
File Info
Linear Forwarders
- Philippa Gardner
- Cosimo Laneve
- Lucian Wischik
Feb 2007

Inf. Comput., vol. 205(10), pp. 1526–1550
File Info
Expressiveness and Complexity of Graph Logic
- Anuj Dawar
- Philippa Gardner
- Giorgio Ghelli
Feb 2007

Information and Computation, vol. 205(3), pp. 263–310
File Info
Context Logic as Modal Logic: Completeness and Parametric Inexpressivity
- Cristiano Calcagno
- Philippa Gardner
- Uri Zarfaty
Jan 2007

Proceedings of the 34^th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL’07), pp. 123–134
Info
An Introduction to Context Logic
- Philippa Gardner
- Uri Zarfaty
2007

Proceedings of the 14^th International Workshop on Logic, Language, Information and Computation (WoLLIC’07), pp. 189–202
File Info
Context logic and Tree Update
- Uri D Zarfaty
2007

Imperial College London

2006

File Info
Local Reasoning About Tree Update
- Uri Zarfaty
- Philippa Gardner
May 2006

Electr. Notes Theor. Comput. Sci., vol. 158, pp. 399–424
Info
Editorial
- Philippa Gardner
- Nobuko Yoshida
2006

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

2005

File Info
Modelling Dynamic Web Data
- Philippa Gardner
- Sergio Maffeis
Sep 2005

Theoretical Computer Science, vol. 342(1), pp. 104–131
File Info
A Note on Context Logic
- Philippa Gardner
Sep 2005
File Info
Explicit Fusions
- Lucian Wischik
- Philippa Gardner
Aug 2005

Theor. Comput. Sci., vol. 340(3), pp. 606–630
File Info
From Separation Logic to First-Order Logic
- Cristiano Calcagno
- Philippa Gardner
- Matthew Hague
Apr 2005

Proceedings of the 8^th International Conference on Foundations of Software Science and Computational Structures (FOSSACS’05), pp. 395–409
File Info
Context Logic and Tree Update
- Cristiano Calcagno
- Philippa Gardner
- Uri Zarfaty
Jan 2005

Proceedings of the 32^nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL’05), pp. 271–282
File Info
Graph Transformations and Process Algebras for Modeling Distributed and Mobile Systems
- Barbara König
- Ugo Montanari
- Philippa Gardner
2005

04241 Abstracts Collection – Graph Transformations and Process Algebras for Modeling Distributed and Mobile Systems

2004

File Info
Adjunct Elimination Through Games in Static Ambient Logic
- Anuj Dawar
- Philippa Gardner
- Giorgio Ghelli
Dec 2004

Proceedings of the 24^th International Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS’04), pp. 211–223
File Info
Behavioural Equivalences for Dynamic Web Data
- Sergio Maffeis
- Philippa Gardner
Aug 2004

Proceedings of 3^rd International Conference on Theoretical Computer Science (TCS’04), pp. 535–548
File Info
Strong Bisimulation for the Explicit Fusion Calculus
- Lucian Wischik
- Philippa Gardner
Mar 2004

Foundations of Software Science and Computation Structures, 7^th 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

2003

Info
Linear Forwarders
- Philippa Gardner
- Cosimo Laneve
- Lucian Wischik
Sep 2003

CONCUR 2003 - Concurrency Theory, 14^th International Conference, Marseille, France, September 3-5, 2003, Proceedings, pp. 408–422
File Info
Modelling Dynamic Web Data
- Philippa Gardner
- Sergio Maffeis
Sep 2003

Proceedings of 9^th International Workshop on Database Programming Languages (DBPL’03), pp. 130–146
File Info
Ubiquitous Data
- Gavin Bierman
- Peter Buneman
- Philipa Gardner
Sep 2003
File Info
Manipulating Trees with Hidden Labels
- Luca Cardelli
- Philippa Gardner
- Giorgio Ghelli
Apr 2003

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

2002

File Info
The Fusion Machine
- Philippa Gardner
- Cosimo Laneve
- Lucian Wischik
Aug 2002

CONCUR 2002 - Concurrency Theory, 13^th International Conference, Brno, Czech Republic, August 20-23, 2002, Proceedings, pp. 418–433
File Info
A Spatial Logic for Querying Graphs
- Luca Cardelli
- Philippa Gardner
- Giorgio Ghelli
Jul 2002

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

2000

File Info
Explicit Fusions
- Philippa Gardner
- Lucian Wischik
Aug 2000

Mathematical Foundations of Computer Science 2000, 25^th International Symposium, MFCS 2000, Bratislava, Slovakia, August 28 - September 1, 2000, Proceedings, pp. 373–382
File Info
From Process Calculi to Process Frameworks
- Philippa Gardner
2000

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

1999

File Info
Symmetric Action Calculi
- Philippa Gardner
- Lucian J. Wischik
Feb 1999
File Info
Closed Action Calculi
- Philippa Gardner
1999

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

1997

File Info
A Type-theoretic Description of Action Calculi
- Philippa Gardner
1997

Electr. Notes Theor. Comput. Sci., vol. 10, pp. 52
File Info
From Action Calculi to Linear Logic
- Andrew G. Barber
- Philippa Gardner
- Masahito Hasegawa
- Gordon D. Plotkin
1997

Computer Science Logic, 11^th International Workshop, CSL ’97, Annual Conference of the EACSL, Aarhus, Denmark, August 23-29, 1997, Selected Papers, pp. 78–97
Info
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

Info
A Name-free Account of Action Calculi
- Philippa Gardner
1995

Electr. Notes Theor. Comput. Sci., vol. 1, pp. 214–231
File Info
Equivalences between Logics and Their Representing Type Theories
- Philippa Gardner
1995

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

1994

File Info
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

Info
A New Type Theory for Representing Logics
- Philippa Gardner
Jul 1993

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

1992

File Info
Representing Logics in Type Theory
- Philippa Gardner
Jan 1992

Ph.D. Thesis, University of Edinburgh, UK

1991

Info
Unfold/Fold Transformations of Logic Programs
- Philippa Gardner
- John C. Shepherdson
1991

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