![]() |
![]() |
![]() |
|||||||
![]() |
![]() |
![]() |
|||||||
![]() |
![]() |
![]() |
|||||||
![]() |
![]() |
![]() ![]() |
![]() |
||||||
![]() |
![]() |
![]() |
![]() |
||||||
![]() |
![]() Erik Martin-DorelPosition:
Maître de Conférences (Associate Professor)
Department:
E-mail:
erik
Localization:
UPS / IRIT2 / Level 4, Office: 473
Phone:
+33 (0)5 61 55 6416
ResearchResearch TopicsThe following keywords recap my main research interests:
Current Research ActivitiesMy research activities focus on the applications of interactive formal proof, in particular for the formal verification of results in computer arithmetic and game theory. I am also interested in designing methods to increase proof automation within formal proof assistants, as well as automating tests in general and specifically around the tooling of projects in the OCaml and Coq community. Research ExperienceSince the 1st September 2014, I am Associate Professor (Maître de Conférences) at the Université Toulouse III – Paul Sabatier and I do my research in the ACADIE team of the IRIT research lab. Previously, I was a postdoc in the VALS/Toccata team of LRI (UMR 8623 CNRS & Université Paris-Sud) at Inria Saclay - Île-de-France and was involved in the VERASCO project of the French ANR. Before that, I was a postdoc in the Marelle project-team at Inria Sophia Antipolis, and was involved in the TaMaDi project of the French ANR. I defended my PhD thesis on the 26th September 2012 in ENS de Lyon, where I worked in the AriC project-team (formerly known as Arénaire) of the LIP research laboratory, under the joint supervision of Jean-Michel Muller and Micaela Mayero. My PhD manuscript and my PhD defense slides are available online. Selected TalksCertified, Efficient and Sharp Univariate Taylor Models in COQ at SYNASC 2013. Formal proofs and certified computation in Coq at Games 2015. Proving Tight Bounds on Univariate Expressions with Elementary Functions in Coq at FAC 2016. A Reflexive Tactic for Polynomial Positivity using Numerical Solvers and Floating-Point Computations at CPP 2017. An Existence Theorem of Nash Equilibrium in Coq and Isabelle at GandALF 2017 (code). The under tactic (math-comp meeting, 2019-02-28) SSReflect in Coq 8.10 at the Coq Workshop 2019 (Demo) Primitive Floats in Coq at ITP 2019 Overview of the recent and upcoming features of Learn-OCaml (Learn-OCaml WG, 2022-03-23) Learn-OCaml: How to contribute? (Learn-OCaml WG, 2022-03-23) Overview of the PFITAXEL project Using the Learn-OCaml platform (DAS e-education@IRIT, 2022-05-20) Learn-OCaml Presentation (in French) at the 1st Meetup Toulouse OCaml UserS (2022-10-11) Hardware floating-point computations in Coq at Certified and Symbolic-Numeric Computation (ENS de Lyon, 2023-05-26) Internship proposals (2022-2023)
If you are strongly interested in one of the research topics that I mention, but no internship proposal about it appears at the time, feel free to contact me and send me a CV+cover-letter, to discuss a possible internship supervised by me within the ACADIE team.
Teaching
More precisely, I have been involved in the following teaching units (in reverse chronological order):
|
![]() |
|||||||
![]() |
![]() |
![]() |
|||||||
![]() |
![]() |
![]() |
![]() |