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

Mi estas Martin Bodin¹, skipano de Spades, en Grenoblo, ĉe Inria.

Je suis Martin Bodin¹, membre de l’équipe Spades, à Grenoble, à l’Inria.

My research interests are mainly around programming languages design, formalisations, and analyses. I work with the Coq 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.

Mia esploradinteresoj ĉefe fokusiĝas pri programlingvaĵaj elkreoj, formalizigoj, kaj analizoj. Mi laboras kun la Coq pruvilo, kiu alte fidigas la programaĵojn kiujn mi kreas. Mi specife interesiĝas pri apliki formalajn metodojn al industrie uzitajn programlingvaĵojn. Tiaj lingvaĵojn elmontremas specialajn (kaj kelkfoje neatenditajn) komportamentojn, kiuj povas konduki al gravaj programeraroj. Mi pensas ke formalaj metodoj povas helpi programistojn ekscii kaj eviti tiajn erarojn.

Mes thèmes de recherches se concentrent majoritairement autour de la conception, la formalisation, et les analyses de langages de programmation. Je travaille avec l’assistant de preuve Coq, qui garantit un haut niveau de confiance aux programmes que je conçois. Je suis particulièrement intéressé par l’application des méthodes formelles aux langages de programmation fréquemment utilisés en industrie. Ces langages ont souvent des comportements spéciaux parfois inattendus, qui peuvent mener à des erreurs de programmation importantes. Je pense que les méthodes formelles peuvent aider les programmeurs à détecter et éviter ces erreurs.

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

Mi nuntempe laboras kun la IREM pere de la projekto LiberAbaci. La celo de tiu projekto temas pri kompreni kiel krei matematikajn kursojn parte-bazitaj en Coq, laborante kun matematikaj instruistoj, kaj celante matematikajn studentojn (kaj ne komputikajn).

Je travaille actuellement avec l’IREM dans le cadre du projet LiberAbaci. Le projet consiste à comprendre comment concevoir des cours de mathématiques incluant des TPs Coq, en partenariat avec des professeurs de mathématiques, le tout dans un cursus mathématique (et non informatique).

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.

En mia esplorado, mi formaligis multuzitajn programlingvaĵojn (JavaScript, R, kaj WebAssembly). Tiuj formaligadoj (krom WebAssembly) rimarkiĝas per siaj grandecoj kompare al aliaj formaligoj el la fako. Mi do helpis elkrei la ostarojn, kiu estas formalaĵo por defini kaj elkrei formalpruvitajn programanalizojn el tiaj grandaj formaligoj.

Parmi mes travaux, j’ai aussi formalisé des langages de programmation très utilisés (JavaScript, R, et WebAssembly). Ces formalisations (à l’exception de WebAssembly) se distinguent des autres formalisations du domaine par leur taille importante. J’ai donc participé à la conception des squelettes, un formalisme pour exprimer et dériver des analyses de programmes certifiées à partir de telles 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.

Mi doktoriĝis ĉe Inria Rennes superrigardite de Alan Schmitt kaj Thomas Jensen. Mi tiam laboris pri formala analizo de la Javaskripta programlingvaĵo. Pli da informoj troviĝas en mia kundoktoriĝdokumento.

J’ai fait mon doctorat à Inria, à Rennes, sous la supervision d’Alan Schmitt et de Thomas Jensen. Je travaillais alors sur l’analyse formelle du langage de programmation JavaScript. Plus d’informations peuvent se trouver sur mon guide de thèse.

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

Mi postdoktoriĝis ĉe la CMM, en Santiago, en Ĉilio. Mi tiam formaligis la programlingvaĵon R en Coq. La formaligado disponeblas rete.

J’ai fait un post-doc au CMM, à Santiago, au Chili. J’y ai formalisé le langage de programmation R en Coq. La formalisation est disponible en ligne.

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

Mi poste postdoktoriĝis ĉe Imperial College, en Londono, je la esplorada grupo Verified Trustworthy Software Specification. Ĝi alkondukis al du Coqaj formaligaĵoj: pri ostaraj semantikoj, kaj WebAssembly.

J’ai ensuite été post-doctorant à l’Imperial College, à Londres, dans le groupe de recherche Verified Trustworthy Software Specification. Ce post-doc a conduit à deux formalisations Coq: une sur les sémantiques squelettiques, et une sur WebAssembly.

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

¹ Prononcita /maʁtɛ̃ bodɛ̃/. Mi ankaŭ estas konata kiel Martin Constantino–Bodin /maʁtɛ̃ kɔnstɐ̃ntino bodɛ̃/.

¹ Prononcé /maʁtɛ̃ bodɛ̃/. On me connait aussi sous le nom de Martin Constantino–Bodin /maʁtɛ̃ kɔnstɐ̃ntino bodɛ̃/.