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. Skeletal Semantics and their Interpretations

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

   PACMPL, vol. 3( POPL)

2. A Trusted Mechanised JavaScript Specification

   • Martin Bodin
   • Arthur Charguéraud
   • Daniele Filaretti
   • Philippa Gardner
   • Sergio Maffeis
   • Daiva Naudžiūnienė
   • Alan Schmitt
   • Gareth Smith

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