IRIT - UMR 5505

Français
UPS
  Bandeau IRIT
 
Photo EMD

Erik Martin-Dorel

Position: 
Maître de Conférences (Associate Professor)
Laboratory: 
Informatics Research Institute of Toulouse (IRIT)
Department: 
Reliability of Systems and Software (RSS)
Team: 
Assistance to the Certification of Distributed and Embedded Applications (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;
  • game theory: formal proof for game theory: formalization of Boolean games, determinacy, games in normal form...
  • software engineering : CI/CD, automating tests, V&V or continuous deployment...

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, as well as automating tests in general and specifically around the tooling of projects in the OCaml and Coq community.

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

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)

(filled)

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.

 

Top

 

Teaching

UPS
Département Info
 Since Septembre 2014, I hold lectures and practical sessions for the Computer Science Department of the FSI at UPS, for both undergraduate and master's degrees.
Master DL In particular, I belong to the steering committee of the Master DL for which I do most of my teaching activities.

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

 

Top