Martin Bodin is a Research Associate with the group.

Martin is currently working 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. He is also working on a formalisation of WebAssembly/Wasm in Coq.

Martin Bodin did his PhD on formal analyses of the JavaScript programming language at at the University of Rennes 1 under the supervision of Alan Schmitt and Thomas Jensen. He was part of the JSCert project 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.

Martin is a keen speaker of Esperanto.

Group Publications

  1. Skeletal Semantics and their Interpretations

    PACMPL, vol. 3( POPL)

  2. A Trusted Mechanised JavaScript Specification

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