This readme file is published in its fully rendered form on the website.

The source code for this site is hosted on the DoC GitLab server, you should have access to edit it if a member of the resource-reasoning group.

DO NOT EDIT THE SOURCE CODE IN /vol/rr/www, IT IS ALL REPLACED EACH TIME THE SITE IS REBUILT FROM VERSION CONTROL

## Managing Content

### Publications

Please see the dedicated publications repository for instructions on how to add new publications to the website.

## Technical Detail

This website is built using the Jekyll website framework. Pages can be written using Markdown (preferred) or HTML. Files should be named with the extension they’re writen in (.md, .markdown, .html, …), they’ll be compiled to .html versions of the file on publication. (Unless otherwise specified with the ‘permalink’ property of the page).

Pages to be interpreted by the Jekyll framework should be started with a YAML variable block. The variables here can be used to change properties of the page. For further details, see the Jekyll documentation. For example, to set the page title and it’s URL:

---
title: Page Name
---


Variables that templates currently take into account are:

• title, sets the page title
• menu, (default: false) places the page into the website’s navigation menu
• menu_order, decides the order of menu
• parent_menu, creates a parent menu with a dropdown box including the current page. Pages with the same parent menu are put in the same box. Please also ensures the existence of parent_menu and its value, and menu_order are consistent.
• sub_menu_order, decides the order of menu in corresponding dropdown box.
• project_id, links the page to a project.
• project, (please only use this for person, i.e. file under the directory of _people), links a person to a project.
• firstname, lastname, position, webpage, email, github, describes a person.

Any other files present in the directory structure (except for those prefixed with _, ., or explicitly excluded in _config.yml) will be published unchanged to the website.

# Jekyll Scholar Configuration Detail

We desire the output URL structure to be:

• /publications/
• index.html - a page listing the entire bibliography
• publications.bib - the raw bibtex file, directly from the source
• Key.html - details page generated for each publication
• Key.* - Any files associated with each publication, copied directly from the source

In the scholar section of the configuration file, configuration options we’ve used are:

• source: Directory in which our bibtex files are to be found (publications)
• details_dir: Directory to output Key.html files for each publication (publications), rendered using the layout defined in the details_layout option.
• details_link: We override the default here, as we generate our own HTML to render this link in our bibliography_template.
• repository: Location of files associated with publications (publications) (the same directory is used for both input and output: it is handled as usual by jekyll)

The template used to generate individual publication pages is here. The part of interest is the Source Materials section. We iterate through a predefined list of file types and output a link (using icon and text from the file type list) to the file in the repository if it exists.

Finally, in order to generate the complete biography page, we use a page in the site’s root just outputting a <ol class="bibliography"><li><div class="btn-group pull-xs-right" role="group"> </div>

JSExplain: a Double Debugger for JavaScript

WWW ’18 Companion: The 2018 Web Conference Companion, April 23–27, 2018, Lyon, France

</li>

• JaVerT: JavaScript verification toolchain

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

• Algebraic Laws for Weak Consistency

Proceedings of 28th International Conference on Concurrency Theory, (Concur 2017)

• Verified trustworthy software systems

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

• Towards Logic-based Verification of JavaScript Programs

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

• Deciding Secrecy of Security Protocols for an Unbounded Number of Sessions: The Case of Depth-bounded Processes

Proceedings of 30th IEEE Computer Security Foundations Symposium, (CSF 2017)

• Abstraction, Refinement and Concurrent Reasoning

Ph.D. Thesis, Imperial College London

• Reasoning with Time and Data Abstractions

Ph.D. Thesis, Imperial College London

• Caper: Automatic Verification for Fine-grained Concurrency

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

• Abstract Specifications for Concurrent Maps

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

• Reasoning About POSIX File Systems

Ph.D. Thesis, Imperial College London

• Modular Termination Verification for Non-blocking Concurrency

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

• DOM: Specification and Client Reasoning

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

• Mashic Compiler: Mashup Sandboxing based on Inter-frame Communication

Journal of Computer Security, vol. 1(24), pp. 91–136

• Verifying Concurrent Graph Algorithms

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

• Fault-tolerant Resource Reasoning

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

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

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

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

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

• CoLoSL: Concurrent Local Subjective Logic

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

• A Trusted Mechanised Specification of JavaScript: One Year On

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

• Modular Monitor Extensions for Information Flow Security in JavaScript

Trustworthy Global Computing - 10th International Symposium, TGC 2015, Madrid, Spain, August 31 - September 1, 2015 Revised Selected Papers, pp. 47–62

• Hybrid Typing of Secure Information Flow in a JavaScript-Like Language

Trustworthy Global Computing - 10th International Symposium, TGC 2015, Madrid, Spain, August 31 - September 1, 2015 Revised Selected Papers, pp. 63–78

