diff --git a/publications.bib b/publications.bib
index e89df8254c74b4e7ae2b6923baeddda3ac98ca23..4f21a3432532cd8dcb2fc8c9590a707b2b05b6fa 100644
--- a/publications.bib
+++ b/publications.bib
@@ -1825,16 +1825,16 @@ previously unknown bugs.},
 }
 
 @Article{DOsualdo2020TaDa,
-  author    = {Emanuele D'Osualdo and
-               Azadeh Farzan and
-               Philippa Gardner and
-               Julian Sutherland},
-  title     = {TaDA Live: Compositional Reasoning for Termination of Fine-grained
-               Concurrent Programs},
-  journal   = {CoRR},
-  volume    = {abs/1901.05750},
-  year      = {2020},
-  abstract  = {We present TaDA Live, a concurrent separation logic for reasoning compositionally about the termination of
+author    = {Emanuele D'Osualdo and
+            Azadeh Farzan and
+            Philippa Gardner and
+            Julian Sutherland},
+title     = {TaDA Live: Compositional Reasoning for Termination of Fine-grained
+            Concurrent Programs},
+journal   = {CoRR},
+volume    = {abs/1901.05750},
+year      = {2020},
+abstract  = {We present TaDA Live, a concurrent separation logic for reasoning compositionally about the termination of
 blocking fine-grained concurrent programs. The crucial challenge is how to deal with abstract atomic blocking:
 that is, abstract atomic operations that have blocking behaviour arising from busy-waiting patterns as found in,
 for example, fine-grained spin locks. Our fundamental innovation is with the design of abstract specifications
@@ -1873,23 +1873,23 @@ certificate of correctness. We provide a prototype implementation and we report
 on some textbook examples.},
 }
 
- @inproceedings{Maksimovic2021Gillian,
-  author    = {Petar Maksimovic and
-               Sacha{-}{\'{E}}lie Ayoun and
-               Jos{\'{e}} Fragoso Santos and
-               Philippa Gardner},
-  editor    = {Alexandra Silva and
-               K. Rustan M. Leino},
-  title     = {Gillian, Part {II:} Real-World Verification for JavaScript and {C}},
-  booktitle = {Computer Aided Verification - 33rd International Conference, {CAV}
+@InProceedings{Maksimovic2021Gillian,
+author    = {Petar Maksimovic and
+            Sacha{-}{\'{E}}lie Ayoun and
+            Jos{\'{e}} Fragoso Santos and
+            Philippa Gardner},
+editor    = {Alexandra Silva and
+            K. Rustan M. Leino},
+title     = {Gillian, Part {II:} Real-World Verification for JavaScript and {C}},
+booktitle = {Computer Aided Verification - 33rd International Conference, {CAV}
                2021, Virtual Event, July 20-23, 2021, Proceedings, Part {II}},
-  series    = {Lecture Notes in Computer Science},
-  volume    = {12760},
-  pages     = {827--850},
-  publisher = {Springer},
-  year      = {2021},
-  doi       = {10.1007/978-3-030-81688-9\_38},
-  abstract  = {We introduce verification based on separation logic to Gillian,
+series    = {Lecture Notes in Computer Science},
+volume    = {12760},
+pages     = {827--850},
+publisher = {Springer},
+year      = {2021},
+doi       = {10.1007/978-3-030-81688-9\_38},
+abstract  = {We introduce verification based on separation logic to Gillian,
 a multi-language platform for the development of symbolic analysis tools
 which is parametric on the memory model of the target language. Our
 work develops a methodology for constructing compositional memory
@@ -1900,6 +1900,39 @@ designing common abstractions used for both verification tasks, and find
 two bugs in the JavaScript and three bugs in the C implementation.},
 }
 
+@InProceedings{Watt2021Two,
+author = {Conrad Watt and
+          Xiaojia Rao and 
+          Jean Pichon-Pharabod and
+          Martin Bodin and 
+          Philippa Gardner},
+title = {Two mechanisations of WebAssembly 1.0},
+booktitle = {Proceedings of the 24th international symposium of Formal Methods (FM21), Beijing, China; November 20-25, 2021},
+year = {2021},
+abstract = {WebAssembly (Wasm) is a new bytecode language supported
+by all major Web browsers, designed primarily to be an efficient compilation
+target for low-level languages such as C/C++ and Rust. It is unusual in that 
+it is officially specified through a formal semantics. An initial draft 
+specification was published in 2017 with an associated mechanised 
+specification in Isabelle/HOL published by Watt that found
+bugs in the original specification, fixed before its publication. 
+The  first official W3C standard, WebAssembly 1.0, was published in
+2019. Building on Watt's original mechanisation, we introduce two 
+mechanised specifications of the WebAssembly 1.0 semantics, written
+in different theorem provers: WasmCert-Isabelle and WasmCert-Coq. 
+Wasm's compact design and official formal semantics enable our mechanisations
+to be particularly complete and close to the published language standard. 
+We present a high-level description of the language's updated
+type soundness result, referencing both mechanisations. 
+We also describe the current state of the mechanisation of language features not previously
+supported: WasmCert-Isabelle includes a verified executable definition 
+of the instantiation phase as part of an executable verified interpreter;
+WasmCert-Coq includes executable parsing and numeric definitions as 
+on-going work towards a more ambitious end-to-end verified interpreter
+which does not require an OCaml harness like WasmCert-Isabelle.},
+}
+ 
+
 @Comment{jabref-meta: databaseType:bibtex;}
 
 @Comment{jabref-meta: saveActions:enabled;