Mi estas Martin Bodin1, finiĝante mian postdoktoradon ĉe Imperial College, en Londono, je la esplorada grupo Verified Trustworthy Software Specification. Mi baldaŭ estos skipano de Spades, en Grenoblo, ĉe Inria.
Je suis Martin Bodin1, en transition de post-doctorant à l’Imperial College, à Londres, dans le groupe de recherche Verified Trustworthy Software Specification. Je serais bientôt membre de l’équipe Spades, à Grenoble, à l’Inria.
I am Martin Bodin1, in transition from a postdoc at the Imperial College, in London, in the Verified Trustworthy Software Specification research group. I will soon be part of the Spades team, in Grenoble, at Inria.
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.
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.
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.
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.
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.
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 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.
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.
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 de nombreux 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.
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 many 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.
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.
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 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 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 for code-quality control in industry.
¹ Prononcita /maʁtɛ̃ bodɛ̃/. Mi ankaŭ estas konata kiel Martin Constantino–Bodin.
¹ Prononcé /maʁtɛ̃ bodɛ̃/. On me connait aussi sous le nom de Martin Constantino–Bodin.
¹ Pronounced /maʁtɛ̃ bodɛ̃/. I am also known as Martin Constantino–Bodin.
- Nuna pozicio
- Postdoktorulo ĉe Imperial College, en Londono.
- Skipo
- Verified Trustworthy Software Specification
- Vivresumo
- Havebla tie ĉi
- Publikaj ŝlosiloj
- Interreta ĉeesto
- Position actuelle
- Post-doctorant à l’Imperial College, à Londres.
- Équipe
- Verified Trustworthy Software Specification
- CV
- Disponible ici
- Clefs publiques
- Présence sur Internet
- Current position
- Postdoc at the Imperial College, in London.
- Team
- Verified Trustworthy Software Specification
- CV
- Available there
- Public keys
- Internet presence