From 34c1fe40eefbb0bcf8424a1e4d5c23a2cd9b608a Mon Sep 17 00:00:00 2001 From: Teresa Carbajo-Garcia <t.carbajo-garcia@imperial.ac.uk> Date: Wed, 7 Oct 2020 16:47:37 +0100 Subject: [PATCH] Update 2020-10-01-martin.md --- _posts/2020-10-01-martin.md | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/_posts/2020-10-01-martin.md b/_posts/2020-10-01-martin.md index d698372..adf3353 100644 --- a/_posts/2020-10-01-martin.md +++ b/_posts/2020-10-01-martin.md @@ -1,11 +1,11 @@ --- -title: Goodby and best of luck to Martin Bodin +title: Goodbye and best of luck to Martin Bodin --- -Goodbye and our best wishes to Martin Bodin who is leaving the group to join [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) in the [Sound Programming of Adaptive Dependable Embedded Systems (Spades)](https://team.inria.fr/spades/) group. +Goodbye and our best wishes to Martin Bodin who is leaving the group to join [the Inria Grenoble-Rhône-Alpes Research Centre](https://www.inria.fr/en/centre-inria-grenoble-rhone-alpes), France, as a CRCN (chargé de recherche de classe normale) in the [Sound Programming of Adaptive Dependable Embedded Systems (Spades)](https://team.inria.fr/spades/) group. The [Spades group’s research focuses on component-based programming: analysis of embedded systems, both in term of correctness and efficiency (time or energy use) and Martin will work in particular on the topic of Skeletal Semantics as Certified Analyses of Real-world Programs. You can read more about his proposed research below. Many programming languages used in industry are complex. This complexity is sometimes associated to deep research questions, like pointer arithmetic or concurrency. However, this complexity is sometimes only due to special behaviours of these languages. Languages likes JavaScript or R are known for such unexpected special behaviours. Such programming languages are thus frequently idealised in research. This unfortunately narrows the application of formal analyses. My research aims at developing formalisms (namely, skeletal semantics in the context of the Coq proof assistant) that enable the application of analyses of such complex languages, in particular in the context of real-time systems. -Ni deziras al vi bonÅancon en via nova posto ĉe Inria, Martin! \ No newline at end of file +Ni deziras al vi bonÅancon en via nova posto ĉe Inria, Martin! -- GitLab