.deploy.sh

+#!/bin/sh
+# Use rsync to transfer files to a server via ssh, ensuring that the files are transferred with the correct permissions,
+# user group. The command will also remove old files from the remote directory.
+# To transfer files to the default location, you will need to be a member of the `rr` DoC usergroup.
+#
+# Example usage:
+# DOC_DEPLOY_USER=me ./.deploy.sh
+
+set -x
+USER=${DOC_DEPLOY_USER:+${DOC_DEPLOY_USER}@}
+SERVER=${DOC_DEPLOY_SERVER:-shell1.doc.ic.ac.uk}
+PTH=${DOC_DEPLOY_PATH:-/vol/rr/www}
+exec rsync -e "ssh -o StrictHostKeyChecking=no" --chmod=Dg+s,ug+rwX,o+rX --chown=:rr -igrp --delete _site/ "${USER}${SERVER}:${PTH}"
+

.gitignore

 _site
 .sass-cache
 .jekyll-metadata
+vendor
+.bundle/config
+.DS_Store

.gitlab-ci.yml

-before_script:
-  - bundle install
+stages:
+  - update
+  - build
+  - deploy
 
-test:
-  stage: test
+image: "ruby:2.6-buster"
+variables:
+  NOKOGIRI_USE_SYSTEM_LIBRARIES: "true"
+
+build:
+  stage: build
+  artifacts:
+    paths:
+      - _site/
+    expire_in: 1 day
+  cache:
+    paths:
+      - vendor/bundle/
+  except:
+    - triggers
+  tags:
+    - docker
+    - vtss_site
+  before_script:
+    - bundle install --deployment --without=development --with=test
+    - bundle exec rake init
   script:
-    - bundle exec rake test
+    - bundle exec rake -s --suppress-backtrace . test
 
 deadlinks:
-  stage: test
-  script:
-    - bundle exec rake testlinks
+  stage: deploy
   allow_failure: true
+  cache:
+    paths:
+      - vendor/bundle/
+  except:
+    - triggers
+  tags:
+    - docker
+    - vtss_site
+  before_script:
+    - bundle install --deployment --without=development --with=test
+  script:
+    - bundle exec rake -s --suppress-backtrace . testlinks
 
 deploy:
   stage: deploy
+  environment: production
+  image: resourcereasoning/website-deploy
+  tags:
+    - docker
+    - vtss_site
+  only:
+    - master
+  except:
+    - triggers
+  # DOC_DEPLOY_USER and DOC_DEPLOY_KEY should be defined as secret variables in the GitLab CI Settings panel
+  before_script:
+    - eval `ssh-agent`
+    - echo "$DOC_DEPLOY_KEY" | ssh-add -
   script:
-    - bundle exec rake deploy
+    - ./.deploy.sh
+
+# Special target triggered when publications repository is updated:
+update_publications:
+  stage: update
+  variables:
+    GIT_AUTHOR_NAME: Resource Reasoning Group Backup Bot
+    GIT_COMMITTER_NAME: Resource Reasoning Group Backup Bot
+    GIT_AUTHOR_EMAIL: rr-gitlab-bot@example.com
+    EMAIL: rr-gitlab-bot@example.com
+    # PUSH_KEY should be defined as a secret variable in the GitLab UI
+    SSH_KEY: $PUSH_KEY
+  image: ignoredambience/github-gitlab-sync
   tags:
-    - doc
+    - docker
+    - vtss_site
+  only:
+    - triggers
+  before_script:
+    - eval `ssh-agent`
+    - echo "$SSH_KEY" | ssh-add -
+  script:
+    - git checkout -B ${CI_COMMIT_REF_NAME}
+    - git submodule update --init --remote
+    - git add publications
+    - git commit -m "[AUTO] Updating publications submodule" || exit 0
+    - git remote rm rw || true
+    - git remote add rw git@gitlab.doc.ic.ac.uk:${CI_PROJECT_PATH}.git
+    - git push rw ${CI_COMMIT_REF_NAME}

.gitmodules

+[submodule "publications"]
+	path = publications
+	url = https://gitlab.doc.ic.ac.uk/verified-software/publications.git
+	branch = master

.htaccess

+CheckSpelling Off
+Options -Indexes
+
+RewriteEngine on
+
+# Rewrite former site subdomain pages to new site pages
+RewriteCond %{HTTP_HOST} =www-rw.doc.ic.ac.uk
+RewriteRule ^ http://vtss.doc.ic.ac.uk/research/javascript.html [R=301,L]
+
+RewriteCond %{HTTP_HOST} =www-lrr.doc.ic.ac.uk
+RewriteRule ^papers.html http://vtss.doc.ic.ac.uk/publications/ [R=301,L]
+RewriteCond %{HTTP_HOST} =www-lrr.doc.ic.ac.uk
+RewriteRule ^ca($|/) http://vtss.doc.ic.ac.uk/research/concurrency.html [R=301,L]
+
+# Bump any other subdomain request that gets here over to the main psvg site
+RewriteCond %{HTTP_HOST} !=vtss.doc.ic.ac.uk
+RewriteRule ^(.*)$ http://vtss.doc.ic.ac.uk/$1 [R=301,L]
+
+ErrorDocument 403 /403.html
+ErrorDocument 404 /404.html

403.md

