Keywords

Floating-point

  

Rounding

  

Formalization of mathematics

  

Formal proof

  

Coq

  

Program verification

More keywords

I created a word cloud using wordclouds from the titles of my publication:

Responsibilities

I translated as best as I could. I let the French version when useful.

• Deputy Scientific Head of Inria Saclay (Déléguée Scientifique Adjointe, DSA)
• member of the Scientific Council of CentraleSupélec
• elected chair of the ARITH working group of the GDR-IM (a CNRS subgroup of computer science)
• member of the (temporary) council of the Computer Science Graduate School of Université Paris-Saclay
• member of the CoDiReV Paris-Saclay (committee of the research heads of the Paris-Saclay components and partners)
• deputy member of the CFVU Paris-Saclay (commission de la formation et de la vie universitaire)
• member of the CDT commission of Inria Saclay (commission de développement technologique) for selecting engineering positions
• member of the partners commission for the Digicosme Labex (comité des tutelles du labex Digicosme)
• member of the program committee for selecting postdocs of the maths/computer science program of the Labex mathématique Hadamard
• member of the (national) Inria IES commission (commission pour l'information et l'édition scientifique) about scientific edition and publication models
• member of the Inria Saclay CLFP (commission locale de formation permanente)

I used to be (see also my popularization page):

• member of the STIC department commission of Université Paris-Sud (2019-2020)
• member of the executive commission for the Digicosme Labex (comité exécutif du labex Digicosme) (2019-2020)
• member of the committee for the Gilles Kahn PhD award of the French Computer Science Society (2015-2017)
• member of the Inria evaluation committee (2011-2014)

Program Committees

• IEEE Symposium on Computer Arithmetic (ARITH): ARITH 2020 (no number anymore), ARITH-26 (2019, PC chair), ARITH-25 (2018), ARITH-24 (2017), ARITH-23 (2016), ARITH-22 (2015)
• Certified Programs and Proofs (CPP): CPP 2018, CPP 2017
• NASA Formal Methods (NFM): NFM 2019, NFM 2018
• Interactive Theorem Proving (ITP): ITP 2017
• Numerical Software Verification (NSV): NSV 2020, NSV 2017 (PC chair), NSV 2016, NSV 2015, NSV 2014, NSV 2011
• Workshop on High-Consequence Control Verification (HCCV), HCCV 2016
• "Journées Francophones des Langages Applicatifs" (JFLA): JFLA 2018 (general and PC chair), JFLA 2017 (PC and vice-president), JFLA 2016, JFLA 2015, JFLA 2011
• Coq workshop: Coq-2020, 7th Coq workshop (2015)

PhD students

• Diane Gallois-Wong, 2017-, co-advisor: Thibault Hilaire
• Florian Faissole, 2016-2019, co-advisor: Alexandre Chapoutot, now Researcher at Mitsubishi Electric
• Catherine Lelay, 2011-2015, co-advisor: Guillaume Melquiond, now mathematics teacher
• Tuyen Nguyen, 2009-2012, advisor: Claude Marché, now Lecturer at HCMC University Of Science

Award

I got the Best Talk Award at the Numerical Sotware Verification 2016 conference for my talk about Computing a correct and tight rounding error bound using rounding-to-nearest.

Funded projects

• EMC2, ERC Synergy project about Extreme-scale Mathematically-based Computational Chemistry, 2019-2025, member
• MILC, DIM-RFSI project about Lebesgue integration in Coq, 2018-2020, member
• ELEFFAN, DigiCosme project, rounding errors of numerical schemes, 2016-2019, PI
• ELFIC DigiCosme working group, certification about the finite element method, 2014-2016, PI
• FastRelax ANR project, fast and reliable approximation algorithms, 2014-2018, site leader
• Coquelicot Digiteo project, new Coq library for reals, 2011-2014, PI
• Verasco ANR project, verified static analyzers and compilers, 2011-2015
• FOST ANR project, formal proofs about scientific computations, 2009-2012, PI
• HISSEO Digiteo project, handling compiler discrepancies when verifying floating-point programs, 2008-2012
• CERPAN ANR project, certification of applied mathematics programs, 2005-2008, site leader