diff --git a/_people/bodin.md b/_people/bodin.md index b73eff2730576718b114ad06a1dea7bc495f6287..da976048a79e45ff7e2ab9af7447d3e717c2ab52 100644 --- a/_people/bodin.md +++ b/_people/bodin.md @@ -5,16 +5,16 @@ position: Researcher webpage: https://www.doc.ic.ac.uk/~mbodin email: m.bodin@imperial.ac.uk github: -alumnus: false +alumnus: true projects: - web --- -Martin Bodin is a Research Associate with the group. +Martin Bodin was a Research Associate with the group. -Martin is currently working on a formalism called skeletons to represent the semantics +Martin's work focused 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 working on -a [formalisation of WebAssembly/Wasm in Coq](https://github.com/Imperial-Wasm/wasm-coq-public). +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 @@ -25,4 +25,4 @@ 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). \ No newline at end of file +Martin is a [keen speaker of Esperanto](https://www.doc.ic.ac.uk/~mbodin/index.html?lang=eo#eo).