FM 2021
Conrad Watt, Xiaojia Rao, Jean Pichon-Pharabod, Martin Bodin, and Philippa Gardner, Two Mechanisations of WebAssembly 1.0, International Symposium on Formal Methods, 2021, DOI: 10.1007/978-3-030-90870-6_4.
Research
Esplorado
Travaux de recherche
Link
Hide
Show
Hide All
Show All
Ligilo
Malafiŝi
Afiŝi
Malafiŝi ĉion
Afiŝi ĉion
Lien
Cacher
Montrer
Cacher tout
Montrer tout
I am a member of the Spades team, in Grenoble, at Inria.
Mi estas skipano de Spades, en Grenoblo, ĉe Inria.
Je suis membre de l’équipe Spades, à Grenoble, à l’Inria.
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).
This page lists my publications. You can also check my Orcid, DBLP, or Google Scholar profile.
Ĉi tiu paĝo listas miajn eldonaĵojn. Vi ankaŭ povas kontroli miajn profilojn ĉe Orcid, DBLP, aŭ Google Scholar.
Cette page liste mes publications. Vous pouvez aussi consulter mon profil Orcid, DBLP, ou Google Scholar.
Conrad Watt, Xiaojia Rao, Jean Pichon-Pharabod, Martin Bodin, and Philippa Gardner, Two Mechanisations of WebAssembly 1.0, International Symposium on Formal Methods, 2021, DOI: 10.1007/978-3-030-90870-6_4.
Conrad Watt, Xiaojia Rao, Jean Pichon-Pharabod, Martin Bodin, kaj Philippa Gardner, Two Mechanisations of WebAssembly 1.0, International Symposium on Formal Methods, 2021, DOI: 10.1007/978-3-030-90870-6_4.
Conrad Watt, Xiaojia Rao, Jean Pichon-Pharabod, Martin Bodin, et Philippa Gardner, Two Mechanisations of WebAssembly 1.0, International Symposium on Formal Methods, 2021, DOI : 10.1007/978-3-030-90870-6_4.
Martin Bodin, Philippa Gardner, Thomas Jensen, and Alan Schmitt, Skeletal Semantics and Their Interpretations, Symposium on Principles of Programming Languages, 2019, DOI: 10.1145/3290357.
Martin Bodin, Philippa Gardner, Thomas Jensen, kaj Alan Schmitt, Skeletal Semantics and Their Interpretations, Symposium on Principles of Programming Languages, 2019, DOI: 10.1145/3290357.
Martin Bodin, Philippa Gardner, Thomas Jensen, et Alan Schmitt, Skeletal Semantics and Their Interpretations, Symposium on Principles of Programming Languages, 2019, DOI : 10.1145/3290357.
Martin Bodin, Tomás Diaz, and Éric Tanter, A Trustworthy Mechanized Formalization of R, Dynamic Languages Symposium, 2018, DOI: 10.1145/3276945.3276946.
Martin Bodin, Tomás Diaz, kaj Éric Tanter, A Trustworthy Mechanized Formalization of R, Dynamic Languages Symposium, 2018, DOI: 10.1145/3276945.3276946.
Martin Bodin, Tomás Diaz, et Éric Tanter, A Trustworthy Mechanized Formalization of R, Dynamic Languages Symposium, 2018, DOI : 10.1145/3276945.3276946.
Martin Bodin, Thomas Jensen, and Alan Schmitt, Certified Abstract Interpretation with Pretty-Big-Step Semantics, Certified Programs and Proofs, 2015, DOI: 10.1145/2676724.2693174.
Martin Bodin, Thomas Jensen, kaj Alan Schmitt, Certified Abstract Interpretation with Pretty-Big-Step Semantics, Certified Programs and Proofs, 2015, DOI: 10.1145/2676724.2693174.
Martin Bodin, Thomas Jensen, et Alan Schmitt, Certified Abstract Interpretation with Pretty-Big-Step Semantics, Certified Programs and Proofs, 2015, DOI : 10.1145/2676724.2693174.
Martin Bodin, Arthur Charguéraud, Daniele Filaretti, Philippa Gardner, Sergio Maffeis, Daiva Naudžiūnienė, Alan Schmitt, and Gareth Smith, A Trusted Mechanised JavaScript Specification, Symposium on Principles of Programming Languages, 2014, DOI: 10.1145/2578855.2535876.
Martin Bodin, Arthur Charguéraud, Daniele Filaretti, Philippa Gardner, Sergio Maffeis, Daiva Naudžiūnienė, Alan Schmitt, kaj Gareth Smith, A Trusted Mechanised JavaScript Specification, Symposium on Principles of Programming Languages, 2014, DOI: 10.1145/2578855.2535876.
Martin Bodin, Arthur Charguéraud, Daniele Filaretti, Philippa Gardner, Sergio Maffeis, Daiva Naudžiūnienė, Alan Schmitt, et Gareth Smith, A Trusted Mechanised JavaScript Specification, Symposium on Principles of Programming Languages, 2014, DOI : 10.1145/2578855.2535876.
Jörg Endrullis, Dimitri Hendriks, and Martin Bodin, Circular Coinduction in Coq Using Bisimulation-Up-To Techniques, Interactive Theorem Proving, 2013, DOI: 10.1007/978-3-642-39634-2_26.
Jörg Endrullis, Dimitri Hendriks, kaj Martin Bodin, Circular Coinduction in Coq Using Bisimulation-Up-To Techniques, Interactive Theorem Proving, 2013, DOI: 10.1007/978-3-642-39634-2_26.
Jörg Endrullis, Dimitri Hendriks, et Martin Bodin, Circular Coinduction in Coq Using Bisimulation-Up-To Techniques, Interactive Theorem Proving, 2013, DOI : 10.1007/978-3-642-39634-2_26.
David Monniaux and Martin Bodin, Modular Abstractions of Reactive Nodes using Disjunctive Invariants, Asian Symposium on Programming Languages and Systems, 2011, DOI: 10.1007/978-3-642-25318-8_5.
David Monniaux kaj Martin Bodin, Modular Abstractions of Reactive Nodes using Disjunctive Invariants, Asian Symposium on Programming Languages and Systems, 2011, DOI: 10.1007/978-3-642-25318-8_5.
David Monniaux et Martin Bodin, Modular Abstractions of Reactive Nodes using Disjunctive Invariants, Asian Symposium on Programming Languages and Systems, 2011, DOI : 10.1007/978-3-642-25318-8_5.
Emmanuel Beffara and Martin Bodin, Un jeu de plateau pour comprendre la dualité en logique, Adjectif : analyses et recherches sur les TICE, 2024.
Emmanuel Beffara kaj Martin Bodin, Un jeu de plateau pour comprendre la dualité en logique, Adjectif : analyses et recherches sur les TICE, 2024.
Emmanuel Beffara et Martin Bodin, Un jeu de plateau pour comprendre la dualité en logique, Adjectif : analyses et recherches sur les TICE, 2024.
Emmanuel Beffara, Martin Bodin, Nadine Mandran, and Rémi Molinier, Instrumentation de l’association de registres sémiotiques dans un assistant de preuve, Conférence sur les Environnements Informatiques pour l'Apprentissage Humain, 2023.
Emmanuel Beffara, Martin Bodin, Nadine Mandran, kaj Rémi Molinier, Instrumentation de l’association de registres sémiotiques dans un assistant de preuve, Conférence sur les Environnements Informatiques pour l'Apprentissage Humain, 2023.
Emmanuel Beffara, Martin Bodin, Nadine Mandran, et Rémi Molinier, Instrumentation de l’association de registres sémiotiques dans un assistant de preuve, Conférence sur les Environnements Informatiques pour l'Apprentissage Humain, 2023.
Jean Abou Samra, Martin Bodin, and Yannick Zakowski, Effectful Programming across Heterogeneous Computations — Work in Progress, Journées Francophones des Langages Applicatifs, 2023.
Jean Abou Samra, Martin Bodin, kaj Yannick Zakowski, Effectful Programming across Heterogeneous Computations — Work in Progress, Journées Francophones des Langages Applicatifs, 2023.
Jean Abou Samra, Martin Bodin, et Yannick Zakowski, Effectful Programming across Heterogeneous Computations — Work in Progress, Journées Francophones des Langages Applicatifs, 2023.
Martin Bodin, Les Assistants de preuve : l’exemple de Coq, Séminaire de l’IREM, 2022.
Martin Bodin, Les Assistants de preuve : l’exemple de Coq, Séminaire de l’IREM, 2022.
Martin Bodin, Les Assistants de preuve : l’exemple de Coq, Séminaire de l’IREM, 2022.
Martin Bodin, Philippa Gardner, Thomas Jensen, and Alan Schmitt, Poster: Skeletal Semantics, Verified Software Workshop, 2019.
Martin Bodin, Philippa Gardner, Thomas Jensen, kaj Alan Schmitt, Poster: Skeletal Semantics, Verified Software Workshop, 2019.
Martin Bodin, Philippa Gardner, Thomas Jensen, et Alan Schmitt, Poster: Skeletal Semantics, Verified Software Workshop, 2019.
Martin Bodin, Tomás Diaz, and Éric Tanter, A Trustworthy Mechanized Formalization of R, Formal Methods for Statistical Software, 2019.
Martin Bodin, Tomás Diaz, kaj Éric Tanter, A Trustworthy Mechanized Formalization of R, Formal Methods for Statistical Software, 2019.
Martin Bodin, Tomás Diaz, et Éric Tanter, A Trustworthy Mechanized Formalization of R, Formal Methods for Statistical Software, 2019.
Martin Bodin, A Coq Formalisation of a Core of R, CoqPL, 2018.
Martin Bodin, A Coq Formalisation of a Core of R, CoqPL, 2018.
Martin Bodin, A Coq Formalisation of a Core of R, CoqPL, 2018.
Martin Bodin, Thomas Jensen, and Alan Schmitt, An Abstract Separation Logic for Interlinked Extensible Records, Journées Francophones des Langages Applicatifs, 2016.
Martin Bodin, Thomas Jensen, kaj Alan Schmitt, An Abstract Separation Logic for Interlinked Extensible Records, Journées Francophones des Langages Applicatifs, 2016.
Martin Bodin, Thomas Jensen, et Alan Schmitt, An Abstract Separation Logic for Interlinked Extensible Records, Journées Francophones des Langages Applicatifs, 2016.
Martin Bodin, Thomas Jensen, and Alan Schmitt, Pretty-big-step-semantics-based Certified Abstract Interpretation, Journées Francophones des Langages Applicatifs, 2014.
Martin Bodin, Thomas Jensen, kaj Alan Schmitt, Pretty-big-step-semantics-based Certified Abstract Interpretation, Journées Francophones des Langages Applicatifs, 2014.
Martin Bodin, Thomas Jensen, et Alan Schmitt, Pretty-big-step-semantics-based Certified Abstract Interpretation, Journées Francophones des Langages Applicatifs, 2014.
Martin Bodin, Thomas Jensen, and Alan Schmitt, Pretty-big-step-semantics-based Certified Abstract Interpretation (Preliminary version), Festschrift for David Schmidt, 2013, DOI: 10.4204/EPTCS.129.23.
Martin Bodin, Thomas Jensen, kaj Alan Schmitt, Pretty-big-step-semantics-based Certified Abstract Interpretation (Preliminary version), Festschrift for David Schmidt, 2013, DOI: 10.4204/EPTCS.129.23.
Martin Bodin, Thomas Jensen, et Alan Schmitt, Pretty-big-step-semantics-based Certified Abstract Interpretation (Preliminary version), Festschrift for David Schmidt, 2013, DOI : 10.4204/EPTCS.129.23.
Martin Bodin and Alan Schmitt, A Certified JavaScript Interpreter, Journées Francophones des Langages Applicatifs, 2013.
Martin Bodin kaj Alan Schmitt, A Certified JavaScript Interpreter, Journées Francophones des Langages Applicatifs, 2013.
Martin Bodin et Alan Schmitt, A Certified JavaScript Interpreter, Journées Francophones des Langages Applicatifs, 2013.
I defended my PhD Thesis in 2016. My PhD advisors were Alan Schmitt and Thomas Jensen.
Mi doktoriĝis en 2016. Miaj doktoriĝestroj estis Alan Schmitt kaj Thomas Jensen.
J’ai soutenu en 2016. Mes encadrants étaient Alan Schmitt et Thomas Jensen.
Research situation within classes studied with IREM's group.
Situacio de esplorado en klasoj studita en la grupo de la IREM.
Situation de recherche en classe travaillée dans le groupe de l'IREM.
Talk to high school students.
Prelego al mezlernejaj studentoj.
Présentation pour des étudiants de lycée.
Talk to the students of the ENS Lyon.
Prelego al la studentoj de la ENS Lyon.
Présentation pour le séminaire sport-étude de l’ENS Lyon.
Talk at the Science group of TEJO.
Prelego por la Scienca grupo de TEJO.
Présentation pour le groupe Science de TEJO.
This is the document that I prepared for the French “qualification” for the CNRS.
Tio estas la dokumentaro kiun mi preparis por la franca “qualification”, por la CNRS.
Ceci est le dossier que j’ai monté pour la qualification aux postes d’enseignents-checheurs aux CNRS.
Small video in Esperanto to present my field of research.
Esperanta filmeto kiu prezentas mian esploradan temon.
Vidéo en espéranto sur une présentation générale de ma recherche.