Martin Bodin — Home page

I am Martin Bodin¹, member of the Spades team, in Grenoble, at Inria.

My research interests are mainly around programming languages design, formalisations, and analyses. I work with the Coq/Rocq proof assistant, which provides strong guarantees to the softwares I build. I am especially interested in applying formal methods to real-world programming languages. Such languages usually come with many special (possibly unexpected) behaviours, which can lead to serious programming mistakes. I believe that formal methods can help programmers detect and avoid these mistakes.

I currently work with the IREM within the LiberAbaci project. The goal is to understand how to design mathematics courses including Coq/Rocq-based tutoriels, by working with mathematics teachers, for mathematics students (and not computer sciences’s).

In my research, I also formalised widely used programming languages (JavaScript, R, and WebAssembly). These formalisations (with the exception of WebAssembly) are notably large compared to other formalisations from the field. I thus helped design skeletons, a formalism to express and derive formally-proven program analyses from such large formalisations.

I did my PhD at Inria Rennes under the supervision of Alan Schmitt and Thomas Jensen. My PhD was about formal analyses of the JavaScript programming language. More information can be found in my thesis companion.

I did a postdoc in the CMM, in Santiago de Chile, where I formalised the R programming language in Coq/Rocq. The formalisation is available online.

I then did a postdoc at the Imperial College, in London, in the Verified Trustworthy Software Specification research group. It led to two Coq/Rocq formalisations: skeletal semantics, and WebAssembly.

¹ Pronounced /maʁtɛ̃ bodɛ̃/. I am also known as Martin Constantino–Bodin /maʁtɛ̃ kɔnstɐ̃ntino bodɛ̃/.