Verified Software

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

   • Conrad Watt
   • Xiaojia Rao
   • Jean Pichon-Pharabod
   • Martin Bodin
   • Philippa Gardner

   Proceedings of the 24^th international symposium of Formal Methods (FM21), Beijing, China; November 20-25, 2021, pp. 61–79

2. Skeletal Semantics and their Interpretations

   • Martin Bodin
   • Philippa Gardner
   • Thomas Jensen
   • Alan Schmitt

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

3. A Trusted Mechanised JavaScript Specification

   • Martin Bodin
   • Arthur Charguéraud
   • Daniele Filaretti
   • Philippa Gardner
   • Sergio Maffeis
   • Daiva Naudziuniene
   • Alan Schmitt
   • Gareth Smith

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