Language Specifiaction and Program Verification

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

   Formal Methods (FM) 2021

2. Skeletal Semantics and their Interpretations

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

   POPL 2019

3. A Trusted Mechanised JavaScript Specification

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

   POPL 2014