IRIT - UMR 5505

Français
UPS
  Bandeau IRIT
 
Photo EMD

Erik Martin-Dorel

Status:  Maître de Conférences (Associate Professor)
Team:  Assistance à la Certification des Applications DIstribuées et Embarquées (ACADIE)
E-mail:  erikREMOVETHIS.martin-dorel@REMOVETHATirit.fr
Localization:  UPS / IRIT2 / Level 4, Office: 473
Phone:  +33 (0)5 61 55 6416
Publications:  Publis

 

Research

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;
  • algorithmic game theory.

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.

 

Top

 

Teaching

Since Septembre 2014, I hold lectures and practical sessions in Computer Science for the FSI at UPS, for both undergraduate and master's degrees.

More precisely, I have been involved in the following teaching units (in reverse chronological order):

 

Top