Martin Bodin was a Research Associate with the group.
Martin Bodin was a Research Associate with the group. In 2020 Martin joined the [Inria Grenoble-Rhône-Alpes Research Centre](https://www.inria.fr/en/centre-inria-grenoble-rhone-alpes) as a CRCN (chargé de recherche de classe normale) with the [Sound Programming of Adaptive Dependable Embedded Systems (Spades)](https://team.inria.fr/spades/) group.
Martin's work focused on a formalism called skeletons to represent the semantics
While at Imperial, Martin's work focused on a formalism called skeletons used 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 also was part of the team working on the
[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 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/).
Martin is a [keen speaker of Esperanto](https://www.doc.ic.ac.uk/~mbodin/index.html?lang=eo#eo).
[formalisation of WebAssembly/Wasm in Coq](https://github.com/Imperial-Wasm/wasm-coq-public).
