-
Notifications
You must be signed in to change notification settings - Fork 0
/
research.html
115 lines (96 loc) · 7.45 KB
/
research.html
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
<!--
0. Do whatever you want with this file.
-->
<html>
<head>
<meta charset="utf-8"/>
<title>Research - Damien Rouhling</title>
<link href="static/style.css" type="text/css" rel="stylesheet"/>
</head>
<body>
<header>
<div id="logo">
<h1>Damien Rouhling</h1>
</div>
<nav>
<div id="bar"><ul><li><a href="index.html">Home</a></li><li class="current"><a href="research.html">Research</a></li><li><a href="teaching.html">Teaching</a></li></ul></div>
</nav>
</header>
<section>
<h1 id="Papers">Papers</h1>
<ul><li><p><strong>Competing inheritance paths in dependent type theory: a case study in
functional analysis</strong>, R. Affeldt, C. Cohen, M. Kerjean, A. Mahboubi,
D. Rouhling, K. Sakaguchi.<br/> In the proceedings of <a href='https://ijcar2020.org/'>IJCAR 2020</a>.<br/> [<a href='https://hal.inria.fr/hal-02463336v2/bibtex'>bib</a> | <a href='data/papers/IJCAR2020.pdf'>pdf</a>]</p>
</li><li><p><strong>Formalization Techniques for Asymptotic Reasoning in Classical Analysis</strong>,
R. Affeldt, C. Cohen and D. Rouhling.<br/> In <a href='https://jfr.unibo.it/index'>Journal of Formalized Reasoning 2018</a>.<br/> [<a href='https://hal.inria.fr/hal-01719918v3/bibtex'>bib</a> | <a href='data/papers/JFR2018.pdf'>pdf</a>]</p>
</li><li><p><strong>A Formal Proof in Coq of a Control Function for the Inverted Pendulum</strong>,
D. Rouhling.<br/> In the proceedings of <a href='https://popl18.sigplan.org/track/CPP-2018'>CPP 2018</a>.<br/> [<a href='https://hal.inria.fr/hal-01639819v2/bibtex'>bib</a> | <a href='data/papers/CPP2018.pdf'>pdf</a>]</p>
</li><li><p><strong>A Formal Proof in Coq of LaSalle's Invariance Principle</strong>, C. Cohen and
D. Rouhling.<br/> In the proceedings of <a href='http://itp2017.cic.unb.br/'>ITP 2017</a>.<br/> [<a href='https://hal.inria.fr/hal-01612293v1/bibtex'>bib</a> | <a href='data/papers/ITP2017.pdf'>pdf</a>]</p>
</li><li><p><strong>A refinement-based approach to large scale reflection for algebra</strong>,
C. Cohen and D. Rouhling.<br/> In the proceedings of <a href='http://jfla.inria.fr/2017/'>JFLA 2017</a>.<br/> [<a href='https://hal.archives-ouvertes.fr/hal-01414881v1/bibtex'>bib</a> | <a href='data/papers/JFLA2017.pdf'>pdf</a>]</p>
</li><li><p><strong>Axiomatic constraint systems for proof search modulo theories</strong>,
D. Rouhling, M. Farooque, S. Graham-Lengrand, A. Mahboubi and J.-M. Notin.<br/> In the proceedings of <a href='http://frocos2015.ii.uni.wroc.pl/'>FroCoS 2015</a>.<br/> [<a href='https://hal-ens-lyon.archives-ouvertes.fr/hal-01107944v1/bibtex'>bib</a> | <a href='data/papers/FroCoS2015.pdf'>pdf</a>]</p>
</li></ul>
<h1 id="Talk-proposals">Talk proposals</h1>
<ul><li><strong>Classical Analysis with Coq</strong>, R. Affeldt, C. Cohen, A. Mahboubi,
D. Rouhling and P.-Y. Strub.<br/> <a href='http://coqworkshop2018.inria.fr/'>The Coq Workshop 2018</a>.<br/> [<a href='data/proposals/CoqWS2018.pdf'>pdf</a>]</li></ul>
<h1 id="Talks">Talks</h1>
<ul><li><p><strong>Asymptotic Reasoning in Coq</strong>, at the <a href='http://gallium.inria.fr/seminar.html'>Gallium
seminar</a>.<br/> [<a href='data/talks/Gallium.pdf'>slides</a>]</p>
</li><li><p><strong>Formal Proofs for Control Theory and Robotics: A Case Study</strong>, at the
<a href='http://fastrelax.gforge.inria.fr/Sophia2018.html'>journées FastRelax 2018</a>.<br/> [<a href='data/talks/FastRelax2018.pdf'>slides</a>]</p>
</li><li><p><strong>A Stability Proof for the Inverted Pendulum</strong>, at <a href='https://popl18.sigplan.org/track/CPP-2018'>CPP
2018</a>.<br/> [<a href='data/talks/CPP2018.pdf'>slides</a>]</p>
</li><li><p><strong>A formal proof in Coq of LaSalle's invariance principle</strong>, at <a href='http://itp2017.cic.unb.br/'>ITP
2017</a>.<br/> [<a href='data/talks/ITP2017.pdf'>slides</a>]</p>
</li><li><p><strong>A formal proof in Coq of LaSalle's invariance principle</strong>, at the <a href='http://fastrelax.gforge.inria.fr/Paris2017.html'>journées
FastRelax 2017</a>.<br/> [<a href='data/talks/FastRelax2017.pdf'>slides</a>]</p>
</li><li><p><strong>Refinement: a reflection on proofs and computations</strong>, at the <a href='https://specfun.inria.fr/seminar/'>SpecFun
seminar</a>.<br/> [<a href='data/talks/SpecFun.pdf'>slides</a>]</p>
</li><li><p><strong>Refining the ring tactic</strong>, at <a href='http://jfla.inria.fr/2017/'>JFLA 2017</a>.<br/> [<a href='data/talks/JFLA2017.pdf'>slides</a>]</p>
</li><li><p><strong>Constraint systems for proof-search modulo a theory</strong>, at the <a href='https://lama.univ-savoie.fr/~hirschowitz/LAC2014'>journées LAC
2014</a>.<br/> [<a href='data/talks/LAC2014.pdf'>slides</a>]</p>
</li><li><p><strong>Delayed instantiation of existential variables in presence of a theory</strong>, at
the <a href='http://www.lix.polytechnique.fr/~lengrand/Events/PSATTT13'>PSATTT 2013</a>
workshop.<br/> [<a href='data/talks/PSATTT2013.pdf'>slides</a>]</p>
</li></ul>
<h1 id="PhD-Thesis">PhD Thesis</h1>
<h3 id="Thesis">Thesis</h3>
<p>Here is the final version.<br/>[<a href='data/phd/thesis.pdf'>manuscript</a>]</p>
<h3 id="Source-code">Source code</h3>
<p>The source code is spread across three repositories:
<a href='https://github.com/CoqEAL/CoqEAL'>CoqEAL</a>,
<a href='https://github.com/drouhling/LaSalle'>LaSalle</a> and
<a href='https://github.com/math-comp/analysis'>mathcomp-analysis</a>.</p>
<p>A snapshot of the code presented in the manuscript is
<a href='data/phd/sources.tar.gz'>here</a>.</p>
<h3 id="Defense">Defense</h3>
<p>I defended my thesis on September 30, 2019.</p>
<p>Jury:</p>
<ul><li><p><strong>Advisors</strong>: Yves Bertot and Cyril Cohen.</p>
</li><li><p><strong>Rapporteurs</strong>: Sylvie Boldo and Lawrence Paulson.</p>
</li><li><p><strong>Examiners</strong>: Jesús Aransay, Éric Goubault and Étienne Lozes.</p>
</li></ul>
<p>Here is my presentation.<br/>[<a href='data/phd/defence.pdf'>slides</a>]</p>
<h1 id="Internships">Internships</h1>
<ul><li><p><strong>January - June 2016</strong>: M2 internship.<br/> <em>Automatic refinements in Coq</em>.<br/> At <a href='https://www.inria.fr/en/centre-inria-sophia-antipolis-mediterranee'>Inria Sophia Antipolis -
Méditerranée</a>,
in the <a href='https://team.inria.fr/marelle/en/'>MARELLE</a> team, under the
supervision of Cyril Cohen.<br/> [<a href='data/internships/M2Report.pdf'>report</a> | <a href='data/internships/M2Slides.pdf'>slides</a>]</p>
</li><li><p><strong>Summer 2014</strong>: M1 internship.<br/> <em>Dependently typed lambda calculus with a lifting operator</em>.<br/> At the <a href='http://www.chalmers.se/cse/EN'>computer science and engineering
department</a> of <a href='http://www.chalmers.se/EN'>Chalmers University of
Technology</a>, in Gothenburg, Sweden, under the
supervision of Thierry Coquand.<br/> [<a href='data/internships/M1Report.pdf'>report</a> | <a href='data/internships/M1Slides.pdf'>(french) slides</a>]</p>
</li><li><p><strong>Summer 2013</strong>: L3 internship.<br/> <em>Congruence closure and proof-search modulo a theory</em>.
At the <a href='http://www.lix.polytechnique.fr/en/'>LIX laboratory</a>, in the <a href='http://www.lix.polytechnique.fr/~lengrand/PSI/'>PSI
project</a>, under the
supervision of Stéphane Graham-Lengrand and Assia Mahboubi.<br/> [<a href='data/internships/L3Report.pdf'>(french) report</a> | <a href='data/internships/L3Slides.pdf'>(french) slides</a>]</p>
</li></ul>
</section>
<footer>
<a href="http://dev.isomorphis.me/stone">Stone λ-powered</a>
<p>Last modified: 2021/07/13</p>
</footer>
</body>
</html>