README.md

@@ -5,11 +5,13 @@ This repository contains the group's (and its members') publications, BibTeX
 references, and associated materials.
 
 ## How to Deposit a Publication.
-1. To fulfill funding and REF requirements and for long-term archival, all papers and
-   tech reports should be deposited into
-   [Imperial Spiral](http://spiral.imperial.ac.uk/) within THREE MONTHS OF ACCEPTANCE. Do this now, so you don't
-   forget. Once this is done, email Teresa with a copy of the accepted submission so that she can publish the details of 
-the acceptance in the news section of the website.
+1. To fulfill funding and REF requirements and for long-term archival, all
+   papers and tech reports should be deposited into
+   [Imperial Spiral](http://spiral.imperial.ac.uk/) within THREE MONTHS OF
+   ACCEPTANCE. Do this now, so you don't forget.
+
+2. Email Teresa with a copy of the accepted submission so that she can publish
+   the details of the acceptance in the news section of the website.
 
 2. Create a BibTeX record for the publication in
    the [publications.bib](publications.bib) file. Post-publication, records can
@@ -19,33 +21,76 @@ the acceptance in the news section of the website.
    appropriate version of each field, as they all usually vary in quality.
    See below for BibTeX style notes.
 
-3. Commit files associated with the publication in this directory. Files should
-   be named with the bibtex key as the base of the file name, and the
-   appropriate extension from the table below according to document purpose.
+3. Commit files associated with the publication to this directory. *Files
+   should be named with the bibtex key as the root of the file name*, and the
+   appropriate extension from the section below according to document purpose.
 
 ## Copyright Notes
-You should check with the publisher's T&Cs (in particular the Copyright waiver
-form) to determine which version of the paper you are allowed to publish here.
-Often it is only the pre-print edition that is passed to the publisher
-**before** they make any changes. The final proof copy and the publisher's own
-copy is often not permitted to be published.
-
-## BibTeX Record Structure
-Record keys have the preferred format of `<first author surname><year><first
-word of title>`
-
-Fields:
-* **doi**: Please remove the `http://dx.doi.org/` prefix, so the doi is of the
-  form `nn.nnnn/....`]
-* **url**: This field should **not** contain a duplicate of the doi. It
+** Please take careful note of this section!**
+
+You **must** check with the publisher's T&Cs (in particular the Copyright
+waiver form) to determine which version of the paper you are allowed to publish
+here. Often it is only the *pre-print* edition that is passed to the publisher
+*before* they make any changes. The final proof copy and the publisher's own
+copy is usually not permitted to be published on the author's own website.
+
+## BibTeX
+A BibTeX record looks like this:
+```bibtex
+@Type{Key,
+  field = {value},
+  field = {value},
+}```
+
+For details of the possible types of entries, and their minimal set of required
+fields, see [the Wikipedia BibTeX article](https://en.wikipedia.org/wiki/BibTeX#Entry_types).
+
+For the group websites, we've chosen a BibTeX key format of:
+`<first author surname><year><first word of title>`, this is used as the
+record's key in the `publications.bib` file, and as the root of the filename
+for each associated file (article, slides, etc) in this repository.
+
+In values, Surround special characters and characters requiring exact
+capitalisation in `{}` curly braces. For example:
+`Naud{\v{z}}i{\={u}}nien{\.{e}}` and `{ECMAS}cript`.
+
+### Fields Style Guide
+* **author**: Author names should be separated by `and`, names can be in either
+  the `Last, First` *(preferred)* or `First Last` style.
+  Multiple-word last names should use the `Last, First` style to minimise
+  confusion. For example: `da Rocha Pinto, Pedro and Fragoso Santos, Jos{\'e}
+  and D'Osualdo, Emanuele`. For further details of how BibTeX treats names, see
+  [this summary](http://artis.imag.fr/~Xavier.Decoret/resources/xdkbibtex/bibtex_summary.html#names).
+* **doi**: Please remove the `http://dx.doi.org/` prefix, so the DOI, so it is
+  of the form `nn.nnnn/xyzabc`. For display on the website, this value will be
+  prefixed with `http://dx.doi.org/` to produce a link to the publisher's
+  article website.
+* **url**: This field should **not** contain a duplicate of the doi. It is
   generally only used to link to the publisher's version if the publisher does
-  not also issue a DOI.
-* **month**: Add the exact date of the conference as publication date. 
-  This will keep the file hidden until the actual publication date.
+  not also issue a DOI. If the publisher's link is the same location as the DOI
+  after redirections, then it should not be filled in the url field.
+* **month**: **Required** The first three letters of the month of publication (possibly in
+  the future). This field does not require quoting or placing into braces.
+  The standard months are: jan, feb, mar, apr, may, jun, jul, aug, sep, oct,
+  nov, dec. For example: `month = mar,`.
+  Publications will not appear on the websites until their month of
+  publication (as per Philippa's policy decision).
+* **year**: **Required** Year of publication.
 * **file**: This field is added automatically by the JabRef reference manager,
   it is ignored by the website. It is mostly useful as a quick check in the
   JabRef user interface that all publications have an associated file. See next
   section for file matching on the website.
+* **booktitle**: For the `@inproceedings` type, this is the title of the
+  conference proceedings. Different publishers prefer different (long) styles,
+  Philippa usually prefers something short like POPL'12. We may need to find a
+  way to standardise on this.
+
+### Further Reading/References
+* [Wikipedia BibTeX article](https://en.wikipedia.org/wiki/BibTeX)
+* The [BibTeX FAQ](http://mirrors.ctan.org/biblio/bibtex/contrib/doc/btxFAQ.pdf)
+* [Xavier Decoret's guide](http://artis.imag.fr/~Xavier.Decoret/resources/xdkbibtex/bibtex_summary.html)
+* [Tame the BeaST](http://www.lsv.fr/~markey/BibTeX/doc/ttb_en.pdf), by Nicolas
+  Markey
 
 ## Publication File Extension Types
 Publication file types are listed in the configuration file

publications.bib

@@ -93,7 +93,6 @@ We present JSCert, a formalisation of the current ECMA standard in the Coq proof
   title     = {Reasoning About POSIX File Systems},
   school    = {Imperial College London},
   year      = {2017},
-  month     = may,
   type      = {phdthesis},
   abstract  = {POSIX is a standard for operating systems, with a substantial part devoted to specifying file-system operations. File-system operations exhibit complex concurrent behaviour, comprising multiple actions affecting different parts of the state: typically, multiple atomic reads followed by an atomic update. However, the standard's description of concurrent behaviour is unsatisfactory: it is fragmented; contains ambiguities; and is generally under-specified. We provide a formal concurrent specification of POSIX file systems and demonstrate scalable reasoning for clients. Our speciation is based on a concurrent specification language, which uses a modern concurrent separation logic for reasoning about abstract atomic operations, and an associated refinement calculus. Our reasoning about clients highlights an important difference between reasoning about modules built over a heap, where the interference on the shared state is restricted to the operations of the module, and modules built over a file system, where the interference cannot be restricted as the file system is a public namespace. We introduce specifications conditional on context invariants used to restrict the interference, and apply our reasoning to lock files and named pipes. Program reasoning based on separation logic has been successful at verifying that programs do not crash due to illegal use of resources, such invalid memory accesses. The underlying assumption of separation logics, however, is that machines do not fail. In practice, machines can fail unpredictably for various reasons, such as power loss, corrupting resources or resulting in permanent data loss. Critical software, such as file systems and databases, employ recovery methods to mitigate these effects. We introduce an extension of the Views framework to reason about programs in the presence of such events and their associated recovery methods. We use concurrent separation logic as an instance of the framework to illustrate our reasoning, and explore programs using write-ahead logging, such a stylised ARIES recovery algorithm.},
   file      = {Ntzik2017Reasoning.pdf:Ntzik2017Reasoning.pdf:PDF},
@@ -127,6 +126,21 @@ We present JSCert, a formalisation of the current ECMA standard in the Coq proof
   project   = { concurrency },
 }
 
+
+@InProceedings{FragosoSantos2017Towards,
+  author    = {Jos{\'{e}} {Fragoso Santos} and Philippa Gardner and Petar Maksimovi\'{c} and Daiva Naud\v{z}i\={u}nien\.{e}},
+  title     = {{Towards Logic-based Verification of JavaScript Programs}},
+  booktitle = {Proceedings of 26\textsuperscript{th} Conference on Automated Deduction {(CADE 26)}},
+  year      = {2017},
+  month     = aug,
+  abstract  = {In this position paper, we argue for what we believe is a correct pathway to achieving scalable symbolic verification of JavaScript based on separation logic. We highlight the difficulties imposed by the language, the current state-of-the-art in the literature, and the  sequence of steps that needs to be taken. We briefly describe \javert, our semi-automatic toolchain for JavaScript verification.},
+  doi       = {10.1007/978-3-319-63046-5_2},
+  file      = {FragosoSantos2017Towards.pdf:FragosoSantos2017Towards.pdf:PDF},
+  project   = {web},
+  url       = {https://link.springer.com/chapter/10.1007/978-3-319-63046-5_2},
+}
+
+
 @InProceedings{Cerone2017Algebraic,
   author    = {Andrea Cerone and Alexey Gotsman and Hongseok Yang},
   title     = {Algebraic Laws for Weak Consistency},
@@ -149,39 +163,6 @@ We present JSCert, a formalisation of the current ECMA standard in the Coq proof
   project   = {concurrency},
 }
 
-@InProceedings{DBLP:conf/cade/SantosGMN17,
-  author    = {Jos{\'{e}} Fragoso Santos and Philippa Gardner and Petar Maksimovic and Daiva Naudziuniene},
-  title     = {Towards Logic-Based Verification of JavaScript Programs},
-  booktitle = {Automated Deduction - {CADE} 26 - 26th International Conference on Automated Deduction, Gothenburg, Sweden, August 6-11, 2017, Proceedings},
-  year      = {2017},
-  editor    = {Leonardo de Moura},
-  volume    = {10395},
-  series    = {Lecture Notes in Computer Science},
-  pages     = {8--25},
-  publisher = {Springer},
-  bibsource = {dblp computer science bibliography, http://dblp.org},
-  biburl    = {http://dblp.uni-trier.de/rec/bib/conf/cade/SantosGMN17},
-  doi       = {10.1007/978-3-319-63046-5_2},
-  timestamp = {Wed, 12 Jul 2017 10:06:41 +0200},
-  url       = {https://doi.org/10.1007/978-3-319-63046-5_2},
-}
-
-@InProceedings{DBLP:conf/aplas/RaadSG16,
-  author    = {Azalea Raad and Jos{\'{e}} Fragoso Santos and Philippa Gardner},
-  title     = {{DOM:} Specification and Client Reasoning},
-  booktitle = {Programming Languages and Systems - 14th Asian Symposium, {APLAS} 2016, Hanoi, Vietnam, November 21-23, 2016, Proceedings},
-  year      = {2016},
-  editor    = {Atsushi Igarashi},
-  volume    = {10017},
-  series    = {Lecture Notes in Computer Science},
-  pages     = {401--422},
-  bibsource = {dblp computer science bibliography, http://dblp.org},
-  biburl    = {http://dblp.uni-trier.de/rec/bib/conf/aplas/RaadSG16},
-  doi       = {10.1007/978-3-319-47958-3_21},
-  timestamp = {Fri, 19 May 2017 01:25:54 +0200},
-  url       = {https://doi.org/10.1007/978-3-319-47958-3_21},
-}
-
 @Article{DBLP:journals/entcs/PintoDG15,
   author    = {Pedro da Rocha Pinto and Thomas Dinsdale{-}Young and Philippa Gardner},
   title     = {Steps in Modular Specifications for Concurrent Modules (Invited Tutorial Paper)},
@@ -228,21 +209,6 @@ We present JSCert, a formalisation of the current ECMA standard in the Coq proof
   url       = {https://doi.org/10.4230/DagRep.5.5.1},
 }
 
-@InProceedings{DBLP:conf/popl/BodinCFGMNSS14,
-  author    = {Martin Bodin and Arthur Chargu{\'{e}}raud and Daniele Filaretti and Philippa Gardner and Sergio Maffeis and Daiva Naudziuniene and Alan Schmitt and Gareth Smith},
-  title     = {A trusted mechanised JavaSript specification},
-  booktitle = {The 41st Annual {ACM} {SIGPLAN-SIGACT} Symposium on Principles of Programming Languages, {POPL} '14, San Diego, CA, USA, January 20-21, 2014},
-  year      = {2014},
-  editor    = {Suresh Jagannathan and Peter Sewell},
-  pages     = {87--100},
-  publisher = {{ACM}},
-  bibsource = {dblp computer science bibliography, http://dblp.org},
-  biburl    = {http://dblp.uni-trier.de/rec/bib/conf/popl/BodinCFGMNSS14},
-  doi       = {10.1145/2535838.2535876},
-  timestamp = {Thu, 15 Jun 2017 01:00:00 +0200},
-  url       = {http://doi.acm.org/10.1145/2535838.2535876},
-}
-
 @Proceedings{DBLP:conf/esop/2013,
   title     = {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},
   year      = {2013},
@@ -439,18 +405,20 @@ We present JSCert, a formalisation of the current ECMA standard in the Coq proof
   timestamp = {Sun, 28 May 2017 01:00:00 +0200},
   url       = {https://doi.org/10.1016/j.tcs.2005.03.017},
 }
-
-@Proceedings{DBLP:conf/dagstuhl/2004P4241,
-  title     = {Graph Transformations and Process Algebras for Modeling Distributed and Mobile Systems, 6.-11. June 2004},
-  year      = {2005},
-  editor    = {Barbara K{\"{o}}nig and Ugo Montanari and Philippa Gardner},
-  volume    = {04241},
+@proceedings{DBLP:conf/dagstuhl/2004P4241,
+  editor    = {Barbara K{\"{o}}nig and
+               Ugo Montanari and
+               Philippa Gardner},
+  title     = {Graph Transformations and Process Algebras for Modeling Distributed
+               and Mobile Systems, 6.-11. June 2004},
   series    = {Dagstuhl Seminar Proceedings},
+  volume    = {04241},
   publisher = {IBFI, Schloss Dagstuhl, Germany},
-  bibsource = {dblp computer science bibliography, http://dblp.org},
-  biburl    = {http://dblp.uni-trier.de/rec/bib/conf/dagstuhl/2004P4241},
-  timestamp = {Wed, 07 Jan 2015 00:00:00 +0100},
+  year      = {2005},
   url       = {http://drops.dagstuhl.de/portals/04241/},
+  timestamp = {Wed, 07 Jan 2015 18:21:20 +0100},
+  biburl    = {http://dblp.uni-trier.de/rec/bib/conf/dagstuhl/2004P4241},
+  bibsource = {dblp computer science bibliography, http://dblp.org}
 }
 
 @InProceedings{DBLP:conf/fossacs/WischikG04,
@@ -470,21 +438,6 @@ We present JSCert, a formalisation of the current ECMA standard in the Coq proof
   url       = {https://doi.org/10.1007/978-3-540-24727-2_34},
 }
 
-@Proceedings{DBLP:conf/concur/2004,
-  title     = {{CONCUR} 2004 - Concurrency Theory, 15th International Conference, London, UK, August 31 - September 3, 2004, Proceedings},
-  year      = {2004},
-  editor    = {Philippa Gardner and Nobuko Yoshida},
-  volume    = {3170},
-  series    = {Lecture Notes in Computer Science},
-  publisher = {Springer},
-  isbn      = {3-540-22940-X},
-  bibsource = {dblp computer science bibliography, http://dblp.org},
-  biburl    = {http://dblp.uni-trier.de/rec/bib/conf/concur/2004},
-  doi       = {10.1007/b100113},
-  timestamp = {Tue, 30 May 2017 01:00:00 +0200},
-  url       = {https://doi.org/10.1007/b100113},
-}
-
 @InProceedings{DBLP:conf/dagstuhl/KonigMG04,
   author    = {Barbara K{\"{o}}nig and Ugo Montanari and Philippa Gardner},
   title     = {04241 Abstracts Collection - Graph Transformations and Process Algebras for Modeling Distributed and Mobile Systems},
@@ -1275,6 +1228,20 @@ Building on separation logic with concurrent abstract predicates (CAP), we intro
   project   = { concurrency, tada },
 }
 
+@Proceedings{DBLP:conf/concur/2004,
+  title     = {{CONCUR} 2004 - Concurrency Theory, 15th International Conference, London, UK, August 31 - September 3, 2004, Proceedings},
+  year      = {2004},
+  editor    = {Philippa Gardner and Nobuko Yoshida},
+  volume    = {3170},
+  series    = {Lecture Notes in Computer Science},
+  publisher = {Springer},
+  isbn      = {3-540-22940-X},
+  bibsource = {dblp computer science bibliography, http://dblp.org},
+  biburl    = {http://dblp.uni-trier.de/rec/bib/conf/concur/2004},
+  doi       = {10.1007/b100113},
+  url       = {https://doi.org/10.1007/b100113},
+}
+
 @Comment{jabref-meta: databaseType:bibtex;}
 
 @Comment{jabref-meta: saveActions:enabled;