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

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

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

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 les 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.

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.

Parmi mes travaux, j’ai ainsi 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. J’ai bon espoir que ces projets permettrons de concevoir des outils de controle de qualité de code pour l’industrie.

In my research, I thus 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 hope that these projects will help designing practical tools for code-quality control in industry.

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, iu formalaĵo por defini kaj elkrei formalpruvitajn programanalizojn el tiaj grandaj formaligoj. Mi esperas ke tiaj projektoj helpos krei praktikajn ilojn por industrie kontroli kodkvaliton.

Je travaille actuellement sur un formalisme, les squelettes, représentant la sémantique de langages de programmation complexes (JavaScript, R, etc.). Ce formalisme permet de déduire avec un effort minimal toute une gamme d’analyses de programmes certifiées dans l’assistant de preuve Coq. Je travaille aussi sur une formalisation de WebAssembly/Wasm en Coq.

I am currently working on a formalism called skeletons to represent the semantics of real-world programming languages (JavaScript, R, etc.). This formalism enables to derive with minimal effort a wide range of program analyses certified in the Coq proof assistant. I am also working on a formalisation of WebAssembly/Wasm in Coq.

Mi nun laboras pri formalismo (kiu nomiĝas ostaron) por reprezenti la semantikon de vervivaj programlingvaĵoj (Javaskripto, R, ktp.). Ĉi tiu formalismo permesigas dedukti granddiversajn programanalizojn pruvitajn en la Coq pruvilo. Mi ankaŭ laboras pri formaligado de WebAssembly/Wasm en Coq.

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 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 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 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 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.

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.

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

¹ 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ɛ̃/.