Update bodin.md

_people/bodin.md

@@ -3,19 +3,27 @@
 firstname: Martin
 lastname: Bodin
 position: Research Associate
-webpage:  https://www.doc.ic.ac.uk/~mbodin
+webpage:  www.doc.ic.ac.uk/~mbodin
 email: m.bodin@imperial.ac.uk
 github:  
 alumnus: false
 projects:
   - web
 ---
-Martin Bodin is a Research Associate with the group. Martin Bodin did his PhD at 
-the [University of Rennes 1](https://english.univ-rennes1.fr/) under the supervision 
+Martin Bodin is a Research Associate with the group.  
+
+Martin is currently working on a formalism called skeletons to represent the semantics 
+of real-world language, in order to get as many properties as possible [certified in the Coq 
+proof assistant](https://coq.inria.fr). He is also workiing on 
+a [formalisation of WebAssembly/Wasm in Coq](https://github.com/Imperial-Wasm/wasm-coq-public).
+
+Martin Bodin did his PhD on [formal analyses of the JavaScript programming 
+language](https://www.doc.ic.ac.uk/~mbodin/doktorigxo/companion.html?lang=en#en) at at the 
+[University of Rennes 1](https://english.univ-rennes1.fr/) under the supervision 
 of [Alan Schmitt]( http://people.rennes.inria.fr/Alan.Schmitt/index.html) 
 and [Thomas Jensen]( https://www.researchgate.net/profile/Thomas_Jensen3). 
-He participated to the [JSCert project]( http://www.jscert.org/) to build a Coq 
+He was part of the [JSCert project]( http://www.jscert.org/) to build a Coq 
 specification for JavaScript. He applied the same formalising technique to build 
 a semantics for R during his postdoc at the [University of Chile]( http://www.cmm.uchile.cl/). 
-These specifications come with a high degree of confidence, but also with a large size. 
-His current work focuses on building and proving abstract analyses for such large semantics.
+
+Martin is a [keen speaker of Esperanto](https://www.doc.ic.ac.uk/~mbodin/index.html?lang=eo#eo).
\ No newline at end of file