math-comp.github.io/papers.html at master · math-comp/math-comp.github.io · GitHub

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
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
687
688
689
690
691
692
693
694
695
696
697
698
699
700
701
702
703
704
705
706
707
708
709
710
711
712
713
714
715
716
717
718
719
720
721
722
723
724
725
726
727
728
729
730
731
732
733
734
735
736
737
738
739
740
741
742
743
744
745
746
747
748
749
750
751
752
753
754
755
756
757
758
759
760
761
762
763
764
765
766
767
768
769
770
771
772
773
774
775
776
777
778
779
780
781
782
783
784
785
786
787
788
789
790
791
792
793
794
795
796
797
798
799
800
801
802
803
804
805
806
807
808
809
810
811
812
813
814
815
816
817
818
819
820
821
822
823
824
825
826
827
828
829
<?xml version="1.0" encoding="utf-8"?>
<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Strict//EN"
"http://www.w3.org/TR/xhtml1/DTD/xhtml1-strict.dtd">
<html xmlns="http://www.w3.org/1999/xhtml" lang="en" xml:lang="en">
<head>
<!-- 2026-09-22 mar. 12:50 -->
<meta http-equiv="Content-Type" content="text/html;charset=utf-8" />
<meta name="viewport" content="width=device-width, initial-scale=1" />
<title>Mathematical Components: Research Papers</title>
<meta name="generator" content="Org mode" />
<meta name="author" content="Marie" />
<style type="text/css">
 <!--/*--><![CDATA[/*><!--*/
  .title  { text-align: center;
             margin-bottom: .2em; }
  .subtitle { text-align: center;
              font-size: medium;
              font-weight: bold;
              margin-top:0; }
  .todo   { font-family: monospace; color: red; }
  .done   { font-family: monospace; color: green; }
  .priority { font-family: monospace; color: orange; }
  .tag    { background-color: #eee; font-family: monospace;
            padding: 2px; font-size: 80%; font-weight: normal; }
  .timestamp { color: #bebebe; }
  .timestamp-kwd { color: #5f9ea0; }
  .org-right  { margin-left: auto; margin-right: 0px;  text-align: right; }
  .org-left   { margin-left: 0px;  margin-right: auto; text-align: left; }
  .org-center { margin-left: auto; margin-right: auto; text-align: center; }
  .underline { text-decoration: underline; }
  #postamble p, #preamble p { font-size: 90%; margin: .2em; }
  p.verse { margin-left: 3%; }
  pre {
    border: 1px solid #ccc;
    box-shadow: 3px 3px 3px #eee;
    padding: 8pt;
    font-family: monospace;
    overflow: auto;
    margin: 1.2em;
  }
  pre.src {
    position: relative;
    overflow: visible;
    padding-top: 1.2em;
  }
  pre.src:before {
    display: none;
    position: absolute;
    background-color: white;
    top: -10px;
    right: 10px;
    padding: 3px;
    border: 1px solid black;
  }
  pre.src:hover:before { display: inline;}
  /* Languages per Org manual */
  pre.src-asymptote:before { content: 'Asymptote'; }
  pre.src-awk:before { content: 'Awk'; }
  pre.src-C:before { content: 'C'; }
  /* pre.src-C++ doesn't work in CSS */
  pre.src-clojure:before { content: 'Clojure'; }
  pre.src-css:before { content: 'CSS'; }
  pre.src-D:before { content: 'D'; }
  pre.src-ditaa:before { content: 'ditaa'; }
  pre.src-dot:before { content: 'Graphviz'; }
  pre.src-calc:before { content: 'Emacs Calc'; }
  pre.src-emacs-lisp:before { content: 'Emacs Lisp'; }
  pre.src-fortran:before { content: 'Fortran'; }
  pre.src-gnuplot:before { content: 'gnuplot'; }
  pre.src-haskell:before { content: 'Haskell'; }
  pre.src-hledger:before { content: 'hledger'; }
  pre.src-java:before { content: 'Java'; }
  pre.src-js:before { content: 'Javascript'; }
  pre.src-latex:before { content: 'LaTeX'; }
  pre.src-ledger:before { content: 'Ledger'; }
  pre.src-lisp:before { content: 'Lisp'; }
  pre.src-lilypond:before { content: 'Lilypond'; }
  pre.src-lua:before { content: 'Lua'; }
  pre.src-matlab:before { content: 'MATLAB'; }
  pre.src-mscgen:before { content: 'Mscgen'; }
  pre.src-ocaml:before { content: 'Objective Caml'; }
  pre.src-octave:before { content: 'Octave'; }
  pre.src-org:before { content: 'Org mode'; }
  pre.src-oz:before { content: 'OZ'; }
  pre.src-plantuml:before { content: 'Plantuml'; }
  pre.src-processing:before { content: 'Processing.js'; }
  pre.src-python:before { content: 'Python'; }
  pre.src-R:before { content: 'R'; }
  pre.src-ruby:before { content: 'Ruby'; }
  pre.src-sass:before { content: 'Sass'; }
  pre.src-scheme:before { content: 'Scheme'; }
  pre.src-screen:before { content: 'Gnu Screen'; }
  pre.src-sed:before { content: 'Sed'; }
  pre.src-sh:before { content: 'shell'; }
  pre.src-sql:before { content: 'SQL'; }
  pre.src-sqlite:before { content: 'SQLite'; }
  /* additional languages in org.el's org-babel-load-languages alist */
  pre.src-forth:before { content: 'Forth'; }
  pre.src-io:before { content: 'IO'; }
  pre.src-J:before { content: 'J'; }
  pre.src-makefile:before { content: 'Makefile'; }
  pre.src-maxima:before { content: 'Maxima'; }
  pre.src-perl:before { content: 'Perl'; }
  pre.src-picolisp:before { content: 'Pico Lisp'; }
  pre.src-scala:before { content: 'Scala'; }
  pre.src-shell:before { content: 'Shell Script'; }
  pre.src-ebnf2ps:before { content: 'ebfn2ps'; }
  /* additional language identifiers per "defun org-babel-execute"
       in ob-*.el */
  pre.src-cpp:before  { content: 'C++'; }
  pre.src-abc:before  { content: 'ABC'; }
  pre.src-coq:before  { content: 'Coq'; }
  pre.src-groovy:before  { content: 'Groovy'; }
  /* additional language identifiers from org-babel-shell-names in
     ob-shell.el: ob-shell is the only babel language using a lambda to put
     the execution function name together. */
  pre.src-bash:before  { content: 'bash'; }
  pre.src-csh:before  { content: 'csh'; }
  pre.src-ash:before  { content: 'ash'; }
  pre.src-dash:before  { content: 'dash'; }
  pre.src-ksh:before  { content: 'ksh'; }
  pre.src-mksh:before  { content: 'mksh'; }
  pre.src-posh:before  { content: 'posh'; }
  /* Additional Emacs modes also supported by the LaTeX listings package */
  pre.src-ada:before { content: 'Ada'; }
  pre.src-asm:before { content: 'Assembler'; }
  pre.src-caml:before { content: 'Caml'; }
  pre.src-delphi:before { content: 'Delphi'; }
  pre.src-html:before { content: 'HTML'; }
  pre.src-idl:before { content: 'IDL'; }
  pre.src-mercury:before { content: 'Mercury'; }
  pre.src-metapost:before { content: 'MetaPost'; }
  pre.src-modula-2:before { content: 'Modula-2'; }
  pre.src-pascal:before { content: 'Pascal'; }
  pre.src-ps:before { content: 'PostScript'; }
  pre.src-prolog:before { content: 'Prolog'; }
  pre.src-simula:before { content: 'Simula'; }
  pre.src-tcl:before { content: 'tcl'; }
  pre.src-tex:before { content: 'TeX'; }
  pre.src-plain-tex:before { content: 'Plain TeX'; }
  pre.src-verilog:before { content: 'Verilog'; }
  pre.src-vhdl:before { content: 'VHDL'; }
  pre.src-xml:before { content: 'XML'; }
  pre.src-nxml:before { content: 'XML'; }
  /* add a generic configuration mode; LaTeX export needs an additional
     (add-to-list 'org-latex-listings-langs '(conf " ")) in .emacs */
  pre.src-conf:before { content: 'Configuration File'; }

  table { border-collapse:collapse; }
  caption.t-above { caption-side: top; }
  caption.t-bottom { caption-side: bottom; }
  td, th { vertical-align:top;  }
  th.org-right  { text-align: center;  }
  th.org-left   { text-align: center;   }
  th.org-center { text-align: center; }
  td.org-right  { text-align: right;  }
  td.org-left   { text-align: left;   }
  td.org-center { text-align: center; }
  dt { font-weight: bold; }
  .footpara { display: inline; }
  .footdef  { margin-bottom: 1em; }
  .figure { padding: 1em; }
  .figure p { text-align: center; }
  .equation-container {
    display: table;
    text-align: center;
    width: 100%;
  }
  .equation {
    vertical-align: middle;
  }
  .equation-label {
    display: table-cell;
    text-align: right;
    vertical-align: middle;
  }
  .inlinetask {
    padding: 10px;
    border: 2px solid gray;
    margin: 10px;
    background: #ffffcc;
  }
  #org-div-home-and-up
   { text-align: right; font-size: 70%; white-space: nowrap; }
  textarea { overflow-x: auto; }
  .linenr { font-size: smaller }
  .code-highlighted { background-color: #ffff00; }
  .org-info-js_info-navigation { border-style: none; }
  #org-info-js_console-label
    { font-size: 10px; font-weight: bold; white-space: nowrap; }
  .org-info-js_search-highlight
    { background-color: #ffff00; color: #000000; font-weight: bold; }
  .org-svg { width: 90%; }
  /*]]>*/-->
</style>
<meta http-equiv="Content-Type" content="text/html; charset=utf-8">
<style type="text/css"> body {font-family: Arial, Helvetica; margin-left: 5em; font-size: large;} </style>
<style type="text/css"> h1 {margin-left: 0em; padding: 0px; text-align: center} </style>
<style type="text/css"> h2 {margin-left: 0em; padding: 0px; color: #580909} </style>
<style type="text/css"> h3 {margin-left: 1em; padding: 0px; color: #C05001;} </style>
<style type="text/css"> body { max-width: 1100px; width: 100% - 30px; margin-left: 30px}</style>
<script type="text/javascript">
/*
@licstart  The following is the entire license notice for the
JavaScript code in this tag.

Copyright (C) 2012-2020 Free Software Foundation, Inc.

The JavaScript code in this tag is free software: you can
redistribute it and/or modify it under the terms of the GNU
General Public License (GNU GPL) as published by the Free Software
Foundation, either version 3 of the License, or (at your option)
any later version.  The code is distributed WITHOUT ANY WARRANTY;
without even the implied warranty of MERCHANTABILITY or FITNESS
FOR A PARTICULAR PURPOSE.  See the GNU GPL for more details.

As additional permission under GNU GPL version 3 section 7, you
may distribute non-source (e.g., minimized or compacted) forms of
that code without the copy of the GNU GPL normally required by
section 4, provided you include this license notice and a URL
through which recipients can access the Corresponding Source.


@licend  The above is the entire license notice
for the JavaScript code in this tag.
*/
<!--/*--><![CDATA[/*><!--*/
 function CodeHighlightOn(elem, id)
 {
   var target = document.getElementById(id);
   if(null != target) {
     elem.cacheClassElem = elem.className;
     elem.cacheClassTarget = target.className;
     target.className = "code-highlighted";
     elem.className   = "code-highlighted";
   }
 }
 function CodeHighlightOff(elem, id)
 {
   var target = document.getElementById(id);
   if(elem.cacheClassElem)
     elem.className = elem.cacheClassElem;
   if(elem.cacheClassTarget)
     target.className = elem.cacheClassTarget;
 }
/*]]>*///-->
</script>
</head>
<body>
<div id="content">
<h1 class="title">Mathematical Components: Research Papers</h1>
<div id="table-of-contents">
<h2>Table of Contents</h2>
<div id="text-table-of-contents">
<ul>
<li><a href="#org87c5133">Mathematics</a></li>
<li><a href="#org5da8a53">Programming and Algorithms</a></li>
<li><a href="#org31b53d2">Other Applications</a></li>
<li><a href="#org62254e4">Tooling</a></li>
<li><a href="#org6f27c05">PhD theses and Habilitation theses</a></li>
</ul>
</div>
</div>
<p>
This is a list of research papers and theses using the Mathematical
Components libraries and published (among others) in the following
venues:
</p>
<ul class="org-ul">
<li>ITP = Interactive Theorem Proving (was TPHOLs until 2009)</li>
<li>CPP = Certified Programs and Proofs</li>
<li>CICM = Conference on Intelligent Computer Mathematics</li>
<li>IJCAR = International Joint Conference on Automated Reasoning</li>
<li>ICFP = International Conference on Functional Programming</li>
<li>FSCD = International Conference on Formal Structures for Computation and Deduction</li>
<li>TACAS = International Conference on Tools and Algorithms for the Construction and Analysis of Systems</li>
<li>ESOP = European Symposium on Programming</li>
<li>POPL = Principles of Programming Languages</li>
<li>PPDP = Principles and Practice of Declarative Programming</li>
<li>JAR = Journal of Automated Reasoning</li>
<li>JFP = Journal of Functional Programming</li>
<li>LMCS = Logical Methods in Computer Science</li>
</ul>

<p>
Your paper/thesis is not in the list? You have a suggestion about the organization of this page?
Please, send <a href="mailto:mathcomp-dev@inria.fr?subject=MathComp%20related%20paper">us</a> a message or <a href="https://github.com/math-comp/math-comp.github.io">issue/PR on github</a>.
</p>

<div id="outline-container-org87c5133" class="outline-2">
<h2 id="org87c5133">Mathematics</h2>
<div class="outline-text-2" id="text-org87c5133">
<ul class="org-ul">
<li>Reinis Cirpons, Florent Hivert, Assia Mahboubi, Guillaume Melquiond, James Mitchell, Finn Smith, <span class="underline">Certifying the decidability of the word problem in monoids at large</span>. CPP 2026. <a href="https://hal.science/hal-05448783">pdf</a></li>
<li>Quentin Vermande, <span class="underline">Cylindrical Algebraic Decomposition in Coq/Rocq</span>. CPP 2026. <a href="https://dl.acm.org/doi/epdf/10.1145/3779031.3779100">pdf</a></li>
<li>Reynald Affeldt, Alessandro Bruni, Cyril Cohen, Pierre Roux, Takafumi Saikawa.
<span class="underline">Formalizing Concentration Inequalities in Rocq: Infrastructure and Automation</span>.
ITP 2025. <a href="https://drops.dagstuhl.de/storage/00lipics/lipics-vol352-itp2025/LIPIcs.ITP.2025.21/LIPIcs.ITP.2025.21.pdf">pdf</a></li>
<li>Quentin Vermande. <span class="underline">Décomposition Algébrique Cylindrique en Coq/Rocq</span>.
36es Journées Francophones des Langages Applicatifs (JFLA 2025). <a href="https://inria.hal.science/hal-04859512/file/jfla2025-final84.pdf">pdf</a></li>
<li>Reynald Affeldt.
<span class="underline">Prouver que π est irrationnel avec MathComp-Analysis</span>.
36es Journées Francophones des Langages Applicatifs (JFLA 2025). <a href="https://hal.science/hal-04859455v1/document">pdf</a></li>
<li>Florent Hivert.
<span class="underline">Machine Checked Proofs and Programs in Algebraic Combinatorics</span>.
CPP 2025. <a href="https://arxiv.org/pdf/2412.04864">pdf</a></li>
<li>Reynald Affeldt, Zachary Stone.
<span class="underline">A Comprehensive Overview of the Lebesgue Differentiation Theorem in Coq</span>.
ITP 2024. <a href="https://drops.dagstuhl.de/storage/00lipics/lipics-vol309-itp2024/LIPIcs.ITP.2024.5/LIPIcs.ITP.2024.5.pdf">pdf</a></li>
<li>Assia Mahboubi, Matthieu Piquerez.
<span class="underline">A First Order Theory of Diagram Chasing</span>.
32nd EACSL Annual Conference on Computer Science Logic (CSL 2024). <a href="https://drops.dagstuhl.de/storage/00lipics/lipics-vol288-csl2024/LIPIcs.CSL.2024.38/LIPIcs.CSL.2024.38.pdf">pdf</a></li>
<li>Benoît Guillemet, Assia Mahboubi, Matthieu Piquerez.
<span class="underline">Machine-Checked Categorical Diagrammatic Reasoning</span>.
FSCD 2024. <a href="https://drops.dagstuhl.de/storage/00lipics/lipics-vol299-fscd2024/LIPIcs.FSCD.2024.7/LIPIcs.FSCD.2024.7.pdf">pdf</a></li>
<li>Yoshihiro Ishiguro, Reynald Affeldt.
<span class="underline">The Radon-Nikodým Theorem and the Lebesgue-Stieltjes Measure in Coq</span>.
Computer Software 41(2), 2024. <a href="https://www.jstage.jst.go.jp/article/jssst/41/2/41_2_41/_pdf/-char/en">pdf</a></li>
<li>Reynald Affeldt, Cyril Cohen.
<span class="underline">Measure construction by extension in dependent type theory with application to integration</span>.
JAR 2023. <a href="https://arxiv.org/pdf/2209.02345.pdf">pdf</a></li>
<li>Pierre Pomeret-Coquot, Helene Fargier, Érik Martin-Dorel.
<span class="underline">Bel-Games: A Formal Theory of Games of Incomplete Information Based on Belief Functions in the Coq Proof Assistant</span>.
ITP 2023. <a href="https://drops.dagstuhl.de/opus/volltexte/2023/18400/pdf/LIPIcs-ITP-2023-25.pdf">pdf</a></li>
<li>Xavier Allamigeon, Quentin Canu, Pierre-Yves Strub.
<span class="underline">A Formal Disproof of Hirsch Conjecture</span>.
CPP 2023. <a href="https://arxiv.org/pdf/2301.04060.pdf">pdf</a></li>
<li>Xavier Allamigeon, Ricardo D. Katz, Pierre-Yves Strub.
<span class="underline">Formalizing the Face Lattice of Polyhedra</span>.
LMCS 18(2), 2022. <a href="https://lmcs.episciences.org/9570/pdf">pdf</a></li>
<li>Assia Mahboubi, Thomas Sibut-Pinote.
<span class="underline">A Formal Proof of the Irrationality of ζ(3)</span>.
LMCS 17(1), 2021. <a href="https://lmcs.episciences.org/7193/pdf">pdf</a></li>
<li>Sophie Bernard, Cyril Cohen, Assia Mahboubi, Pierre-Yves Strub.
<span class="underline">Unsolvability of the Quintic Formalized in Dependent Type Theory</span>
ITP 2021. <a href="https://hal.inria.fr/hal-03136002v3/document">pdf</a></li>
<li>Xavier Allamigeon, Ricardo D. Katz, Pierre-Yves Strub.
<span class="underline">Formalizing the Face Lattice of Polyhedra</span>.
IJCAR 2020. <a href="https://dx.doi.org/10.1007%2F978-3-030-51054-1_11">doi</a></li>
<li>Reynald Affeldt, Cyril Cohen, Marie Kerjean, Assia Mahboubi, Damien Rouhling, Kazuhiko Sakaguchi.
<span class="underline">Competing inheritance paths in dependent type theory: a case study in functional analysis</span>.
IJCAR 2020. <a href="https://hal.inria.fr/hal-02463336v2/document">pdf</a>, <a href="https://math-comp.github.io/competing-inheritance-paths-in-dependent-type-theory/">code</a></li>
<li>Xavier Allamigeon, Ricardo D. Katz.
<span class="underline">A Formalization of Convex Polyhedra Based on the Simplex Method</span>.
JAR 63(2), 2019. <a href="https://doi.org/10.1007/s10817-018-9477-1">doi</a></li>
<li>Florent Bréhard, Assia Mahboubi, Damien Pous. <span class="underline">A certificate-based
approach to formally verified approximations</span>. ITP 2019. <a href="https://hal.laas.fr/hal-02088529v2/document">pdf</a></li>
<li>Reynald Affeldt, Cyril Cohen, Damien Rouhling.
<span class="underline">Formalization techniques for asymptotic reasoning in classical analysis</span>.
Journal of Formalized Reasoning 11(1), 2018. <a href="https://jfr.unibo.it/article/view/8124/8407">pdf</a></li>
<li>Reynald Affeldt, Cyril Cohen, Assia Mahboubi, Damien Rouhling, Pierre-Yves Strub.
<span class="underline">Classical Analysis with Coq</span>. Coq Workshop 2018. <a href="https://staff.aist.go.jp/reynald.affeldt/documents/coqws-reals.pdf">pdf</a></li>
<li>Xavier Allamigeon, Ricardo D. Katz.
<span class="underline">A formalization of convex polyhedra based on the simplex method</span>. ITP 2017. <a href="https://arxiv.org/pdf/1706.10269.pdf">pdf</a></li>
<li>Evmorfia-Iro Bartzia.
<span class="underline">A Formalization of Elliptic Curves for Cryptography</span>.
PhD thesis, Université Paris-Saclay, 2017. <a href="https://pastel.archives-ouvertes.fr/tel-01563979/document">pdf</a></li>
<li>Guillaume Cano, Cyril Cohen, Maxime Dénès, Anders Mörtberg, Vincent Siles.
<span class="underline">Formalized linear algebra over Elementary Divisor Rings in Coq</span>.
LMCS 12(2), 2016. <a href="https://hal.inria.fr/hal-01081908/document">pdf</a></li>
<li>Cyril Cohen, Boris Djalal.
<span class="underline">Formalization of a newton series representation of polynomials</span>. CPP 2016. <a href="https://hal.inria.fr/hal-01240469/document">pdf</a></li>
<li>Ken'ichi Kuga, Manabu Hagiwara, Mitsuharu Yamamoto.
<span class="underline">Formalization of Bing's Shrinking Method in Geometric Topology</span>. CICM 2016. <a href="https://doi.org/10.1007/978-3-319-42547-4_2">doi</a></li>
<li>Gallego Arias, Emilio Jesús, Pierre Jouvelot.
<span class="underline">Adventures in the (not so) Complex Space</span>. Coq Workshop 2015. <a href="https://github.com/ejgallego/mini-dft-coq">paper, code, slides</a></li>
<li>Frédéric Chyzak, Assia Mahboubi, Thomas Sibut-Pinote, Enrico Tassi.
<span class="underline">A Computer-Algebra-Based Formal Proof of the Irrationality of ζ(3)</span>. ITP 2014. <a href="https://hal.inria.fr/hal-00984057/document">pdf</a></li>
<li>Cyril Cohen, Anders Mörtberg.
<span class="underline">A Coq Formalization of Finitely Presented Modules</span>. ITP 2014. <a href="https://perso.crans.org/cohen/papers/fpmods.pdf">pdf</a></li>
<li>Anders Mörtberg.
<span class="underline">Formalizing Refinements and Constructive Algebra in Type Theory</span>.
PhD, University of Gothenburg, 2014. <a href="http://staff.math.su.se/anders.mortberg/thesis/thesis.pdf">pdf</a></li>
<li>Evmorfia-Iro Bartzia, Pierre-Yves Strub.
<span class="underline">A Formal Library for Elliptic Curves in the Coq Proof Assistant</span>. ITP 2014. <a href="https://hal.inria.fr/hal-01102288/file/A-Formal-Library-for-Elliptic-Curves-in-the-Coq-Proof-Assistant.pdf">pdf</a></li>
<li>Jónathan Heras, Thierry Coquand, Anders Mörtberg, Vincent Siles.
<span class="underline">Computing persistent homology within Coq/SSReflect</span>. ACM Transactions on Computational Logic 14(4), 2013. <a href="https://arxiv.org/pdf/1209.1905.pdf">pdf</a></li>
<li>Georges Gonthier, Andrea Asperti, Jeremy Avigad, Yves Bertot, Cyril
Cohen, François Garillot, Stéphane Le Roux, Assia Mahboubi, Russell
O'Connor, Sidi Ould Biha, Ioana Pasca, Laurence Rideau, Alexey
Solovyev, Enrico Tassi, Laurent Théry.
<span class="underline">A Machine-Checked Proof of the Odd Order Theorem</span>. ITP 2013. <a href="https://hal.inria.fr/hal-00816699/document">pdf</a></li>
<li>Cyril Cohen. <span class="underline">Pragmatic Quotient Types in Coq</span>. ITP 2013. <a href="https://hal.inria.fr/hal-01966714/document">pdf</a></li>
<li>Assia Mahboubi. <span class="underline">The Rooster and the Butterflies</span>. CICM 2013. <a href="https://hal.inria.fr/hal-00825074v3/document">pdf</a></li>
<li>Maxime Dénès, Anders Mörtberg, Vincent Siles.
<span class="underline">A Refinement-Based Approach to Computational Algebra in Coq</span>. ITP 2012. <a href="https://hal.inria.fr/hal-00734505/document">pdf</a></li>
<li>Jónathan Heras, Maxime Dénès, Gadea Mata, Anders Mörtberg, María Poza, Vincent Siles.
<span class="underline">Towards a Certified Computation of Homology Groups for Digital Images</span>.
4th International Workshop on Computational Topology in Image Context (CTIC 2012). <a href="https://hal.inria.fr/hal-00711385/document">pdf</a></li>
<li>Assia Mahboubi, Cyril Cohen.
<span class="underline">Formal proofs in real algebraic geometry: from ordered fields to quantifier elimination</span>.
LMCS 8(1), 2012. <a href="https://hal.inria.fr/inria-00593738v4/document">pdf</a></li>
<li>Thierry Coquand, Anders Mörtberg, Vincent Siles.
<span class="underline">Coherent and Strongly Discrete Rings in Type Theory</span>. CPP 2012. <a href="https://staff.math.su.se/anders.mortberg/papers/coherent.pdf">pdf</a></li>
<li>Cyril Cohen.
<span class="underline">Formalized algebraic numbers: construction and first-order theory</span>.
PhD thesis, Ecole Polytechnique, 2012. <a href="https://pastel.archives-ouvertes.fr/pastel-00780446/file/main.pdf">pdf</a></li>
<li>Jónathan Heras, María Poza, Maxime Dénès, Laurence Rideau.
<span class="underline">Incidence Simplicial Matrices Formalized in Coq/SSReflect</span>.
18th Symposium on Symposium on the Integration of Symbolic Computation and Mechanized Reasoning (Calculemus 2011). <a href="https://hal.inria.fr/inria-00603208/file/ismfis.pdf">pdf</a></li>
<li>Georges Gonthier.
 <span class="underline">Point-Free, Set-Free Concrete Linear Algebra</span>.
ITP 2011. <a href="https://hal.inria.fr/hal-00805966/document">pdf</a></li>
<li>Sidi Ould Biha.
<span class="underline">Finite groups representation theory with Coq</span>.
8th International Conference on Mathematical Knowledge Management (MKM 2009). <a href="https://hal.inria.fr/inria-00377431/document">pdf</a></li>
<li>Yves Bertot, Georges Gonthier, Sidi Ould Biha, Ioana Pasca.
<span class="underline">Canonical Big Operators</span>.
ITP 2008. <a href="https://hal.inria.fr/inria-00331193/document">pdf</a></li>
<li>Georges Gonthier, Assia Mahboubi, Laurence Rideau, Enrico Tassi, Laurent Théry.
<span class="underline">A Modular Formalisation of Finite Group Theory</span>.
TPHOLs 2007. <a href="https://hal.inria.fr/inria-00139131v2/document">pdf</a></li>
<li>Laurent Théry, Laurence Rideau. <span class="underline">Formalising Sylow’s theorems in Coq</span>.
RT-0327 INRIA 2006. <a href="https://hal.inria.fr/inria-00113750v2/document">pdf</a></li>
</ul>
</div>

<div id="outline-container-orgdb20d60" class="outline-3">
<h3 id="orgdb20d60">Graph Theory</h3>
<div class="outline-text-3" id="text-orgdb20d60">
<ul class="org-ul">
<li>Christian Doczkal.
<span class="underline">A Variant of Wagner’s Theorem Based on Combinatorial Hypermaps</span>.
ITP 2021. <a href="https://hal.archives-ouvertes.fr/hal-03142192/document">pdf</a></li>
<li>Christian Doczkal, Damien Pous.
<span class="underline">Graph Theory in Coq: Minors, Treewidth, and Isomorphisms</span>.
JAR (special issue for ITP 2018), 2020. <a href="https://hal.archives-ouvertes.fr/hal-02316859/document">pdf</a></li>
<li>Christian Doczkal, Damien Pous.
<span class="underline">Completeness of an axiomatization of graph isomorphism via graph rewriting in Coq</span>.
CPP 2020. <a href="https://hal.archives-ouvertes.fr/hal-02333553/document">pdf</a></li>
<li>Daniel E. Severín.
<span class="underline">Formalization of the Domination Chain with Weighted Parameters</span>. ITP 2019. <a href="http://drops.dagstuhl.de/opus/volltexte/2019/11091/pdf/LIPIcs-ITP-2019-36.pdf">pdf</a></li>
<li>Christian Doczkal, Guillaume Combette, Damien Pous.
<span class="underline">A Formal Proof of the Minor-Exclusion Property for Treewidth-Two Graphs</span>. ITP 2018. <a href="https://hal.archives-ouvertes.fr/hal-01703922/document">pdf</a></li>
<li>George Gonthier.
<span class="underline">A computer-checked proof of the Four Colour Theorem</span>.
<a href="http://www2.tcs.ifi.lmu.de/~abel/lehre/WS07-08/CAFR/4colproof.pdf">pdf</a></li>
</ul>
</div>
</div>

<div id="outline-container-orgedc7c18" class="outline-3">
<h3 id="orgedc7c18">Robotics</h3>
<div class="outline-text-3" id="text-orgedc7c18">
<ul class="org-ul">
<li>Yves Bertot, Thomas Portet. <span class="underline">Formally Verifying a Vertical Cell Decomposition Algorithm</span>.
ITP 2025. <a href="https://drops.dagstuhl.de/storage/00lipics/lipics-vol352-itp2025/LIPIcs.ITP.2025.24/LIPIcs.ITP.2025.24.pdf">pdf</a></li>
<li>Yves Bertot. <span class="underline">Safe Smooth Paths Between Straight Line Obstacles</span>.
Logics and Type Systems in Theory and Practice, LNCS 14560, 2024.
<a href="https://doi.org/10.1007/978-3-031-61716-4">doi</a>, <a href="https://inria.hal.science/hal-04312815">pdf</a></li>
<li>Cyril Cohen, Damien Rouhling.
<span class="underline">A Formal Proof in Coq of LaSalle's Invariance Principle</span>. ITP 2017. <a href="https://hal.inria.fr/hal-01612293/document">pdf</a></li>
<li>Reynald Affeldt, Cyril Cohen.
<span class="underline">Formal Foundations of 3D Geometry to Model Robot Manipulators</span>. CPP 2017. <a href="https://hal.inria.fr/hal-01414753/document">pdf</a></li>
</ul>
</div>
</div>
</div>

<div id="outline-container-org5da8a53" class="outline-2">
<h2 id="org5da8a53">Programming and Algorithms</h2>
<div class="outline-text-2" id="text-org5da8a53">
<ul class="org-ul">
<li>Assia Mahboubi, Guillaume Melquiond, Pierre-Yves Strub, Tomás Vallejos Paradas.
<span class="underline">Functional correctness of an optimized modular inversion algorithm</span>. ITP 2026. <a href="https://hal.science/hal-05554365v1/document">pdf</a></li>
<li>Reynald Affeldt, Jacques Garrigue, Takafumi Saikawa.
<span class="underline">A practical formalization of monadic equational reasoning in dependent-type theory</span>.
JFP 35(e1). <a href="https://www.cambridge.org/core/services/aop-cambridge-core/content/view/B59B87DE000F48B9807F24AEDB11452E/S0956796824000157a.pdf/a-practical-formalization-of-monadic-equational-reasoning-in-dependent-type-theory.pdf">pdf</a></li>
<li>Cyril Cohen, Kazuhiko Sakaguchi.
<span class="underline">A bargain for mergesorts &#x2013; How to prove your mergesort correct and stable, almost for free</span>.
ICFP 2025. <a href="https://arxiv.org/pdf/2403.08173">pdf</a></li>
<li>Ana de Almeida Borges, Mireia González Bedmar, Juan Conejero Rodríguez, Eduardo Hermo Reyes, Joaquim Casals Buñuel, Joost J. Joosten.
<span class="underline">UTC time, formally verified</span>.
CPP 2024. <a href="https://arxiv.org/pdf/2209.14227.pdf">pdf</a></li>
<li>Philipp G. Haselwarter, Exequiel Rivas, Antoine Van Muylder, Théo Winterhalter,
Carmine Abate, Nikolaj Sidorenco, Cătălin Hriţcu, Kenji Maillard, Bas Spitters.
<span class="underline">SSProve: A Foundational Framework for Modular Cryptographic Proofs in Coq</span>.
ACM Transactions on Programming Languages and Systems 45(3), 2023. <a href="https://dl.acm.org/doi/pdf/10.1145/3594735">pdf</a></li>
<li>Ming-Hsien Tsai, Yu-Fu Fu, Jiaxiang Liu, Xiaomu Shi, Bow-Yaw Wang, Bo-Yin Yang.
<span class="underline">CoqCryptoLine: A Verified Model Checker with Certified Results</span>.
Conference on Computer-Aided Verification (CAV 2023). <a href="https://link.springer.com/chapter/10.1007/978-3-031-37703-7_11">doi</a></li>
<li>Ayumu Saito, Reynald Affeldt.
<span class="underline">Towards a Practical Library for Monadic Equational Reasoning in Coq</span>.
Mathematics of Program Construction (MPC 2022). <a href="https://staff.aist.go.jp/reynald.affeldt/documents/monae-mpc2022.pdf">pdf</a></li>
<li>Reynald Affeldt, David Nowak.
<span class="underline">Extending equational monadic reasoning with monad transformers</span>.
TYPES 2020. <a href="https://arxiv.org/pdf/2011.03463.pdf">pdf</a></li>
<li>Reynald Affeldt, David Nowak, Takafumi Saikawa.
<span class="underline">A Hierarchy of Monadic Effects for Program Verification Using Equational Reasoning</span>.
Mathematics of Program Construction (MPC 2019)</li>
<li>Ran Chen, Cyril Cohen, Jean-Jacques Levy, Stephan Merz, Laurent Thery.
<span class="underline">Formal Proof of Tarjan’s Strongly Connected Components Algorithm in Why3, Coq, and Isabelle</span>.
ITP 2019. <a href="http://drops.dagstuhl.de/opus/volltexte/2019/11068/pdf/LIPIcs-ITP-2019-13.pdf">pdf</a></li>
<li>Reynald Affeldt, Jacques Garrigue, Xuanrui Qi, Kazunari Tanaka.
<span class="underline">Proving tree algorithms for succinct data structures</span>.
ITP 2019. <a href="https://arxiv.org/pdf/1904.02809.pdf">pdf</a></li>
<li>Reynald Affeldt, Jacques Garrigue, Xuanrui Qi, Kazunari Tanaka.
<span class="underline">Experience Report: Type-Driven Development of Certified Tree Algorithms in Coq</span>.
Coq Workshop 2019. <a href="https://staff.aist.go.jp/reynald.affeldt/coq2019/coqws2019-affeldt-garrigue-qi-tanaka.pdf">pdf</a></li>
<li>Cyril Cohen, Damien Rouhling.
<span class="underline">A refinement-based approach to large scale reflection for algebra</span>.
28ème Journées Francophones des Langages Applicatifs (JFLA 2017). <a href="https://hal.inria.fr/hal-01414881/document">pdf</a></li>
<li>Timmy Weerwag.
<span class="underline">Verifying an elliptic curve cryptographic algorithm using Coq and the Ssreflect extension</span>.
Master’s thesis, Mathematics, Radboud University, 2016. <a href="https://www.ru.nl/publish/pages/813286/weerwag_timmy_-1a.pdf">pdf</a></li>
<li>Beta Ziliani, Derek Dreyer, Neelakantan R. Krishnaswami, Aleksandar Nanevski, Viktor Vafeiadis.
<span class="underline">Mtac: A Monad for Typed Tactic Programming in Coq</span>. JFP 25, 2015. <a href="https://people.mpi-sws.org/~dreyer/papers/mtac/journal.pdf">pdf</a></li>
<li>Cyril Cohen, Maxime Dénès, Anders Mörtberg.
<span class="underline">Refinements for free!</span>. CPP 2013. <a href="https://hal.inria.fr/hal-01113453/document">pdf</a></li>
<li>Andrew Kennedy, Nick Benton, Jonas B. Jensen, Pierre-Evariste Dagand.
<span class="underline">Coq: the world's best macro assembler?</span> PPDP 2013. <a href="http://nickbenton.name/coqasm.pdf">pdf</a></li>
<li>Germán Andrés Delbianco, Aleksandar Nanevski.
<span class="underline">Hoare-Style Reasoning with (Algebraic) Continuations</span>. ICFP 2013. <a href="https://doi.org/10.1145/2544174.2500593">doi</a></li>
<li>Beta Ziliani, Derek Dreyer, Neelakantan R. Krishnaswami, Aleksandar Nanevski, Viktor Vafeiadis.
<span class="underline">Mtac: A Monad for Typed Tactic Programming in Coq</span>. ICFP 2013. <a href="https://doi.org/10.1017/S0956796815000118">doi</a></li>
<li>Aleksandar Nanevski, Viktor Vafeiadis, Josh Berdine.
<span class="underline">Structuring the Verification of Heap-Manipulating Programs</span>. POPL 2010. <a href="https://doi.org/10.1145/1706299.1706331">doi</a></li>
</ul>
</div>

<div id="outline-container-org88cc409" class="outline-3">
<h3 id="org88cc409">Concurrency</h3>
<div class="outline-text-3" id="text-org88cc409">
<ul class="org-ul">
<li>Mohit Tekriwal, Avi Tachna-Fram, Jean-Baptiste Jeannin, Manos Kapritsos, Dimitra Panagou.
<span class="underline">Formally verified asymptotic consensus in robust networks</span>.
TACAS 2024. <a href="https://arxiv.org/pdf/2202.13833.pdf">pdf</a></li>
<li>Søren Eller Thomsen, Bas Spitters.
<span class="underline">Formalizing Nakamoto-Style Proof of Stake</span>.
34th IEEE Computer Security Foundations Symposium (CSF 2021). <a href="https://arxiv.org/pdf/2007.12105">pdf</a></li>
<li>Musab A. Alturki, Jing Chen, Victor Luchangco, Brandon Moore, Karl Palmskog, Lucas Peña, Grigore Roşu.
<span class="underline">Towards a Verified Model of the Algorand Consensus Protocol in Coq</span>.
1st Workshop on Formal Methods for Blockchains (FMBC 2019). <a href="https://arxiv.org/pdf/1907.05523">pdf</a></li>
<li>Joseph Tassarotti, Robert Harper.
<span class="underline">A Separation Logic for Concurrent Randomized Programs</span>.
POPL 2019. <a href="http://www.cs.bc.edu/~tassarot/papers/iris-prob-paper/paper.pdf">pdf</a></li>
<li>Ilya Sergey, James R. Wilcox, Zachary Tatlock.
<span class="underline">Programming and Proving with Distributed Protocols</span>. POPL 2018. <a href="https://dl.acm.org/citation.cfm?doid=3177123.3158116">pdf</a></li>
<li>George Pîrlea, Ilya Sergey. <span class="underline">Mechanising Blockchain Consensus</span>. CPP 2018. <a href="https://dl.acm.org/citation.cfm?id=3167086">pdf</a></li>
<li>Germán Andrés Delbianco, Ilya Sergey, Aleksandar Nanevski, Anindya Banerjee.
<span class="underline">Concurrent Data Structures Linked in Time</span>.
European Conference on Object-Oriented Programming (ECOOP 2017). <a href="https://drops.dagstuhl.de/opus/volltexte/2017/7255/pdf/LIPIcs-ECOOP-2017-8.pdf">pdf</a></li>
<li>Mitsuharu Yamamoto, Shogo Sekine, Saki Matsumoto.
<span class="underline">Formalization of Karp-Miller Tree Construction on Petri Nets</span>. CPP 2017. <a href="https://doi.org/10.1145/3018610.3018626">doi</a></li>
<li>Germán Andrés Delbianco.
<span class="underline">Hoare-style Reasoning with Higher-order Control: Continuations and Concurrency</span>.
PhD thesis, Computer Science, Universidad Politécnica de Madrid, 2017. <a href="http://oa.upm.es/47796/1/GERMAN_ANDRES_DELBIANCO.pdf">pdf</a></li>
<li>Ralf Jung, Robbert Krebbers, Lars Birkedal, Derek Dreyer.
<span class="underline">Higher-Order Ghost State</span>.
ICFP 2016. <a href="https://dl.acm.org/doi/pdf/10.1145/2951913.2951943">pdf</a></li>
<li>Ilya Sergey, Aleksandar Nanevski, Anindya Banerjee, Germán Andrés Delbianco.
<span class="underline">Hoare-style Specifications as Correctness Conditions for Non-linearizable Concurrent Objects</span>.
Object-oriented Programming, Systems, Languages, and Applications (OOPSLA 2016). <a href="https://arxiv.org/pdf/1509.06220.pdf">pdf</a></li>
<li>Ilya Sergey, Aleksandar Nanevski, Anindya Banerjee.
 <span class="underline">Mechanized Verification of Fine-grained Concurrent Programs</span>.
Programming Language Design and Implementation (PLDI 2015). <a href="https://doi.org/10.1145/2737924.2737964">doi</a></li>
<li>Ilya Sergey, Aleksandar Nanevski, Anindya Banerjee.
 <span class="underline">Specifying and Verifying Concurrent Algorithms with Histories and Subjectivity</span>.
ESOP 2015. <a href="https://arxiv.org/pdf/1410.0306.pdf">pdf</a></li>
<li>Aleksandar Nanevski, Ruy Ley-Wild, Ilya Sergey, Germán Andrés Delbianco.
 <span class="underline">Communicating State Transition Systems for Fine-Grained Concurrent Resources</span>.
ESOP 2014. <a href="https://doi.org/10.1007/978-3-642-54833-8_16">doi</a></li>
<li>Ruy Ley-Wild, Aleksandar Nanevski.
<span class="underline">Subjective Auxiliary State for Coarse-Grained Concurrency</span>. POPL 2013. <a href="https://doi.org/10.1145/2429069.2429134">doi</a></li>
</ul>
</div>
</div>

<div id="outline-container-orgb0747c7" class="outline-3">
<h3 id="orgb0747c7">Information Flow</h3>
<div class="outline-text-3" id="text-orgb0747c7">
<ul class="org-ul">
<li>Aleksandar Nanevski, Anindya Banerjee, Deepak Garg.
<span class="underline">Dependent Type Theory for Verification of Information Flow and Access Control Policies</span>.
ACM Transactions on Programming Languages and Systems, 35(2):6:1-6:41, 2013. <a href="https://doi.org/10.1145/2491522.2491523">doi</a></li>
<li>Gordon Stewart, Anindya Banerjee, Aleksandar Nanevski.
<span class="underline">Dependent Types for Enforcement of Information Flow and Erasure Policies in Heterogeneous Data Structures</span>.
PPDP 2013. <a href="https://doi.org/10.1145/2505879.2505895">doi</a></li>
<li>Aleksandar Nanevski, Anindya Banerjee, Deepak Garg.
 <span class="underline">Verification of Information Flow and Access Control Policies with Dependent Types</span>.
2011 IEEE Symposium on Security and Privacy. <a href="https://ieeexplore.ieee.org/document/5958028">IEEE Xplore</a></li>
</ul>
</div>
</div>

<div id="outline-container-orgc76c72b" class="outline-3">
<h3 id="orgc76c72b">Probabilistic Reasoning</h3>
<div class="outline-text-3" id="text-orgc76c72b">
<ul class="org-ul">
<li>Reynald Affeldt, Yoshihiro Ishiguro, Zachary Stone.
<span class="underline">A Formal Foundation for Equational Reasoning on Probabilistic Programs</span>.
Asian Symposium on Programming Languages and Systems (APLAS 2025). <a href="https://doi.org/10.1007/978-981-95-3585-9_3">doi</a></li>
<li>Reynald Affeldt, Cyril Cohen, Ayumu Saito.
<span class="underline">Semantics of Probabilistic Programs Using s-Finite Kernels in Dependent Type Theory</span>.
ACM Transactions on Probabilistic Machine Learning 1(3), 2025. <a href="https://dl.acm.org/doi/pdf/10.1145/3732291">pdf</a></li>
<li>Reynald Affeldt, Clark Barrett, Alessandro Bruni, Ieva Daukantas, Harun Khan, Takafumi Saikawa, Carsten Schürmann.
<span class="underline">Robust Mean Estimation by All Means (short paper)</span>.
ITP 2024. <a href="https://drops.dagstuhl.de/storage/00lipics/lipics-vol309-itp2024/LIPIcs.ITP.2024.39/LIPIcs.ITP.2024.39.pdf">pdf</a></li>
<li>Filip Markovic, Pierre Roux, Sergey Bozhko, Alessandro V. Papadopoulos, Björn B. Brandenburg.
<span class="underline">CTA: A Correlation-Tolerant Analysis of the Deadline-Failure Probability of Dependent Tasks</span>.
IEEE Real-Time Systems Symposium (RTSS 2023). <a href="https://people.mpi-sws.org/~bbb/papers/pdf/rtss23-CTA.pdf">pdf</a></li>
<li>Ayumu Saito, Reynald Affeldt.
<span class="underline">Experimenting with an Intrinsically-Typed Probabilistic Programming Language in Coq</span>.
Asian Symposium on Programming Languages and Systems (APLAS 2023). <a href="https://link.springer.com/chapter/10.1007/978-981-99-8311-7_9">doi</a></li>
<li>Reynald Affeldt, Cyril Cohen, Ayumu Saito.
<span class="underline">Semantics of Probabilistic Programs using s-Finite Kernels in Coq</span>.
CPP 2023. <a href="https://hal.inria.fr/hal-03917948/document">pdf</a></li>
<li>Ieva Daukantas, Alessandro Bruni, Carsten Schürmann.
<span class="underline">Trimming Data Sets: a Verified Algorithm for Robust Mean Estimation</span>.
PPDP 2021. <a href="https://doi.org/10.1145/3479394.3479412">doi</a></li>
<li>Reynald Affeldt, Jacques Garrigue, David Nowak, Takafumi Saikawa.
<span class="underline">A trustful monad for axiomatic reasoning with probability and nondeterminism</span>.
JFP 31(E17), 2021. <a href="https://arxiv.org/pdf/2003.09993.pdf">pdf</a></li>
<li>Kiran Gopinathan, Ilya Sergey.
<span class="underline">Certifying Certainty and Uncertainty in Approximate Membership Query Structures</span>.
32nd International Conference on Computer-Aided Verification (CAV 2020). <a href="https://arxiv.org/pdf/2004.13312.pdf">pdf</a></li>
<li>Reynald Affeldt, Jacques Garrigue, Takafumi Saikawa.
<span class="underline">Formal adventures in convex and conical spaces</span>.
CICM 2020. <a href="https://arxiv.org/pdf/2004.12713.pdf">pdf</a></li>
<li>Reynald Affeldt, Jacques Garrigue, Takafumi Saikawa.
<span class="underline">Reasoning with conditional probabilities and joint distributions</span>.
Computer Software 37(3):79-95, 2020. <a href="https://staff.aist.go.jp/reynald.affeldt/documents/cproba_preprint.pdf">pdf</a></li>
<li>Joseph Tassarotti, Robert Harper.
<span class="underline">Verified Tail Bounds for Randomized Programs</span>. ITP 2018. <a href="https://www.cs.cmu.edu/~rwh/papers/tail-bounds/paper.pdf">pdf</a></li>
</ul>
</div>
</div>

<div id="outline-container-org1c6c872" class="outline-3">
<h3 id="org1c6c872">Quantum Computing</h3>
<div class="outline-text-3" id="text-org1c6c872">
<ul class="org-ul">
<li>Jacques Garrigue, Takafumi Saikawa.
<span class="underline">Typed Compositional Quantum Computation with Lenses</span>.
JAR 70(10). <a href="https://link.springer.com/article/10.1007/s10817-026-09750-3">pdf</a></li>
<li>Yingte Xu, Gilles Barthe, Li Zhou.
<span class="underline">Automating Equational Proofs in Dirac Notation</span>.
POPL 2025. <a href="https://arxiv.org/pdf/2411.11617">pdf</a></li>
<li>Jacques Garrigue and Takafumi Saikawa.
<span class="underline">Typed compositional quantum computation with lenses</span>.
ITP 2024. <a href="https://drops.dagstuhl.de/storage/00lipics/lipics-vol309-itp2024/LIPIcs.ITP.2024.15/LIPIcs.ITP.2024.15.pdf">pdf</a></li>
<li>Li Zhou, Gilles Barthe, Pierre-Yves Strub, Junyi Liu, Mingsheng Ying.
<span class="underline">CoqQ: Foundational Verification of Quantum Programs</span>.
POPL 2023. <a href="https://arxiv.org/pdf/2207.11350.pdf">pdf</a></li>
</ul>
</div>
</div>
</div>

<div id="outline-container-org31b53d2" class="outline-2">
<h2 id="org31b53d2">Other Applications</h2>
<div class="outline-text-2" id="text-org31b53d2">
<ul class="org-ul">
<li>Pierre-Léo Bégay, Pierre Crégut, Jean-François Monin.
<span class="underline">Developing and certifying Datalog optimizations in Coq/MathComp</span>. CPP 2021. <a href="https://hal.archives-ouvertes.fr/hal-03065304v1/document">pdf</a></li>
<li>Gallego Arias, Emilio Jesús, Olivier Hermant, Pierre Jouvelot.
<span class="underline">A Taste of Sound Reasoning in Faust</span>.
Linux Audio Conference 2015. <a href="https://github.com/ejgallego/mini-faust-coq">paper, code, slides</a></li>
<li>Maxime Dénès, Benjamin Lesage, Yves Bertot, Adrien Richard.
<span class="underline">Formal proof of theorems on genetic regulatory networks</span>.
 11th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing (SYNACS 2009).
 <a href="https://ieeexplore.ieee.org/document/5460865">IEEE Xplore</a></li>
</ul>
</div>

<div id="outline-container-org8194567" class="outline-3">
<h3 id="org8194567">Logic, Types, and Verification</h3>
<div class="outline-text-3" id="text-org8194567">
<ul class="org-ul">
<li>Jan Bessai, Jakob Rehof, Boris Düdder.
<span class="underline">Fast Veriﬁed BCD Subtyping</span>.
Models, Mindsets, Meta: The What, the How, and the Why Not? LNCS 11200, 2019. <a href="https://doi.org/10.1007/978-3-030-22348-9_21">doi</a></li>
<li>Christian Doczkal, Gert Smolka.
<span class="underline">Regular Language Representations in the Constructive Type Theory of Coq</span>.
JAR 61, 2018. <a href="https://hal.archives-ouvertes.fr/hal-01832031/document">pdf</a></li>
<li>Christian Doczkal, Joachim Bard.
<span class="underline">Completeness and Decidability of Converse PDL in the Constructive Type Theory of Coq</span>.
CPP 2018. <a href="https://hal.archives-ouvertes.fr/hal-01646782/document">pdf</a></li>
<li>Angela Bonifati, Stefania Dumbrava, Emilio Jesús Gallego Arias.
<span class="underline">Certified Graph View Maintenance with Regular Datalog</span>.
34th International Conference on Logic Programming (ICLP 2018). <a href="https://hal.archives-ouvertes.fr/hal-01932818/document">pdf</a></li>
<li>Véronique Benzaken, Evelyne Contejean, Stefania Dumbrava.
<span class="underline">Certifying Standard and Stratified Datalog Inference Engines in SSReflect</span>. ITP 2017. <a href="https://hal.archives-ouvertes.fr/hal-01745566/file/ITP2017.pdf">pdf</a></li>
<li>Felipe Cerqueira, Felix Stutz, Björn Brandenburg.
 <span class="underline">Prosa: A Case for Readable Mechanized Schedulability Analysis</span>.
28th Euromicro Conference on Real-Time Systems (ECRTS 2016). <a href="https://ieeexplore.ieee.org/document/7557887">IEEE Xplore</a></li>
<li>Christian Doczkal, Gert Smolka.
<span class="underline">Completeness and Decidability Results for CTL in Constructive Type Theory</span>.
JAR 56, 2016. <a href="https://doi.org/10.1007/s10817-016-9361-9">doi</a></li>
<li>Christian Doczkal, Gert Smolka.
<span class="underline">Completeness and Decidability Results for CTL in Coq</span>. ITP 2014. <a href="https://www.ps.uni-saarland.de/Publications/documents/DoczkalSmolka_2014_comp-dec-CTL.pdf">pdf</a></li>
<li>Christian Doczkal, Gert Smolka.
<span class="underline">Constructive Completeness for Modal Logic with Transitive Closure</span>. CPP 2012. <a href="https://doi.org/10.1007/978-3-642-35308-6_18">doi</a></li>
<li>Christian Doczkal, Gert Smolka.
<span class="underline">Constructive Formalization of Hybrid Logic with Eventualities</span>. CPP 2011. <a href="https://www.ps.uni-saarland.de/Publications/documents/DoczkalSmolka_2011_Constructive_0.pdf">pdf</a></li>
<li>Thierry Coquand, Vincent Siles.
<span class="underline">A Decision Procedure for Regular Expression Equivalence in Type Theory</span>. CPP 2011. <a href="https://doi.org/10.1007/978-3-642-25379-9_11">doi</a></li>
<li>Kasper Svendsen, Lars Birkedal, Aleksandar Nanevski.
 <span class="underline">Partiality, State and Dependent Types</span>.
International Conference on Typed Lambda Calculi and Applications (TLCA 2011). <a href="https://doi.org/10.1007/978-3-642-21691-6_17">doi</a></li>
</ul>
</div>
</div>

<div id="outline-container-org213556a" class="outline-3">
<h3 id="org213556a">Information Theory</h3>
<div class="outline-text-3" id="text-org213556a">
<ul class="org-ul">
<li>Joshua M. Cohen, Qinshi Wang, Andrew W. Appel.
<span class="underline">Verified Erasure Correction in Coq with MathComp and VST</span>.
34th International Conference on Computer-Aided Verification (CAV 2022).  <a href="https://www.cs.princeton.edu/~appel/papers/FECVerification.pdf">pdf</a></li>
<li>Reynald Affeldt, Jacques Garrigue, Takafumi Saikawa.
<span class="underline">A library for formalization of linear error-correcting codes</span>.
JAR 64:1123-1164, 2020. <a href="https://staff.aist.go.jp/reynald.affeldt/documents/ecc.pdf">pdf</a></li>
<li>Kyosuke Nakano, Manabu Hagiwara.
<span class="underline">Formalization of binary symmetric erasure channel based on infotheo</span>.
International Symposium on Information Theory and its Application 2016 (ISITA 2016).
<a href="https://ieeexplore.ieee.org/document/7840477">IEEE Xplore</a></li>
<li>Reynald Affeldt, Jacques Garrigue, Takafumi Saikawa.
<span class="underline">Formalization of Reed-Solomon codes and progress report on formalization of LDPC codes</span>.
International Symposium on Information Theory and its Application 2016 (ISITA 2016)</li>
<li>Reynald Affeldt, Jacques Garrigue.
<span class="underline">Formalization of error-correcting codes: from Hamming to modern coding theory</span>. ITP 2015. <a href="https://staff.aist.go.jp/reynald.affeldt/documents/eccITP2015_authorsversion.pdf">pdf</a></li>
<li>Ryosuke Obi, Manabu Hagiwara, Reynald Affeldt.
 <span class="underline">Formalization of the variable-length source coding theorem: Direct part</span>.
International Symposium on Information Theory and its Application 2014 (ISITA 2014). <a href="https://ieeexplore.ieee.org/document/6979832">IEEE Xplore</a></li>
<li>Reynald Affeldt, Manabu Hagiwara, Jonas Sénizergues.
<span class="underline">Formalization of Shannon's theorems</span>. JAR 53(1), 2014. <a href="https://staff.aist.go.jp/reynald.affeldt/documents/shannon_theorems.pdf">pdf</a></li>
<li>Reynald Affeldt, Manabu Hagiwara.
<span class="underline">Formalization of Shannon's Theorems in SSReflect-Coq</span>. ITP 2012. <a href="https://staff.aist.go.jp/reynald.affeldt/documents/affeldt-itp2012-preprint.pdf">pdf</a></li>
</ul>
</div>
</div>
</div>

<div id="outline-container-org62254e4" class="outline-2">
<h2 id="org62254e4">Tooling</h2>
<div class="outline-text-2" id="text-org62254e4">
<ul class="org-ul">
<li>Cyril Cohen, Enzo Crance, Assia Mahboubi.
<span class="underline">Trocq: Proof Transfer for Free, With or Without Univalence</span>.
ESOP 2024. <a href="https://arxiv.org/pdf/2310.14022">pdf</a></li>
<li>Xavier Allamigeon, Quentin Canu, Cyril Cohen, Kazuhiko Sakaguchi, Pierre-Yves Strub.
<span class="underline">Design patterns of hierarchies for order structures</span>.
HAL 2023. <a href="https://inria.hal.science/hal-04008820/document">pdf</a></li>
<li>Valentin Blot, Denis Cousineau, Enzo Crance, Louise Dubois de Prisque, Chantal Keller, Assia Mahboubi, Pierre Vial.
<span class="underline">Compositional Pre-processing for Automated Reasoning in Dependent Type Theory</span>.
CPP 2023. <a href="https://arxiv.org/pdf/2204.02643.pdf">pdf</a></li>
<li>Benjamin Grégoire, Jean-Christophe Léchenet, Enrico Tassi.
<span class="underline">Practical and sound equality tests, automatically</span>.
CPP 2023. <a href="https://hal.inria.fr/hal-03800154/document">pdf</a></li>
<li>Kazuhiko Sakaguchi. <span class="underline">Reflexive tactics for algebra, revisited</span>. ITP 2022. <a href="https://arxiv.org/pdf/2202.04330.pdf">pdf</a></li>
<li>Reynald Affeldt, Xavier Allamigeon, Yves Bertot, Quentin Canu, Cyril Cohen, Pierre Roux, Kazuhiko Sakaguchi, Enrico Tassi, Laurent Théry, Anton Trunov.
<span class="underline">Porting the Mathematical Components library to Hierarchy Builder</span>. Coq Workshop 2021. <a href="https://coq-workshop.gitlab.io/2021/abstracts/Coq2021-01-02-mathcomp-hierarchy-builder.pdf">pdf</a></li>
<li>Pierre-Léo Bégay, Pierre Crégut, Jean-Francois Monin.
<span class="underline">Developing sequence and tree fintypes in MathComp</span>. Coq Workshop 2020. <a href="https://coq-workshop.gitlab.io/2020/abstracts/Coq2020_03-03-seq-fintype.pdf">pdf</a></li>
<li>Xavier Allamigeon, Cyril Cohen, Kazuhiko Sakaguchi, Pierre-Yves Strub.
<span class="underline">A hierarchy of ordered types in Mathematical Components</span>. Coq Workshop 2020. <a href="https://coq-workshop.gitlab.io/2020/abstracts/Coq2020_03-02-ordered.pdf">pdf</a></li>
<li>Cyril Cohen, Kazuhiko Sakaguchi, Enrico Tassi.
<span class="underline">Hierarchy Builder: algebraic hierarchies made easy in Coq with Elpi</span>.
FSCD 2020. <a href="https://hal.inria.fr/hal-02478907v4/document">pdf</a></li>
<li>Karl Palmskog, Ahmet Celik, Milos Gligoric.
<span class="underline">Practical Machine-Checked Formalization of Change Impact Analysis</span>.
TACAS 2020. <a href="https://users.ece.utexas.edu/~gligoric/papers/PalmskogETAL20Chip.pdf">pdf</a></li>
<li>Kazuhiko Sakaguchi. <span class="underline">Validating Mathematical Structures</span>. IJCAR 2020. <a href="https://arxiv.org/pdf/2002.00620.pdf">pdf</a></li>
<li>Kazuhiko Sakaguchi. <span class="underline">Program extraction for mutable arrays</span>. Science of Computer Programming 191, 2020. <a href="https://doi.org/10.1016/j.scico.2019.102372">doi</a></li>
<li>Erik Martin-Dorel, Enrico Tassi. <span class="underline">SSReflect in Coq 8.10</span>. Coq Workshop 2019. <a href="https://staff.aist.go.jp/reynald.affeldt/coq2019/coqws2019-martindorel-tassi.pdf">pdf</a></li>
<li>Kazuhiko Sakaguchi. <span class="underline">Program Extraction for Mutable Arrays</span>.
15th International Symposium on Functional and Logic Programming (FLOPS 2018). <a href="https://doi.org/10.1007/978-3-319-90686-7_4">doi</a></li>
<li>Kazuhiko Sakaguchi, Yukiyoshi Kameyama.
<span class="underline">Efficient Finite-Domain Function Library for the Coq Proof Assistant</span>.
IPSJ Transactions on Programming 10(1), 2017. <a href="http://logic.cs.tsukuba.ac.jp/~sakaguchi/papers/ipsj-pro-2016-1-7.pdf">pdf (long, in Japanese)</a>, <a href="http://logic.cs.tsukuba.ac.jp/~sakaguchi/papers/ipsj-pro-2016-1-7.en.pdf">pdf (short, in English)</a></li>
<li>Georges Gonthier, Beta Ziliani, Aleksandar Nanevski, Derek Dreyer.
<span class="underline">How to make ad hoc proof automation less ad hoc</span>. JFP 23(4), 2013. <a href="https://doi.org/10.1017/S0956796813000051">doi</a></li>
<li>Vladimir Komendantsky, Alexander Konovalov, Steve Linton.
<span class="underline">Interfacing Coq + SSReflect with GAP</span>. Electronic Notes in Theoretical Computer Science 285, 2012. <a href="https://www.sciencedirect.com/science/article/pii/S1571066112000230">pdf</a></li>
<li>Iain Whiteside, David Aspinall, Gudmund Grov.
<span class="underline">An Essence of SSReflect</span>. CICM 2012. <a href="https://doi.org/10.1007/978-3-642-31374-5_13">doi</a></li>
<li>Georges Gonthier, Enrico Tassi.
<span class="underline">A Language of Patterns for Subterm Selection</span>. ITP 2012. <a href="https://hal.inria.fr/hal-00652286/file/rew.pdf">pdf</a></li>
<li>Georges Gonthier, Assia Mahboubi.
<span class="underline">An introduction to small scale reflection in Coq</span>. Journal of Formalized Reasoning 3(2), 2010. <a href="https://hal.inria.fr/inria-00515548v4/document">pdf</a></li>
<li>François Garillot, Georges Gonthier, Assia Mahboubi, Laurence Rideau.
<span class="underline">Packaging Mathematical Structures</span>. TPHOLs 2009. <a href="https://hal.inria.fr/inria-00368403v1/document">pdf</a></li>
</ul>
</div>

<div id="outline-container-org9895a49" class="outline-3">
<h3 id="org9895a49">Machine Learning</h3>
<div class="outline-text-3" id="text-org9895a49">
<ul class="org-ul">
<li>Reynald Affeldt, Alessandro Bruni, Ekaterina Komendantskaya, Natalia Ślusarz, Kathrin Stark.
<span class="underline">Taming Differentiable Logics with Coq Formalisation</span>.
ITP 2024. <a href="https://drops.dagstuhl.de/storage/00lipics/lipics-vol309-itp2024/LIPIcs.ITP.2024.4/LIPIcs.ITP.2024.4.pdf">pdf</a></li>
<li>Pengyu Nie, Karl Palmskog, Junyi Jessy Li, Milos Gligoric.
<span class="underline">Deep Generation of Coq Lemma Names Using Elaborated Terms</span>. IJCAR 2020. <a href="https://arxiv.org/pdf/2004.07761.pdf">pdf</a></li>
<li>Jónathan Heras, Ekaterina Komendantskaya.
<span class="underline">Recycling Proof Patterns in Coq: Case Studies</span>. Mathematics in Computer Science 8(1), 2014. <a href="https://arxiv.org/pdf/1301.6039v4.pdf">pdf</a></li>
<li>Jónathan Heras, Ekaterina Komendantskaya.
<span class="underline">Proof Pattern Search in Coq/SSReflect</span>. <a href="https://arxiv.org/pdf/1402.0081.pdf">CoRR abs/1402.0081</a>, 2014</li>
<li>Jónathan Heras, Ekaterina Komendantskaya.
<span class="underline">ML4PG in Computer Algebra Verification</span>. CICM 2013. <a href="https://arxiv.org/pdf/1302.6421.pdf">pdf</a></li>
</ul>
</div>
</div>
</div>

<div id="outline-container-org6f27c05" class="outline-2">
<h2 id="org6f27c05">PhD theses and Habilitation theses</h2>
<div class="outline-text-2" id="text-org6f27c05">
<ul class="org-ul">
<li>Cyril Cohen.
<span class="underline">Structuring Mathematics in Dependent Type Theory</span>
Habilitation thesis, 2026. <a href="https://perso.crans.org/cohen/hdr.pdf">pdf</a></li>
<li>Enrico Tassi.
<span class="underline">Elpi: rule-based extension language</span>
Habilitation thesis, 2026. <a href="https://inria.hal.science/hal-05294918v1">pdf</a></li>
<li>Pierre Roux.
<span class="underline">Numerical Computations and Proofs: from Proof-Assistants to Aerospace Applications</span>
Habilitation thesis, 2025. <a href="https://www.onera.fr/sites/default/files/447/hdr.pdf">pdf</a></li>
<li>Assia Mahboubi.
<span class="underline">Machine-checked computer-aided mathematics</span>
Habilitation thesis, 2021. <a href="https://theses.hal.science/tel-03107626v2">pdf</a></li>
</ul>
</div>
</div>
</div>
</body>
</html>