IRIT - UMR 5505

  Bandeau IRIT
Photo EMD

Erik Martin-Dorel

Maître de Conférences (Associate Professor)
UPS / IRIT2 / Level 4, Office: 473
+33 (0)5 61 55 6416



Research Topics

The following keywords recap my main research interests:

  • formal methods: formal proof assistants (Coq, SSReflect, PVS), formalization of mathematics, type theory, proof theory, classical and intuitionnistic logics, formal specifications, formal verification, certificates;
  • numerical methods: computer arithmetic, floating-point arithmetic, correct rounding, certified polynomial approximation, interval arithmetic, global optimization, computer algebra;
  • game theory: formal proof for game theory: formalization of Boolean games, determinacy, games in normal form...

Current Research Activities

My 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.

Research Experience

Since 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 Talks

Certified, 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

Internship proposals (2020-2021)