From ec730687735cf2dbdd9ada29cd27617ca80e4030 Mon Sep 17 00:00:00 2001 From: Teresa Carbajo-Garcia <t.carbajo-garcia@imperial.ac.uk> Date: Wed, 7 Oct 2020 16:58:20 +0100 Subject: [PATCH] Update bodin.md --- _people/bodin.md | 9 ++++----- 1 file changed, 4 insertions(+), 5 deletions(-) diff --git a/_people/bodin.md b/_people/bodin.md index 57c3f8f..ac3a647 100644 --- a/_people/bodin.md +++ b/_people/bodin.md @@ -9,9 +9,8 @@ alumnus: true projects: - web --- -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. - -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 +Martin joined the group as a Research Associate in 2018. His 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). \ No newline at end of file +[formalisation of WebAssembly/Wasm in Coq](https://github.com/Imperial-Wasm/wasm-coq-public). + +In 2020 Martin was appointed CRCN (chargé de recherche de classe normale) in the [Sound Programming of Adaptive Dependable Embedded Systems (Spades)](https://team.inria.fr/spades/) group at [Inria Grenoble-Rhône-Alpes Research Centre](https://www.inria.fr/en/centre-inria-grenoble-rhone-alpes), France. \ No newline at end of file -- GitLab