Martin Bodin

Martin Bodin is a Researcher at Inria in Grenoble, France, where he is a member of the Spades team. Previously, he completed a PhD at Inria Rennes and held postdoctoral positions at the Center for Mathematical Modeling (CMM) in Santiago de Chile and at Imperial College London in the Verified Trustworthy Software Specification research group.

Dr. Bodin's research focuses on programming languages design, formalizations, and analyses. He specializes in applying formal methods to real-world programming languages using the Coq/Rocq proof assistant. His work addresses the challenge of formalizing complex languages with many special behaviors that can lead to serious programming mistakes. He believes formal methods can help programmers detect and avoid these mistakes.

His research has resulted in formalizations of widely used programming languages including JavaScript, R, and WebAssembly. Notably, his formalizations of JavaScript and R are among the largest in the field. To manage this complexity, he helped design "skeletons," a formalism to express and derive formally-proven program analyses from large formalizations.

Currently, Dr. Bodin is working with IREM within the LiberAbaci project to understand how to design mathematics courses that incorporate Coq/Rocq-based tutorials, collaborating with mathematics teachers for mathematics students.