Martin joined the group as a Research Associate in 2018. His work focused on a formalism called skeletons to represent the semantics of real-world programming languages (JavaScript, R, etc.) He also was part of the team working on the formalisation of WebAssembly/Wasm in Coq. In 2020 Martin was appointed CRCN (chargé de recherche de classe normale) in the Sound Programming of Adaptive Dependable Embedded Systems (Spades) group at Inria Grenoble-Rhône-Alpes Research Centre, France.

Group Publications

  1. Two Mechanisations of WebAssembly 1.0

    Proceedings of the 24th international symposium of Formal Methods (FM21), Beijing, China; November 20-25, 2021

  2. Skeletal Semantics and their Interpretations

    Proceedings of the 46th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL’19)

  3. A Trusted Mechanised JavaScript Specification

    Proceedings of the 41st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL’14), pp. 87–100