After 16 years of experience since my Master's degree in Math and Computer Science (working on formal verification and floating-point arithmetic during 5 years, then teaching Software Engineering at the University of Toulouse during 11 years), I'd like to apply my expertise within the software industry. The values of continuous improvement and knowledge sharing are dear to me, and I'm active in the open source community in my spare time; the main projects where I'm involved are pinned on my GitHub profile: https://github.com/erikmd ; I also enjoy working in a team. To date, I had the pleasure to mentor 28 interns in research/development projects, and co-supervise a PhD thesis combining Rocq proofs and decision theory.
I am particularly interested in three kinds of roles: tech lead, DevOps engineer, or product owner in an agile context.
Co-maintainer (with Louis GESBERT and Yann RÉGIS-GIANAS) of the Learn-OCaml platform, a full-stack web application written in OCaml, developed by the OCaml Foundation, and distributed under the MIT license. This platform aims to help learning functional programming in OCaml, with tests dedicated to formative or summative assessments. I have supervised several interns working on the project (6 ⋅ Bachelor, 9 ⋅Master 1, 1 ⋅ Master 2).
I coordinate the distribution of official Docker images of the Rocq Prover (formerly known as the Coq Proof Assistant), developed by Inria and distributed under the LGPL-2.1 license. To this end, I co-maintain the GitHub Action named docker-coq-action, used by 496 GitHub repositories (as of June 2025) and distributed under the MIT license. I also develop the docker-keeper tool, a compiler written in Python 3 that generates GitLab CI children pipelines from a user-friendly DSL. It is also distributed under the MIT license.
Teacher in the Bachelor's degree of Computer Science, and the Master's degree of Computer Science, especially for the Software Engineering curriculum (Master SDL).
Researcher in formal methods for V&V. My publications are available in the HAL open archive. Since 2017, I have supervised 28 internships (11 ⋅ Bachelor, 12 ⋅ Master 1, 5 ⋅ Master 2) on research and/or development topics. From 2017 to 2020, I was the project holder of the FAGames research project funded by the LabEx CIMI (gathering 3 project members, plus interns and invited members). From 2020 to 2023, I co-supervised a PhD student. In 2024 and 2025, I served in the section 27 of the CNU.
During this postdoctoral fellowship, funded by the ANR project Verasco and supervised by Guillaume MELQUIOND, I worked on extending and integrating our implementation of Taylor models in the CoqInterval formal proof library. This Rocq library gathers several proof tactics to automatically and formally prove bounds on real-valued expressions, relying on interval arithmetic.
During this postdoctoral fellowship, funded by the ANR project TaMaDi and supervised by Laurent THÉRY and Laurence RIDEAU, I worked on the formal proof (in Rocq) of an implementation of so-called Taylor models, in a context related to floating-point arithmetic.
During my thesis "Contributions to the Formal Verification of Arithmetic
Algorithms", I designed a certifying algorithm to accelerate the formal
verification of worst-cases for correctly rounding elementary functions, and I contributed to the implementation of two formal proof libraries (using the Rocq Prover, formerly known as the Coq Proof Assistant). I worked under the joint supervision of Jean-Michel MULLER and Micaela MAYERO, in collaboration with six other researchers from ENS Lyon and Inria.
- Français
- Anglais
- Allemand