Papers

• 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

This is a temporary 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.

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]