• TaDA: A Logic for Time and Data Abstraction

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

• A Trusted Mechanised JavaScript Specification

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

• Local Reasoning for the POSIX File System

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

• Abstract Local Reasoning for Concurrent Libraries: Mind the Gap

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

• Structural Separation Logic

Imperial College London

• JuS: Squeezing the Sense out of JavaScript Programs

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

• Views: Compositional Reasoning for Concurrent Programs

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

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

• 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

• Segment Logic

• Mark James Wheelhouse

Imperial College London

• Towards a Program Logic for JavaScript

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

• Processes in space

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

• Abstract Data and Local Reasoning

• Thomas Dinsdale-Young

Imperial College London

• A Simple Abstraction for Complex Concurrent Indexes

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

• Local Reasoning about Web Programs

• Gareth D. Smith

Imperial College London

• Abstract Local Reasoning for Program Modules

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

• Resource Reasoning and Labelled Separation Logic

Imperial College London

VSTTE Theory Workshop 2010

• Report on the EDBT/ICDT 2010 workshop on updates in XML

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

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

• Processes in Space

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

• Adjunct elimination in Context Logic for Trees

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

• Concurrent Abstract Predicates

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

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

• Abstraction and Refinement for Local Reasoning

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

• Reasoning About Client-side Web Programs: Invited Talk

Proceedings of the 2010 EDBT/ICDT Workshops

• A Process Model of Actin Polymerisation

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

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

• Database Programming Languages - DBPL 2009, 12th International Symposium, Lyon, France, August 24, 2009. Proceedings

• Small Specifications for Tree Update

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

• Automatic Parallelization with Separation Logic

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

• Footprints in Local Reasoning

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

• Decidability of Context Logic

• A process model of Rho GTP-binding proteins

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

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

• Behavioural Equivalences for Dynamic Web Data

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

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

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

• DOM: Towards a Formal Specification

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

• Local Hoare Reasoning about DOM

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

• Footprints in Local Reasoning

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

• Reasoning about High-Level Tree Update and its Low-Level Implementation

• Adjunct Elimination in Context Logic for Trees

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

• Local Reasoning about Data Update

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

• Manipulating Trees with Hidden Labels

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

• Linear forwarders

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

• Expressiveness and Complexity of Graph Logic

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

• Context Logic as Modal Logic: Completeness and Parametric Inexpressivity

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

• An Introduction to Context Logic

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

• Context logic and tree update

• Uri D Zarfaty

Imperial College London

• Local Reasoning About Tree Update

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

• Editorial

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

• Modelling Dynamic Web Data

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

• A Note on Context Logic

• Explicit fusions

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

• From Separation Logic to First-Order Logic

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

• Context Logic and Tree Update

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

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

• Adjunct Elimination Through Games in Static Ambient Logic

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

• Behavioural Equivalences for Dynamic Web Data

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

• Strong Bisimulation for the Explicit Fusion Calculus

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

• 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, 6.-11. June 2004

• CONCUR 2004 - Concurrency Theory, 15th International Conference, London, UK, August 31 - September 3, 2004, Proceedings

• Linear Forwarders

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

• Modelling Dynamic Web Data

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

• Ubiquitous Data

• Manipulating Trees with Hidden Labels

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

• The Fusion Machine

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

• A Spatial Logic for Querying Graphs

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

• Explicit Fusions

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

• From Process Calculi to Process Frameworks

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

• Symmetric Action Calculi

• Closed Action Calculi

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

• A Type-theoretic Description of Action Calculi

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

• From Action Calculi to Linear Logic

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

• Types and Models for Higher-Order Action Calculi

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

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

• Equivalences between Logics and Their Representing Type Theories

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

• Discovering Needed Reductions Using Type Theory

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

• A new type theory for representing logics

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

• Representing logics in type theory

Ph.D. Thesis, University of Edinburgh, UK

• Unfold/Fold Transformations of Logic Programs

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

• </ol> as normal (which renders each entry using the layout defined by the scholar bibliography_template option). By using a permalink jekyll option we place the rendered bibliography into the /publications/ output directory as index.html.

## Testing and Deployment

The DoC GitLab instance is configured (using .gitlab-ci.yml) to build, test and deploy the website on tests passing. The tests run are to check that the build works (no critical syntax errors in templates), and that internal page links are consistent.

An additional check that external links are still live is also run, but this test is permitted to fail without blocking the deployment.

The site is deployed to /vol/rr/www automatically on successful build.

## Locally Building and Testing

If you wish to test the site locally, ensure you have ruby installed, and then initially run:

gem install bundler
bundle install
bundle exec rake init


And to start a local webserver that remakes files whenever changed:

bundle exec rake serve


bundle exec rake test