diff --git a/Dawar2004Adjunct.extended.pdf b/Dawar2004Adjunct.extended.pdf
new file mode 100644
index 0000000000000000000000000000000000000000..36823fd6cedfdb53edd163d2b077f239591448d4
Binary files /dev/null and b/Dawar2004Adjunct.extended.pdf differ
diff --git a/publications.bib b/publications.bib
index b2078f1ab00814feaeeff1cc84b8ffb471b81919..3003d8617264b990ad923dda4e23f45a7cbd6c9a 100644
--- a/publications.bib
+++ b/publications.bib
@@ -629,10 +629,11 @@ We present JSCert, a formalisation of the current ECMA standard in the Coq proof
   volume    = {3328},
   series    = {Lecture Notes in Computer Science},
   pages     = {211--223},
+  month     = dec,
   publisher = {Springer},
   abstract  = {Spatial logics are used to reason locally about disjoint data structures. They consist of standard first-order logic constructs, spatial (structural) connectives and their corresponding adjuncts. Lozes has shown that the adjuncts add no expressive power to a spatial logic for analysing tree structures, a surprising and important result. He also showed that a related logic does not have this adjunct elimination property. His proofs yield little information on the generality of adjunct elimination. We present a new proof of these results based on model-comparison games, and strengthen Lozes' results. Our proof is directed by the intuition that adjuncts can be eliminated when the corresponding moves are not useful in winning the game. The proof is modular with respect to the operators of the logic, providing a general technique for determining which combinations of operators admit adjunct elimination.},
   doi       = {10.1007/978-3-540-30538-5_18},
-  file      = {Dawar2004Adjunct.pdf:Dawar2004Adjunct.pdf:PDF},
+  file      = {Dawar2004Adjunct.pdf:Dawar2004Adjunct.pdf:PDF;:Dawar2004Adjunct.extended.pdf:PDF},
   project   = { TBD },
 }