+---
+layout: page
+title: "Error 403: Page Not Found"
+permalink: /403.html
+---
+
+Oops :(. This page is not verified, therefore clients should not access it.

404.md

+---
+layout: page
+title: "Error 404: Page Not Found"
+permalink: /404.html
+---
+
+Oops :(. This page is not verified, therefore clients should not access it.

Dockerfile

+FROM ruby:2.6
+
+# throw errors if Gemfile has been modified since Gemfile.lock
+RUN bundle config --global frozen 1
+RUN gem install bundler:1.16.6
+
+WORKDIR /usr/src/app
+
+COPY Gemfile Gemfile.lock ./
+RUN bundle install
+
+COPY . .
+
+RUN bundle exec rake init
+
+EXPOSE 4000
+
+CMD ["bundle", "exec", "jekyll", "serve", "--host", "0.0.0.0"]
\ No newline at end of file

Gemfile

 source 'https://rubygems.org'
 
+Encoding.default_external = Encoding::UTF_8
+
 gem 'rake'
-gem 'jekyll'
+group :build do
+  gem 'jekyll'
+end
 
-group :default, :jekyll_plugins do
-  gem 'jekyll-scholar', :git => 'https://github.com/inukshuk/jekyll-scholar.git', :ref => '4ef567dc730e373a9b000c97f210b899cd155e6a'
+group :build, :jekyll_plugins do
+  gem 'jekyll-scholar', '~> 5.10'
+  #gem 'jekyll-scholar', :git => '/home/thomas/jekyll-scholar', :branch => 'master'
+  gem 'jekyll-redirect-from'
+  gem 'jekyll-feed'
+  gem 'jekyll-sitemap'
 end
 
 group :test do
-  gem 'html-proofer'
+  gem 'html-proofer', '~> 3.0'
+end
+
+group :development do
 end

Gemfile.lock

-GIT
-  remote: https://github.com/inukshuk/jekyll-scholar.git
-  revision: 4ef567dc730e373a9b000c97f210b899cd155e6a
-  ref: 4ef567dc730e373a9b000c97f210b899cd155e6a
-  specs:
-    jekyll-scholar (5.6.0)
-      bibtex-ruby (~> 4.0, >= 4.0.13)
-      citeproc-ruby (~> 1.0)
-      csl-styles (~> 1.0)
-      jekyll (~> 3.0)
-
 GEM
   remote: https://rubygems.org/
   specs:
-    activesupport (4.2.5.1)
-      i18n (~> 0.7)
-      json (~> 1.7, >= 1.7.7)
+    activesupport (5.2.1)
+      concurrent-ruby (~> 1.0, >= 1.0.2)
+      i18n (>= 0.7, < 2)
       minitest (~> 5.1)
-      thread_safe (~> 0.3, >= 0.3.4)
       tzinfo (~> 1.1)
-    addressable (2.4.0)
-    bibtex-ruby (4.2.0)
+    addressable (2.5.2)
+      public_suffix (>= 2.0.2, < 4.0)
+    bibtex-ruby (4.4.7)
       latex-decode (~> 0.0)
-    citeproc (1.0.2)
-      namae (~> 0.8)
-    citeproc-ruby (1.1.0)
-      citeproc (>= 1.0.2, < 2.0)
-      csl (~> 1.4)
-    colorator (0.1)
-    colored (1.2)
-    csl (1.4.3)
-      namae (~> 0.7)
-    csl-styles (1.0.1.6)
+    citeproc (1.0.9)
+      namae (~> 1.0)
+    citeproc-ruby (1.1.10)
+      citeproc (~> 1.0, >= 1.0.9)
+      csl (~> 1.5)
+    colorator (1.1.0)
+    colorize (0.8.1)
+    concurrent-ruby (1.1.3)
+    csl (1.5.0)
+      namae (~> 1.0)
+    csl-styles (1.0.1.9)
       csl (~> 1.0)
-    ethon (0.8.1)
+    em-websocket (0.5.1)
+      eventmachine (>= 0.12.9)
+      http_parser.rb (~> 0.6.0)
+    ethon (0.11.0)
       ffi (>= 1.3.0)
-    ffi (1.9.10)
-    html-proofer (2.6.4)
-      activesupport (~> 4.2)
+    eventmachine (1.2.7)
+    ffi (1.9.25)
+    forwardable-extended (2.6.0)
+    html-proofer (3.9.2)
+      activesupport (>= 4.2, < 6.0)
       addressable (~> 2.3)
-      colored (~> 1.2)
+      colorize (~> 0.8)
       mercenary (~> 0.3.2)
-      nokogiri (~> 1.5)
+      nokogiri (~> 1.8.1)
       parallel (~> 1.3)
-      typhoeus (~> 0.7)
+      typhoeus (~> 1.3)
       yell (~> 2.0)
-    i18n (0.7.0)
-    jekyll (3.1.1)
-      colorator (~> 0.1)
+    http_parser.rb (0.6.0)
+    i18n (0.9.5)
+      concurrent-ruby (~> 1.0)
+    jekyll (3.8.5)
+      addressable (~> 2.4)
+      colorator (~> 1.0)
+      em-websocket (~> 0.5)
+      i18n (~> 0.7)
       jekyll-sass-converter (~> 1.0)
-      jekyll-watch (~> 1.1)
-      kramdown (~> 1.3)
-      liquid (~> 3.0)
+      jekyll-watch (~> 2.0)
+      kramdown (~> 1.14)
+      liquid (~> 4.0)
       mercenary (~> 0.3.3)
-      rouge (~> 1.7)
+      pathutil (~> 0.9)
+      rouge (>= 1.7, < 4)
       safe_yaml (~> 1.0)
-    jekyll-sass-converter (1.4.0)
+    jekyll-feed (0.11.0)
+      jekyll (~> 3.3)
+    jekyll-redirect-from (0.14.0)
+      jekyll (~> 3.3)
+    jekyll-sass-converter (1.5.2)
       sass (~> 3.4)
-    jekyll-watch (1.3.1)
+    jekyll-scholar (5.14.0)
+      bibtex-ruby (~> 4.0, >= 4.0.13)
+      citeproc-ruby (~> 1.0)
+      csl-styles (~> 1.0)
+      jekyll (~> 3.0)
+    jekyll-sitemap (1.2.0)
+      jekyll (~> 3.3)
+    jekyll-watch (2.1.2)
       listen (~> 3.0)
-    json (1.8.3)
-    kramdown (1.9.0)
-    latex-decode (0.2.2)
-      unicode (~> 0.4)
-    liquid (3.0.6)
-    listen (3.0.5)
-      rb-fsevent (>= 0.9.3)
-      rb-inotify (>= 0.9)
-    mercenary (0.3.5)
-    mini_portile2 (2.0.0)
-    minitest (5.8.4)
-    namae (0.10.1)
-    nokogiri (1.6.7.2)
-      mini_portile2 (~> 2.0.0.rc2)
-    parallel (1.6.1)
-    rake (10.5.0)
-    rb-fsevent (0.9.7)
-    rb-inotify (0.9.5)
-      ffi (>= 0.5.0)
-    rouge (1.10.1)
+    kramdown (1.17.0)
+    latex-decode (0.3.1)
+    liquid (4.0.1)
+    listen (3.1.5)
+      rb-fsevent (~> 0.9, >= 0.9.4)
+      rb-inotify (~> 0.9, >= 0.9.7)
+      ruby_dep (~> 1.2)
+    mercenary (0.3.6)
+    mini_portile2 (2.3.0)
+    minitest (5.11.3)
+    namae (1.0.1)
+    nokogiri (1.8.5)
+      mini_portile2 (~> 2.3.0)
+    parallel (1.12.1)
+    pathutil (0.16.2)
+      forwardable-extended (~> 2.6)
+    public_suffix (3.0.3)
+    rake (12.3.1)
+    rb-fsevent (0.10.3)
+    rb-inotify (0.9.10)
+      ffi (>= 0.5.0, < 2)
+    rouge (3.3.0)
+    ruby_dep (1.5.0)
     safe_yaml (1.0.4)
-    sass (3.4.21)
-    thread_safe (0.3.5)
-    typhoeus (0.8.0)
-      ethon (>= 0.8.0)
-    tzinfo (1.2.2)
+    sass (3.7.2)
+      sass-listen (~> 4.0.0)
+    sass-listen (4.0.0)
+      rb-fsevent (~> 0.9, >= 0.9.4)
+      rb-inotify (~> 0.9, >= 0.9.7)
+    thread_safe (0.3.6)
+    typhoeus (1.3.1)
+      ethon (>= 0.9.0)
+    tzinfo (1.2.5)
       thread_safe (~> 0.1)
-    unicode (0.4.4.2)
-    yell (2.0.5)
+    yell (2.0.7)
 
 PLATFORMS
   ruby
 
 DEPENDENCIES
-  html-proofer
+  html-proofer (~> 3.0)
   jekyll
-  jekyll-scholar!
+  jekyll-feed
+  jekyll-redirect-from
+  jekyll-scholar (~> 5.10)
+  jekyll-sitemap
   rake
 
 BUNDLED WITH
-   1.11.2
+   1.16.6

README.md

-Program Specification & Verification Group Website
-==================================================
+---
+layout: page
+title: VTSS Group Website Readme
+---
 
-[![Dependency Status](https://gemnasium.com/bd81b2aa11ff43417700f75dbd194221.svg)](https://gemnasium.com/6ba7afbbfda9adcba06f007cc565a29a)
+This readme file is published in its fully rendered form [on the website]({{site.baseurl}}{% link README.md %}).
 
-The source code for [this site](http://www-rw.doc.ic.ac.uk) is [hosted on the DoC GitLab server](https://gitlab.doc.ic.ac.uk/resource-reasoning/www-rw.doc.ic.ac.uk),
+The source code for [this site](https://vtss.doc.ic.ac.uk) is [hosted on the DoC GitLab server](https://gitlab.doc.ic.ac.uk/resource-reasoning/vtss.doc.ic.ac.uk),
 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**
+
+[![Build Status](https://gitlab.doc.ic.ac.uk/resource-reasoning/vtss.doc.ic.ac.uk/badges/master/build.svg)](https://gitlab.doc.ic.ac.uk/resource-reasoning/vtss.doc.ic.ac.uk/commits/master)
+[![Dependency Status](https://gemnasium.com/bd81b2aa11ff43417700f75dbd194221.svg)](https://gemnasium.com/6ba7afbbfda9adcba06f007cc565a29a)
+
+## Managing Content
+### Publications
+Please see [the dedicated publications repository](https://gitlab.doc.ic.ac.uk/resource-reasoning/publications) for
+instructions on how to add new publications to the website.
+
 Technical Detail
 ----------------
 This website is built using the [Jekyll](http://jekyllrb.com/) website framework.
 Pages can be written using
-[Markdown](http://daringfireball.net/projects/markdown/) (preferred) or HTML.
+[Markdown](https://github.com/adam-p/markdown-here/wiki/Markdown-Cheatsheet) (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).
 
@@ -25,13 +37,52 @@ permalink: /my-custom-page-path/
 ```
 
 Variables that templates currently take into account are:
-* title, sets the page title
-* menu, (default: true) places the page into the website's navigation menu
+
+* `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.
 
 The main content of the page should then follow.
 
-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.
+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.
+
+For the detail of adding publication, please refer to the README file in publication directory.
+
+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](_layouts/publication.html). The part of interest is
+the Source Materials section. We iterate through a
+[predefined list of file types](publications/_publication_file_types.yml) 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](publications.html) in the site's root just
+outputting a `{% bibliography %}` 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
 ----------------------
@@ -42,19 +93,32 @@ 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-rw` automatically on successful build.
+The site should be deployed automatically by GitLab CI. To deploy the site manually from your own machine, run the `.deploy.sh` script. This will use `rsync` to synchronise the contents of the `_site` directory with the webserver via SSH. Default deployment parameters:
+* DOC_DEPLOY_USER: the default username used by SSH to connect, usually the username on your local machine
+* DOC_DEPLOY_SERVER: `shell1.doc.ic.ac.uk`
+* DOC_DEPLOY_PATH: `/vol/rr/www`
+To override these parameters, set shell variables, eg: `DOC_DEPLOY_USER=me ./.deploy.sh`
+
+The site is deployed to `/vol/rr/www` automatically on successful build using the `.deploy.sh` script.
+The contents of the `DOC_DEPLOY_KEY` CI environment variable are used
+as the private key used to authenticate with the server. This key is currently configured to give locked-down rsync access to the
+`/vol/rr/www` using `pg`'s user account. For further details for how this is achieved, [see this
+howto](https://www.guyrutenberg.com/2014/01/14/restricting-ssh-access-to-rsync/). Note: when deploying to a locked-down
+rsync account, the DOC_DEPLOY_PATH should be set to a path relative to the lockdown path -- use `.` if in doubt. You
+won't need to set this if you're deploying from your own user account.
 
-Local Testing
--------------
+Locally Building and Testing
+----------------------------
 If you wish to test the site locally, ensure you have ruby installed, and then initially run:
 ```
-gem install bundle
+gem install bundler
 bundle install
+bundle exec rake init
 ```
 
 And to start a local webserver that remakes files whenever changed:
 ```
-rake serve
+bundle exec rake serve
 ```
 
 You can test for dead links and html errors using:

Rakefile

-require 'html/proofer'
+require 'html-proofer'
 
 task :default => :build
 
+desc "Initialise/update git submodules"
+task :init do
+  sh "git submodule update --init --remote"
+end
+
 desc "Build the site"
 task :build do
   sh "bundle exec jekyll build"
 end
 
-file_ignore = []
-url_ignore = []
+htmlproofer_config = {
+  :disable_external => true,
+  :check_html => true,
+  :parallel => { :in_processes => 1 },
+  :file_ignore => [/README.html/]
+}
 
 desc "Build the site and test output for dead links, invalid html etc."
 task :test => :build do
-  HTML::Proofer.new("./_site", {
-    :disable_external => true,
-    :validate_html => true,
-    :file_ignore => file_ignore,
-    :url_ignore => url_ignore
-  }).run
+  HTMLProofer.check_directory("./_site", htmlproofer_config).run
 end
 
 desc "Test dead external links"
 task :testlinks => :build do
-  HTML::Proofer.new("./_site", {
-    :validate_html => true,
-    :file_ignore => file_ignore,
-    :url_ignore => url_ignore,
-    :typhoeus => {
-      :ssl_verifypeer => false,
-      :ssl_verifyhost => 0
-    }
-  }).run
+  HTMLProofer.check_directory("./_site", htmlproofer_config.merge({
+    :disable_external => false
+  })).run
 end
 
 desc "Build the site, rebuild when files are edited, and serve via a local http server"
@@ -38,7 +36,7 @@ task :serve do
   sh "bundle exec jekyll serve"
 end
 
-desc "Deploy the site using rsync"
-task :deploy => :build do
-  sh "umask 0002 && rsync --chmod=Dg+s,ug+rwX,o+rX --chown=:rr -igr _site/ /vol/rr/www-rw"
+desc "Deploy the website to the webserver"
+task :deploy do
+  sh ".deploy.sh"
 end

_bibfiles/pgardner-conference-not-refereed.bib

-%San Francisco, CA, USA
-@InProceedings{gardner:cav:2015,
-  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})},
-  Year                  = {2015},
-  Pages                 = {3--10}, 
-  abstract              = {The JSCert project provides a Coq mechanised specification of the core JavaScript language. A key part of the project was to develop a methodology for establishing trust, by designing JSCert in such a way as to provide a strong connection with the JavaScript standard, and by developing JSRef, a reference interpreter which was proved correct with respect to JSCert and tested using the standard Test262 test suite. In this paper, we assess the previous state of the project at POPL?14 and the current state of the project at CAV?15. We evaluate the work of POPL?14, providing an analysis of the methodology as a whole and a more detailed analysis of the tests. We also describe recent work on extending JSRef to include Google?s V8 Array library, enabling us to cover more of the language and to pass more tests.}
-}
-
-@inproceedings{rochapinto:mpfs:2015,
-  title                 =  {{Steps in Modular Specifications for Concurrent Modules}},
-  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},
-  year                  =  {2015}, 
-  abstract              =  {The specification of a concurrent program module is a difficult problem. The specifications must be strong enough to enable reasoning about the intended clients without reference to the underlying module implementation. We survey a range of verification techniques for specifying concurrent modules, in particular highlighting four key concepts: auxiliary state, interference abstraction, resource ownership and atomicity. We show how these concepts combine to provide powerful approaches to specifying concurrent modules.}, 
-}
-
-@InProceedings{gardner:edbticdt:2010,
-  Title                 = {{Reasoning About Client-side Web Programs: Invited Talk}},
-  Author                = {Philippa Gardner},
-  Booktitle             = {Proceedings of the 2010 {EDBT/ICDT} Workshops, Lausanne, Switzerland, March 22-26, 2010},
-  Year                  = {2010}, 
-  abstract              = {In PODS 2008, I presented a paper on a formal, compositional specification of the Document Object Model (DOM), a W3C XML Update library. This work concentrated on Featherweight DOM, a small fragment of DOM which focuses on the XML tree structure and simple text nodes. Since the formal reasoning is compositional, we are able to work with a minimal set of commands and obtain complete reasoning for straight-line code. We are also able to verify, for example, invariant properties of simple DOM programs. This work is based on a recent breakthrough in program verification, based on analysing a program's use of resource. The idea is that the reasoning should follow the programmers' intuitions about which part of the computer memory the program touches. This style of reasoning was introduced by O'Hearn (Queen Mary) and Reynolds (CMU) in their work on Separation Logic for reasoning modularly about large C-programs (e.g. Microsoft device driver code, Linux). I substantially extended the range of local resource reasoning, introducing Context Logic to reason about programs that directly manipulate complex data structures such as XML. In this survey talk, I will give an overview of our theoretical and practical work on reasoning about DOM, highlighting recent developments which include: 1. the extension of this work to DOM Core Level 1. A substantial piece of work, not because of the reasoning, but because full DOM is large, underspecified and difficult to interpret, with no consensus between browsers; 2. reasoning about the combination of JavaScript and DOM to provide, for example, secure mashups for a more flexible, secure integration of outsourced payment services; 3. on-going work on a verification tool for automatically reasoning about DOM programs and the identification of key examples of web applications on which to test our DOM reasoning: e.g., with current technology, we can prove by hand that mashup programs are fault free; with our tool, such proofs will be automatic. An ultimate challenge is to develop the necessary reasoning technology to provide a safe and secure web environment on which to build the next generation of web applications, thus demonstrating the scientific feasibility of a reliable Web.}, 
-}
-
-%Rio de Janeiro, Brazil
-@InProceedings{gardner:wollic:2007,
-  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)},
-  Year                 = {2007},
-  Pages                = {189--202}, 
-  abstract             = {This paper provides a gentle introduction to Context Logic. It contains work previously published with Calcagno [1,2], and is based on Gardner?s notes for her course on Local Reasoning about Data Update at the Appsem PhD summer school [3] and Zarfaty?s thesis [4].}
-}
-
-
-@InProceedings{dinsdaleyoung:calco:2011,
-  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})},
-  Year                = {2011},
-  Pages               = {36--39}, 
-  abstract            = {Hoare logic ([7]) is an important tool for formally proving correctness properties of programs. It takes advantage of modularity by treating program fragments in terms of provable specifications. However, heap programs tend to break this type of modular reasoning by permitting pointer aliasing. For instance, the specification that a program reverses one list does not imply that it leaves a second list alone. To achieve this disjointness property, it is necessary to establish disjointness conditions
-throughout the proof.}
-}
\ No newline at end of file

_bibfiles/pgardner-journal-refereed.bib

-@Article{cardelli:tcs:2012,
-  Title                 = {{Processes in Space}},
-  Author                = {Luca Cardelli and Philippa Gardner},
-  Journal               = {Theoretical Computer Science},
-  Year                  = {2012},
-  Pages                 = {40--55},
-  Volume                = {431}, 
-  abstract              = {We introduce a geometric process algebra based on affine geometry, with the aim of describing the concurrent evolution of geometric structures in 3D space. We prove a relativity theorem stating that algebraic equations are invariant under rigid body transformations.}
-}
-
-@Article{calcagno:ic:2010,
-  Title                = {{Adjunct elimination in Context Logic for Trees}},
-  Author               = {Cristiano Calcagno and Thomas Dinsdale{-}Young and Philippa Gardner},
-  Journal              = {Information and Computation},
-  Year                 = {2010},
-  Number               = {5},
-  Pages                = {474--499}, 
-  Volume               = {208}, 
-  abstract             = {We study adjunct-elimination results for Context Logic applied to trees, following previous results by Lozes for Separation Logic and Ambient Logic. In fact, it is not possible to prove such elimination results for the original single-holed formulation of Context Logic. Instead, we prove our results for multi-holed Context Logic.}
-}
-
-@Article{cardelli:entcs:2009,
-  Title                = {{A Process Model of Actin Polymerisation}},
-  Author               = {Luca Cardelli and Emmanuelle Caron and Philippa Gardner and Ozan Kahramanogullari and Andrew Phillips},
-  Journal              = {Electronic Notes in Theoretical Computer Science},
-  Year                 = {2009},
-  Number               = {1},
-  Pages                = {127--144},
-  Volume               = {229}, 
-  abstract             = {Actin is the monomeric subunit of actin filaments which form one of the three major cytoskeletal networks in eukaryotic cells. Actin dynamics, be it the polymerisation of actin monomers into filaments or the reverse process, plays a key role in many cellular activities such as cell motility and phagocytosis. There is a growing number of experimental, theoretical and mathematical studies on the components of actin polymerisation and depolymerisation. However, it remains a challenge to develop compositional models of actin dynamics, e.g., by using differential equations. In this paper, we propose compositional process algebra models of actin polymerisation, and present a geometric representation of these models that allows to generate movies reflecting their dynamics.
},
-}
-
-@Article{cardelli:tcs:2009,
-  Title               = {{A Process Model of Rho GTP-binding Proteins}},
-  Author              = {Luca Cardelli and Emmanuelle Caron and Philippa Gardner and Ozan Kahramanogullari and Andrew Phillips},
-  Journal             = {Theoretical Computer Science},
-  Year                = {2009},
-  Number              = {33-34},
-  Pages               = {3166--3185},
-  Volume              = {410}, 
-  abstract            = {Rho GTP-binding proteins play a key role as molecular switches in many cellular activities. In response to extracellular stimuli and with the help from regulators (GEF, GAP, Effector, GDI), these proteins serve as switches that interact with their environment in a complex manner. Based on the structure of a published ordinary differential equations (ODE) model, we first present a generic process model for the Rho GTP- binding proteins, and compare it with the ODE model. We then extend the basic model to include the behaviour of the GDIs and explore the parameter space for the extended model with respect to biological data from the literature. We discuss the challenges this extension brings and the directions of further research. In particular, we present techniques for modular representation and refinement of process models, where, for example, different Rho proteins with different rates for regulator interactions can be given as the instances of the same parametric model.}, 
-}
-
-@Article{raza:lmcs:2009,
-  Title              = {{Footprints in Local Reasoning}},
-  Author             = {Mohammad Raza and Philippa Gardner},
-  Journal            = {Logical Methods in Computer Science},
-  Year               = {2009},
-  Number             = {2},
-  Volume             = {5}, 
-  abstract           = {Local reasoning about programs exploits the natural local behaviour common in programs by focussing on the footprint - that part of the resource accessed by the program. We address the problem of formally characterising and analysing the footprint notion for abstract local functions introduced by Calcagno, O?Hearn and Yang. With our definition, we prove that the footprints are the only essential elements required for a complete specification of a local function. We formalise the notion of small specifications in local reasoning and show that for well-founded resource models, a smallest specification always exists that only includes the footprints, and also present results for the non-well-founded case. Finally, we investigate the conditions under which the footprints correspond to the smallest safe states, and present a heap model in which, unlike the standard model, this is the case for every program.}, 
-}
-
-@Article{cardelli:ents:2008,
-  Title              = {{A Process Model of Rho GTP-binding Proteins in the Context of Phagocytosis}},
-  Author             = {Luca Cardelli and Philippa Gardner and Ozan Kahramanogullari},
-  Journal            = {Electronic Notes in Theoretical Computer Science},
-  Year               = {2008},
-  Number             = {3},
-  Pages              = {87--102},
-  Volume             = {194}, 
-  abstract           = {At the early stages of the phagocytic signalling, Rho GTP-binding proteins play a key role. With the stimulus from the cell membrane and with the help from the regulators (GEF, GAP, Effector, GDI), these proteins serve as switches that interact with their environment in a complex manner. We present a generic process model for the Rho GTP-binding proteins, and compare it with a previous model that uses ordinary differential equations. We then extend the basic model to include the behaviour of the GDIs. We discuss the challenges this extension brings and directions of further research.}, 
-}
-
-@Article{maffeis:jlap:2008,
-  Title               = {{Behavioural Equivalences for Dynamic Web Data}},
-  Author              = {Sergio Maffeis and Philippa Gardner},
-  Journal             = {Logic and Algebraic Programming},
-  Year                = {2008},
-  Number              = {1},
-  Pages               = {86--138},
-  Volume              = {75}, 
-  abstract            = {We study behavioural equivalences for dynamic web data in Xdn, a model for reasoning about behaviour found in (for example) dynamic web page programming, applet interaction, and web-service orchestration. Xdn is based on an idealised model of semistructured data, and an extension of the 7r-calculus with locations and operations for interacting with data. The equivalences are nonstandard due to the integration of data and processes, and the presence of locations. }, 
-}
-
-@Article{calcagno:entcs:2007,
-  Title               = {{Local Reasoning about Data Update}},
-  Author              = {Cristiano Calcagno and Philippa Gardner and Uri Zarfaty},
-  Journal             = {Electronic Notes on Theoretical Computer Science},
-  Year                = {2007},
-  Pages               = {133--175},
-  Volume              = {172}, 
-  abstract            = {We present local Hoare reasoning about data update, using Context Logic for analysing structured data. We apply our reasoning to tree update, heap update which is analogous to local Hoare reasoning using Separation Logic, and term rewriting.}
-
-@Article{cardelli:entcs:2007,
-  Title               = {{Manipulating Trees with Hidden Labels}},
-  Author              = {Luca Cardelli and Philippa Gardner and Giorgio Ghelli},
-  Journal             = {Electronic Notes in Theoretical Computer Science},
-  Year                = {2007},
-  Pages               = {177--201},
-  Volume              = {172}, 
-  abstract            = {We define an operational semantics and a type system for manipulat- ing semistructured data that contains hidden information. The data model is sim- ple labeled trees with a hiding operator. Data manipulation is based on pattern matching, with types that track the use of hidden labels.}
-}
-
-@Article{dawar:ic:2007,
-  Title              = {{Expressiveness and Complexity of Graph Logic}},
-  Author             = {Anuj Dawar and Philippa Gardner and Giorgio Ghelli},
-  Journal            = {Information and Computation},
-  Year               = {2007},
-  Number             = {3},
-  Pages              = {263--310},
-  Volume             = {205}, 
-  abstract           = {We investigate the complexity and expressive power of a spatial logic for reasoning about graphs. This logic was previously introduced by Cardelli, Gardner and Ghelli, and provides the simplest setting in which to explore such results for spatial logics. We study several forms of the logic: the logic with and without recursion, and with either an exponential or a linear version of the basic composition operator. We study the combined complexity and the expressive power of the four combinations. We prove that, without recursion, the linear and exponential versions of the logic correspond to significant fragments of first-order (FO) and monadic second-order (MSO) Logics; the two versions are actually equivalent to FO and MSO on graphs representing strings. However, when the two versions are enriched with ?-style recursion, their expressive power is sharply increased.Both are able to express PSPACE-complete problems, although their combined complexity and data complexity still belong to PSPACE.}, 
-}
-
-@Article{gardner:ic:2007,
-  Title              = {{Linear Forwarders}},
-  Author             = {Philippa Gardner and Cosimo Laneve and Lucian Wischik},
-  Journal            = {Information and Computation},
-  Year               = {2007},
-  Number             = {10},
-  Pages              = {1526--1550},
-  Volume             = {205},
-  abstract           = {A linear forwarder is a process that receives one message on a channel and sends it on a different channel. We use linear forwarders to provide a distributed implementation of Milner?s asynchronous pi calculus. Such a distributed implementation is known to be difficult due to input capability, where a received name is used as the subject of a subsequent input. This allows the dynamic creation of large input processes in the wrong place, thus requiring comparatively large code migrations in order to avoid consensus problems. Linear forwarders constitute a small atom of input capability that is easy to move.
We show that the full input capability can be simply encoded using linear for- warders. We also design a distributed machine, demonstrating the ease with which we can implement the pi calculus using linear forwarders. We also show that lin- ear forwarders allow for a simple encoding of distributed choice and have ?clean? behaviour in the presence of failures.},
-}
-
-@Article{wischik:tcs:2005,
-  Title             = {{Explicit Fusions}},
-  Author            = {{Lucian Wischik and Philippa Gardner}},
-  Journal           = {Theoretical Computer Science},
-  Year              = {2005},
-  Number            = {3},
-  Pages             = {606--630},
-  Volume            = {340}, 
-  abstract          = {We introduce explicit fusions of names. An explicit fusion is a process that exists concurrently with the rest of the system and enables two names to be used interchangeably. Explicit fusions provide a small-step account of reaction in process calculi such as the pi calculus and the fusion calculus. In this respect they are similar to the explicit substitutions of Abadi, Cardelli and Curien, which do the same for the lambda calculus. In this paper, we give a technical foundation for explicit fusions. We present the pi-F calculus, a simple process calculus with explicit fusions, and define a strong bisimulation congruence. We study the embeddings of the fusion calculus and the pi calculus. The former is fully abstract with respect to bisimulation.}, 
-}
-
-@Article{gardner:tcs:2005,
-  Title            =  {{Modelling Dynamic Web Data}},
-  Author           = {Philippa Gardner and Sergio Maffeis},
-  Journal          = {Theoretical Computer Science},
-  Year             = {2005},
-  Number           = {1},
-  Pages            = {104--131},
-  Volume           = {342}, 
-  abstract         = {We introduce Xd?, a peer-to-peer model for reasoning about the dynamic behaviour of web data. It is based on an idealised model of semi-structured data, and an extension of the $\pi$-calculus with process mobility and with an operation for interacting with data. Our model can be used to reason about behaviour found in, for example, dynamic web page programming, applet interaction, and service orchestration. We study behavioural equivalences for Xd$\pi$, motivated by examples.}
-}
-
-@Article{gardner:tcs:1999,
-  Title           = {Closed Action Calculi},
-  Author          = {Philippa Gardner},
-  Journal         = {Theoretical Computer Science},
-  Year            = {1999},
-  Number          = {1-2},
-  Pages           = {77--103},
-  Volume          = {228}, 
-  abstract        = {Action calculi provide a framework for capturing many kinds of interactive behaviour by focussing on the primitive notion of names. We introduce a name-free account of action calculi, called the closed action calculi, and show that there is a strong correspondence between the original presentation and the name-free presentation. We also add free names plus natural axioms to the closed world, and show that the abstraction operator can be constructed as a derived operator. Our results show that in some sense names are inessential. However, the purpose of action calculi is to understand formalisms which mimic the behaviour of interactive systems. Perhaps more significantly therefore, these results highlight the important presentational role that names play.}, 
-}
-
-@Article{gardner:entcs:1997,
-  Title           = {A Type-theoretic Description of Action Calculi},
-  Author          = {Philippa Gardner},
-  Journal         = {Electronic Notes in Theoretical Computer Science},
-  Year            = {1997},
-  Pages           = {52},
-  Volume          = {10}, 
-  abstract        = {Action calculi, introduced by Milner, provide a framework for investigating models of interaction. This talk will focus on the connection between action calculi and known concepts arising from type theory. The aim of this work is to isolate what is distinctive about action calculi, and to investigate the potential of action calculi as an underlying framework for many kinds of computational behaviour.The first part of the talk will introduce action calculi. In the second part, I'll give a type-theoretic account of action calculi, using the general binding operators of Aczel. I will discuss two extensions: higher-order action calculi which correspond to Moggi's commutative computational lambda-calculus, and linear action calculi which correspond to the linear type theories of Barber and Benton.This talk is based on joint work with Andrew Barber, Masahito Hasegawa and Gordon Plotkin. If time, I will also describe current work arising from the connections described above. }
-}
-
-@Article{gardner:entcs:1995,
-  Title          = {{A Name-free Account of Action Calculi}},
-  Author         = {Philippa Gardner},
-  Journal        = {Electronic Notes in Theoretical Computer Science},
-  Year           = {1995},
-  Pages          = {214--231},
-  Volume         = {1}, 
-  abstract       = {Action calculi provide a unifying framework for representing a variety of models of communication, such as CCS, Petri nets and the ?-calculus, within a unified setting. A central idea is to model the interaction between actions using names. We introduce a name-free account of action calculi, called the closed action calculi, and show that there is a strong correspondence between the original presentation and the name-free presentation. These results show that, although names play an important presentational role, they are in some sense inessential.}
-}
-
-@Article{gardner:mscs:1995,
-  Title           = {{Equivalences between Logics and their Representing Type Theories}},
-  Author          = {Philippa Gardner},
-  Journal         = {Mathematical Structures in Computer Science},
-  Year            = {1995},
-  Number          = {3},
-  Pages           = {323--349},
-  Volume          = {5}, 
-  abstract        = {We propose a new framework for representing logics, called LF+, which is based on the Edinburgh Logical Framework. The new framework allows us to give, apparently for the first time, general definitions that capture how well a logic has been represented. These definitions are possible because we are able to distinguish in a generic way that part of the LF+ entailment corresponding to the underlying logic. This distinction does not seem to be possible with other frameworks. Using our definitions, we show that, for example, natural deduction first-order logic can be well-represented in LF, whereas linear and relevant logics cannot. We also show that our syntactic definitions of representation have a simple formulation as indexed isomorphisms, which both confirms that our approach is a natural one and provides a link between type-theoretic and categorical approaches to frameworks.},
-}
-
-@Article{gardner:mscs:1991,
-  Title           = {{Unfold/Fold Transformations in Logic Programming}},
-  Author          = {Philippa Gardner},
-  Journal         = {Mathematical Structures in Computer Science},
-  Year            = {1991},
-  Number          = {2},
-  Pages           = {143--157},
-  Volume          = {02}, 
-  abstract        = {Unfold/fold transformation rules for disjunctive logic programs are proposed in this paper. Our transformation rules preserve the meaning of the programs.}, 
-}
-
-

_config.yml

-title: Concurrency
-subtitle: Program Specification and Verification Group</br><a href="http://www.doc.ic.ac.uk">Department of Computing</a>, <a href="http://www.imperial.ac.uk/">Imperial College London</a>
+title: Verified Software
+subtitle: <a href="http://www.doc.ic.ac.uk">Department of Computing</a>, <a href="http://www.imperial.ac.uk/">Imperial College London</a>
 copyright: Imperial College London
 
 baseurl: ""
-url: "http://http://www-rw.doc.ic.ac.uk/"
+url: "https://vtss.doc.ic.ac.uk"
 
 markdown: kramdown
 
+encoding: utf-8
+timezone: Europe/London
+
 include:
   - .htaccess
 exclude:
   - Gemfile*
   - Rakefile
   - .gitlab-ci.yml
-  - README.md
+  - vendor
+  - publications/README.md
 
 collections:
   people:
     output: true
+  research:
+    output: true
+  teaching:
+    output: true
 
 defaults:
   -
     scope:
       path: ""
     values:
-      layout: "page"
+      layout: page
       menu: false
       menu_order: 9
+  -
+    scope:
+      type: posts
+    values:
+      layout: post
   -
     scope:
       path: ""
       type: people
     values:
       layout: person
+  -
+    scope:
+      path: "research"
+    values:
+      layout: research
+  -
+    scope:
+      path: "teaching"
+    values:
+      layout: teaching
 
 scholar:
-  source: .
+  source: publications
   bibliography: publications.bib
   bibliography_template: publication-entry
   details_link: ""
   details_dir: publications
   details_layout: publication.html
 
-  use_raw_bibtex_entry: true
-  bibtex_skip_fields: ['month_numeric']
+  use_raw_bibtex_entry: false
+  bibtex_skip_fields: ['month_numeric', 'project', 'file']
+  bibtex_filters:
+    - superscript
+    - latex
 
-  sort_by: year
+  sort_by: year, month
   order: descending
   group_order: descending
   bibliography_group_tag: 'h3,h4,h5,h6'

_data/external_assets.yml

@@ -26,8 +26,8 @@ fontawesome:
     integrity: "sha384-XdYbMnZ/QjLh6iI4ogqCTaIjrFk87ip+ekIjefZch0Y+PvJ8CDYtEs1ipDmPorQ+"
 
 mathjax:
-  uri: "http://cdn.mathjax.org/mathjax/"
-  version: "latest"
+  uri: "https://cdnjs.cloudflare.com/ajax/libs/mathjax/"
+  version: "2.7.5"
   js:
     path: "/MathJax.js?config=TeX-AMS-MML_HTMLorMML"
     async: true

_data/publication_file_types.yml

+../publications/_publication_file_types.yml
\ No newline at end of file

_includes/alumni.html

+<div class="people panel">
+
+  {% assign grouped_people = include.people | group_by: 'position' | sort: 'name' %}
+  {% for group in grouped_people %}
+  {% assign position = group.name %}
+  {% assign id = group.name | replace:' ','-' %}
+  <div class="panel-heading">
+    <h6 class="panel-title">
+      <a data-toggle="collapse" href="#{{id}}" style="color:black">{{position}}s ↯</a>
+    </h6>
+  </div>
+
+  <div id="{{id}}" class="panel-collapse collapse">
+    {% for person in group.items %}
+    <div class="row">
+      <div class="col-sm-1" >
+        <a href="{{ person.url }}" >{% include person-photo-small.html %}</a>
+      </div>
+      <div class="col-sm-11">
+        <a href="{{ person.url }}" class="h6" style="color:black;font-weight:bold;">{{ person.firstname }} {{ person.lastname }}</a>
+        {{ person.content | remove: '<p>' | remove: '</p>' }}
+      </div>
+    </div>
+    <br/>
+    {% endfor %}
+  </div>
+  {% endfor %}
+</div>

_includes/footer.html

 <footer class="site-footer">
-  <p>&copy; {{ site.time | date: "%Y" }} {{ site.copyright }}</p>
+  <p>&copy; {{ site.time | date: "%Y" }} {{ site.copyright }}<br />
+  <a href="https://www.imperial.ac.uk/about-the-site/privacy/">Privacy Notice</a> - <a href="{{ '/accessibility/' | relative_url }}">Accessibility</a></p>
 </footer>