Je suis Martin Bodin¹, post-doctorant au Imperial College, à Londres, dans le groupe de recherche Verified Trustworthy Software Specification.

Mi estas Martin Bodin¹, postdoktorulo ĉe Imperial College, en Londono, je la esplorada grupo Verified Trustworthy Software Specification.

I am Martin Bodin¹, postdoc at the Imperial College, in London, in the Verified Trustworthy Software Specification research group.

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.

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

I am currently working on a formalism called skeletons to represent the semantics of real-world language (JavaScript, R, etc.). This formalism enables to derive with a 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.

Avant cela, j’ai fait un postdoc au CMM, à Santiago, au Chili. J’y ai formalisé le langage de programmation R en Coq. La formalisation est disponible en ligne.

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

Before this, 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.

J’ai fait mon doctorat à Inria de 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.

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.

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.

Mes thèmes de recherches se concentrent sur la conception et les analyses de langages de programmation. Je travaille avec l’assistant de preuve Coq, qui garantit un haut niveau de confiance pour 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 une large gamme de comportements spéciaux, souvent 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.

Mia esploradinteresoj fokusiĝas ĉirkaŭ programlingvaĵaj elkreok kaj analizoj. Mi laboras kun la Coq pruvilo, kiu donas altan fidon al la programaĵojn kiujn mi kreas. Mi specife interesiĝas en apliki formalajn metodojn al vervivajn programlingvaĵojn. Tiaj lingvaĵojn emas elmontri granddiversajn specialajn (kaj kelkfoje neatenditajn) komportamentojn, kiuj povas elkrei gravajn programerarojn. Mi pensas ke formalaj metodoj povas helpi programistojn ekscii kaj eviti tiajn erarojn.

My research interests are focussed around programming languages design and analyses. I work with the Coq proof assistant, which provides high confidence to the softwares I build. I am especially interested in applying formal methods to real-world programming languages. These languages usually come with a large range of special (and sometimes unexpected) behaviours, which can lead to serious programming mistakes. I believe that formal methods can help programmers detect and avoid these mistakes.

Parmi mes travaux, j’ai ainsi formalisé des langages de programmation très utilisés (JavaScript, R, et Wasm). Ces formalisations se différencient 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 programme certifiées à partir de telles formalisations. J’ai bon espoir que ces projets permettrons de concevoir des outils pratiques de controle de qualité de code dans l’industrie.

En mia esplorado, mi do formaligis multe uzitajn programlingvaĵojn (JavaScript, R, kaj Wasm). Tiuj formaligadoj rimarkiĝas per siaj grandecoj kompare al aliaj formaligadoj de la fako. Mi do helpis elkrei la ostarojn, iu formalaĵo por defini kaj elkrei formalpruvitajn programanalizojn el tiaj grandaj formaligadoj. Mi esperas ke tiaj projektoj helpos krei praktikajn ilojn uzitaj por kontroli kodkvaliton industrie.

In my research, I thus formalised widely used programming languages (JavaScript, R, and Wasm). These formalisations 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 used for code-quality control in industry.

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

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

¹ Pronounced /maʁtɛ̃ bodɛ̃/. I am also known as Martin Constantino–Bodin.