**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]

**Classical Analysis with Coq**, R. Affeldt, C. Cohen, A. Mahboubi, D. Rouhling and P.-Y. Strub.

The Coq Workshop 2018.

[pdf]

**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]**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]

Here is the final version.

[manuscript]

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

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

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]

**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]