Papers

• Competing inheritance paths in dependent type theory: a case study in functional analysis, R. Affeldt, C. Cohen, M. Kerjean, A. Mahboubi, D. Rouhling, K. Sakaguchi.
  In the proceedings of IJCAR 2020.
  [bib | pdf]

• Formalization Techniques for Asymptotic Reasoning in Classical Analysis, R. Affeldt, C. Cohen and D. Rouhling.
  In Journal of Formalized Reasoning 2018.
  [bib | pdf]

• A Formal Proof in Coq of a Control Function for the Inverted Pendulum, D. Rouhling.
  In the proceedings of CPP 2018.
  [bib | pdf]

• A Formal Proof in Coq of LaSalle's Invariance Principle, C. Cohen and D. Rouhling.
  In the proceedings of ITP 2017.
  [bib | pdf]

• A refinement-based approach to large scale reflection for algebra, C. Cohen and D. Rouhling.
  In the proceedings of JFLA 2017.
  [bib | pdf]

• Axiomatic constraint systems for proof search modulo theories, D. Rouhling, M. Farooque, S. Graham-Lengrand, A. Mahboubi and J.-M. Notin.
  In the proceedings of FroCoS 2015.
  [bib | pdf]

Talk proposals

• Classical Analysis with Coq, R. Affeldt, C. Cohen, A. Mahboubi, D. Rouhling and P.-Y. Strub.
  The Coq Workshop 2018.
  [pdf]

Talks

• Asymptotic Reasoning in Coq, at the Gallium seminar.
  [slides]

• Formal Proofs for Control Theory and Robotics: A Case Study, at the journées FastRelax 2018.
  [slides]

• A Stability Proof for the Inverted Pendulum, at CPP 2018.
  [slides]

• A formal proof in Coq of LaSalle's invariance principle, at ITP 2017.
  [slides]

• A formal proof in Coq of LaSalle's invariance principle, at the journées FastRelax 2017.
  [slides]

• Refinement: a reflection on proofs and computations, at the SpecFun seminar.
  [slides]

• Refining the ring tactic, at JFLA 2017.
  [slides]

• Constraint systems for proof-search modulo a theory, at the journées LAC 2014.
  [slides]

• Delayed instantiation of existential variables in presence of a theory, at the PSATTT 2013 workshop.
  [slides]

PhD Thesis

Thesis

Here is the final version.
[manuscript]

Source code

The source code is spread across three repositories: CoqEAL, LaSalle and mathcomp-analysis.

A snapshot of the code presented in the manuscript is here.

Defense

I defended my thesis on September 30, 2019.

Jury:

• Advisors: Yves Bertot and Cyril Cohen.

• Rapporteurs: Sylvie Boldo and Lawrence Paulson.

• Examiners: Jesús Aransay, Éric Goubault and Étienne Lozes.

Here is my presentation.
[slides]

Internships

• January - June 2016: M2 internship.
  Automatic refinements in Coq.
  At Inria Sophia Antipolis - Méditerranée, in the MARELLE team, under the supervision of Cyril Cohen.
  [report | slides]

• Summer 2014: M1 internship.
  Dependently typed lambda calculus with a lifting operator.
  At the computer science and engineering department of Chalmers University of Technology, in Gothenburg, Sweden, under the supervision of Thierry Coquand.
  [report | (french) slides]

• Summer 2013: L3 internship.
  Congruence closure and proof-search modulo a theory. At the LIX laboratory, in the PSI project, under the supervision of Stéphane Graham-Lengrand and Assia Mahboubi.
  [(french) report | (french) slides]