#+TITLE: Mathematical Components: Research Papers

#+OPTIONS: toc:1

#+OPTIONS: ^:nil

#+OPTIONS: html-postamble:nil

#+OPTIONS: num:nil

#+HTML_HEAD: <meta http-equiv="Content-Type" content="text/html; charset=utf-8">

#+HTML_HEAD: <style type="text/css"> body {font-family: Arial, Helvetica; margin-left: 5em; font-size: large;} </style>

#+HTML_HEAD: <style type="text/css"> h1 {margin-left: 0em; padding: 0px; text-align: center} </style>

#+HTML_HEAD: <style type="text/css"> h2 {margin-left: 0em; padding: 0px; color: #580909} </style>

#+HTML_HEAD: <style type="text/css"> h3 {margin-left: 1em; padding: 0px; color: #C05001;} </style>

#+HTML_HEAD: <style type="text/css"> body { max-width: 1100px; width: 100% - 30px; margin-left: 30px}</style>

This is a list of research papers and theses using the Mathematical

Components libraries and published (among others) in the following

venues:

- ITP = Interactive Theorem Proving (was TPHOLs until 2009)

- CPP = Certified Programs and Proofs

- CICM = Conference on Intelligent Computer Mathematics

- IJCAR = International Joint Conference on Automated Reasoning

- ICFP = International Conference on Functional Programming

- FSCD = International Conference on Formal Structures for Computation and Deduction

- TACAS = International Conference on Tools and Algorithms for the Construction and Analysis of Systems

- ESOP = European Symposium on Programming

- POPL = Principles of Programming Languages

- PPDP = Principles and Practice of Declarative Programming

- JAR = Journal of Automated Reasoning

- JFP = Journal of Functional Programming

- LMCS = Logical Methods in Computer Science

Your paper/thesis is not in the list? You have a suggestion about the organization of this page?

Please, send [[mailto:mathcomp-dev@inria.fr?subject=MathComp related paper][us]] a message or [[https://github.com/math-comp/math-comp.github.io][issue/PR on github]].

#+BEGIN_COMMENT

This is a memo to serve in the event we change the sectioning

[2020-07-05 Sun] What about "program verification" and "probabilistic reasoning" sections?

#+END_COMMENT

* Mathematics

- Reinis Cirpons, Florent Hivert, Assia Mahboubi, Guillaume Melquiond, James Mitchell, Finn Smith, _Certifying the decidability of the word problem in monoids at large_. CPP 2026. [[https://hal.science/hal-05448783][pdf]]

- Quentin Vermande, _Cylindrical Algebraic Decomposition in Coq/Rocq_. CPP 2026. [[https://dl.acm.org/doi/epdf/10.1145/3779031.3779100][pdf]]

- Reynald Affeldt, Alessandro Bruni, Cyril Cohen, Pierre Roux, Takafumi Saikawa.

_Formalizing Concentration Inequalities in Rocq: Infrastructure and Automation_.

ITP 2025. [[https://drops.dagstuhl.de/storage/00lipics/lipics-vol352-itp2025/LIPIcs.ITP.2025.21/LIPIcs.ITP.2025.21.pdf][pdf]]

- Quentin Vermande. _Décomposition Algébrique Cylindrique en Coq/Rocq_.

36es Journées Francophones des Langages Applicatifs (JFLA 2025). [[https://inria.hal.science/hal-04859512/file/jfla2025-final84.pdf][pdf]]

- Reynald Affeldt.

_Prouver que π est irrationnel avec MathComp-Analysis_.

36es Journées Francophones des Langages Applicatifs (JFLA 2025). [[https://hal.science/hal-04859455v1/document][pdf]]

- Florent Hivert.

_Machine Checked Proofs and Programs in Algebraic Combinatorics_.

CPP 2025. [[https://arxiv.org/pdf/2412.04864][pdf]]

- Reynald Affeldt, Zachary Stone.

_A Comprehensive Overview of the Lebesgue Differentiation Theorem in Coq_.

ITP 2024. [[https://drops.dagstuhl.de/storage/00lipics/lipics-vol309-itp2024/LIPIcs.ITP.2024.5/LIPIcs.ITP.2024.5.pdf][pdf]]

- Assia Mahboubi, Matthieu Piquerez.

_A First Order Theory of Diagram Chasing_.

32nd EACSL Annual Conference on Computer Science Logic (CSL 2024). [[https://drops.dagstuhl.de/storage/00lipics/lipics-vol288-csl2024/LIPIcs.CSL.2024.38/LIPIcs.CSL.2024.38.pdf][pdf]]

- Benoît Guillemet, Assia Mahboubi, Matthieu Piquerez.

_Machine-Checked Categorical Diagrammatic Reasoning_.

FSCD 2024. [[https://drops.dagstuhl.de/storage/00lipics/lipics-vol299-fscd2024/LIPIcs.FSCD.2024.7/LIPIcs.FSCD.2024.7.pdf][pdf]]

- Yoshihiro Ishiguro, Reynald Affeldt.

_The Radon-Nikodým Theorem and the Lebesgue-Stieltjes Measure in Coq_.

Computer Software 41(2), 2024. [[https://www.jstage.jst.go.jp/article/jssst/41/2/41_2_41/_pdf/-char/en][pdf]]

- Reynald Affeldt, Cyril Cohen.

_Measure construction by extension in dependent type theory with application to integration_.

JAR 2023. [[https://arxiv.org/pdf/2209.02345.pdf][pdf]]

- Pierre Pomeret-Coquot, Helene Fargier, Érik Martin-Dorel.

_Bel-Games: A Formal Theory of Games of Incomplete Information Based on Belief Functions in the Coq Proof Assistant_.

ITP 2023. [[https://drops.dagstuhl.de/opus/volltexte/2023/18400/pdf/LIPIcs-ITP-2023-25.pdf][pdf]]

- Xavier Allamigeon, Quentin Canu, Pierre-Yves Strub.

_A Formal Disproof of Hirsch Conjecture_.

CPP 2023. [[https://arxiv.org/pdf/2301.04060.pdf][pdf]]

- Xavier Allamigeon, Ricardo D. Katz, Pierre-Yves Strub.

_Formalizing the Face Lattice of Polyhedra_.

LMCS 18(2), 2022. [[https://lmcs.episciences.org/9570/pdf][pdf]]

- Assia Mahboubi, Thomas Sibut-Pinote.

_A Formal Proof of the Irrationality of ζ(3)_.

LMCS 17(1), 2021. [[https://lmcs.episciences.org/7193/pdf][pdf]]

- Sophie Bernard, Cyril Cohen, Assia Mahboubi, Pierre-Yves Strub.

_Unsolvability of the Quintic Formalized in Dependent Type Theory_

ITP 2021. [[https://hal.inria.fr/hal-03136002v3/document][pdf]]

- Xavier Allamigeon, Ricardo D. Katz, Pierre-Yves Strub.

_Formalizing the Face Lattice of Polyhedra_.

IJCAR 2020. [[https://dx.doi.org/10.1007%2F978-3-030-51054-1_11][doi]]

- Reynald Affeldt, Cyril Cohen, Marie Kerjean, Assia Mahboubi, Damien Rouhling, Kazuhiko Sakaguchi.

_Competing inheritance paths in dependent type theory: a case study in functional analysis_.

IJCAR 2020. [[https://hal.inria.fr/hal-02463336v2/document][pdf]], [[https://math-comp.github.io/competing-inheritance-paths-in-dependent-type-theory/][code]]

- Xavier Allamigeon, Ricardo D. Katz.

_A Formalization of Convex Polyhedra Based on the Simplex Method_.

JAR 63(2), 2019. [[https://doi.org/10.1007/s10817-018-9477-1][doi]]

- Florent Bréhard, Assia Mahboubi, Damien Pous. _A certificate-based

approach to formally verified approximations_. ITP 2019. [[https://hal.laas.fr/hal-02088529v2/document][pdf]]

- Reynald Affeldt, Cyril Cohen, Damien Rouhling.

_Formalization techniques for asymptotic reasoning in classical analysis_.

Journal of Formalized Reasoning 11(1), 2018. [[https://jfr.unibo.it/article/view/8124/8407][pdf]]

- Reynald Affeldt, Cyril Cohen, Assia Mahboubi, Damien Rouhling, Pierre-Yves Strub.

_Classical Analysis with Coq_. Coq Workshop 2018. [[https://staff.aist.go.jp/reynald.affeldt/documents/coqws-reals.pdf][pdf]]

- Xavier Allamigeon, Ricardo D. Katz.

_A formalization of convex polyhedra based on the simplex method_. ITP 2017. [[https://arxiv.org/pdf/1706.10269.pdf][pdf]]

- Evmorfia-Iro Bartzia.

_A Formalization of Elliptic Curves for Cryptography_.

PhD thesis, Université Paris-Saclay, 2017. [[https://pastel.archives-ouvertes.fr/tel-01563979/document][pdf]]

- Guillaume Cano, Cyril Cohen, Maxime Dénès, Anders Mörtberg, Vincent Siles.

_Formalized linear algebra over Elementary Divisor Rings in Coq_.

LMCS 12(2), 2016. [[https://hal.inria.fr/hal-01081908/document][pdf]]

- Cyril Cohen, Boris Djalal.

_Formalization of a newton series representation of polynomials_. CPP 2016. [[https://hal.inria.fr/hal-01240469/document][pdf]]

- Ken'ichi Kuga, Manabu Hagiwara, Mitsuharu Yamamoto.

_Formalization of Bing's Shrinking Method in Geometric Topology_. CICM 2016. [[https://doi.org/10.1007/978-3-319-42547-4_2][doi]]

- Gallego Arias, Emilio Jesús, Pierre Jouvelot.

_Adventures in the (not so) Complex Space_. Coq Workshop 2015. [[https://github.com/ejgallego/mini-dft-coq][paper, code, slides]]

- Frédéric Chyzak, Assia Mahboubi, Thomas Sibut-Pinote, Enrico Tassi.

_A Computer-Algebra-Based Formal Proof of the Irrationality of ζ(3)_. ITP 2014. [[https://hal.inria.fr/hal-00984057/document][pdf]]

- Cyril Cohen, Anders Mörtberg.

_A Coq Formalization of Finitely Presented Modules_. ITP 2014. [[https://perso.crans.org/cohen/papers/fpmods.pdf][pdf]]

- Anders Mörtberg.

_Formalizing Refinements and Constructive Algebra in Type Theory_.

PhD, University of Gothenburg, 2014. [[http://staff.math.su.se/anders.mortberg/thesis/thesis.pdf][pdf]]

- Evmorfia-Iro Bartzia, Pierre-Yves Strub.

_A Formal Library for Elliptic Curves in the Coq Proof Assistant_. ITP 2014. [[https://hal.inria.fr/hal-01102288/file/A-Formal-Library-for-Elliptic-Curves-in-the-Coq-Proof-Assistant.pdf][pdf]]

- Jónathan Heras, Thierry Coquand, Anders Mörtberg, Vincent Siles.

_Computing persistent homology within Coq/SSReflect_. ACM Transactions on Computational Logic 14(4), 2013. [[https://arxiv.org/pdf/1209.1905.pdf][pdf]]

- 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.

_A Machine-Checked Proof of the Odd Order Theorem_. ITP 2013. [[https://hal.inria.fr/hal-00816699/document][pdf]]

- Cyril Cohen. _Pragmatic Quotient Types in Coq_. ITP 2013. [[https://hal.inria.fr/hal-01966714/document][pdf]]

- Assia Mahboubi. _The Rooster and the Butterflies_. CICM 2013. [[https://hal.inria.fr/hal-00825074v3/document][pdf]]

- Maxime Dénès, Anders Mörtberg, Vincent Siles.

_A Refinement-Based Approach to Computational Algebra in Coq_. ITP 2012. [[https://hal.inria.fr/hal-00734505/document][pdf]]

- Jónathan Heras, Maxime Dénès, Gadea Mata, Anders Mörtberg, María Poza, Vincent Siles.

_Towards a Certified Computation of Homology Groups for Digital Images_.

4th International Workshop on Computational Topology in Image Context (CTIC 2012). [[https://hal.inria.fr/hal-00711385/document][pdf]]

- Assia Mahboubi, Cyril Cohen.

_Formal proofs in real algebraic geometry: from ordered fields to quantifier elimination_.

LMCS 8(1), 2012. [[https://hal.inria.fr/inria-00593738v4/document][pdf]]

- Thierry Coquand, Anders Mörtberg, Vincent Siles.

_Coherent and Strongly Discrete Rings in Type Theory_. CPP 2012. [[https://staff.math.su.se/anders.mortberg/papers/coherent.pdf][pdf]]

- Cyril Cohen.

_Formalized algebraic numbers: construction and first-order theory_.

PhD thesis, Ecole Polytechnique, 2012. [[https://pastel.archives-ouvertes.fr/pastel-00780446/file/main.pdf][pdf]]

- Jónathan Heras, María Poza, Maxime Dénès, Laurence Rideau.

_Incidence Simplicial Matrices Formalized in Coq/SSReflect_.

18th Symposium on Symposium on the Integration of Symbolic Computation and Mechanized Reasoning (Calculemus 2011). [[https://hal.inria.fr/inria-00603208/file/ismfis.pdf][pdf]]

- Georges Gonthier.

_Point-Free, Set-Free Concrete Linear Algebra_.

ITP 2011. [[https://hal.inria.fr/hal-00805966/document][pdf]]

- Sidi Ould Biha.

_Finite groups representation theory with Coq_.

8th International Conference on Mathematical Knowledge Management (MKM 2009). [[https://hal.inria.fr/inria-00377431/document][pdf]]

- Yves Bertot, Georges Gonthier, Sidi Ould Biha, Ioana Pasca.

_Canonical Big Operators_.

ITP 2008. [[https://hal.inria.fr/inria-00331193/document][pdf]]

- Georges Gonthier, Assia Mahboubi, Laurence Rideau, Enrico Tassi, Laurent Théry.

_A Modular Formalisation of Finite Group Theory_.

TPHOLs 2007. [[https://hal.inria.fr/inria-00139131v2/document][pdf]]

- Laurent Théry, Laurence Rideau. _Formalising Sylow’s theorems in Coq_.

RT-0327 INRIA 2006. [[https://hal.inria.fr/inria-00113750v2/document][pdf]]

** Graph Theory

- Christian Doczkal.

_A Variant of Wagner’s Theorem Based on Combinatorial Hypermaps_.

ITP 2021. [[https://hal.archives-ouvertes.fr/hal-03142192/document][pdf]]

- Christian Doczkal, Damien Pous.

_Graph Theory in Coq: Minors, Treewidth, and Isomorphisms_.

JAR (special issue for ITP 2018), 2020. [[https://hal.archives-ouvertes.fr/hal-02316859/document][pdf]]

- Christian Doczkal, Damien Pous.

_Completeness of an axiomatization of graph isomorphism via graph rewriting in Coq_.

CPP 2020. [[https://hal.archives-ouvertes.fr/hal-02333553/document][pdf]]

- Daniel E. Severín.

_Formalization of the Domination Chain with Weighted Parameters_. ITP 2019. [[http://drops.dagstuhl.de/opus/volltexte/2019/11091/pdf/LIPIcs-ITP-2019-36.pdf][pdf]]

- Christian Doczkal, Guillaume Combette, Damien Pous.

_A Formal Proof of the Minor-Exclusion Property for Treewidth-Two Graphs_. ITP 2018. [[https://hal.archives-ouvertes.fr/hal-01703922/document][pdf]]

- George Gonthier.

_A computer-checked proof of the Four Colour Theorem_.

[[http://www2.tcs.ifi.lmu.de/~abel/lehre/WS07-08/CAFR/4colproof.pdf][pdf]]

** Robotics

- Yves Bertot, Thomas Portet. _Formally Verifying a Vertical Cell Decomposition Algorithm_.

ITP 2025. [[https://drops.dagstuhl.de/storage/00lipics/lipics-vol352-itp2025/LIPIcs.ITP.2025.24/LIPIcs.ITP.2025.24.pdf][pdf]]

- Yves Bertot. _Safe Smooth Paths Between Straight Line Obstacles_.

Logics and Type Systems in Theory and Practice, LNCS 14560, 2024.

[[https://doi.org/10.1007/978-3-031-61716-4][doi]], [[https://inria.hal.science/hal-04312815][pdf]]

- Cyril Cohen, Damien Rouhling.

_A Formal Proof in Coq of LaSalle's Invariance Principle_. ITP 2017. [[https://hal.inria.fr/hal-01612293/document][pdf]]

- Reynald Affeldt, Cyril Cohen.

_Formal Foundations of 3D Geometry to Model Robot Manipulators_. CPP 2017. [[https://hal.inria.fr/hal-01414753/document][pdf]]

* Programming and Algorithms

- Assia Mahboubi, Guillaume Melquiond, Pierre-Yves Strub, Tomás Vallejos Paradas.

_Functional correctness of an optimized modular inversion algorithm_. ITP 2026. [[https://hal.science/hal-05554365v1/document][pdf]]

- Reynald Affeldt, Jacques Garrigue, Takafumi Saikawa.

_A practical formalization of monadic equational reasoning in dependent-type theory_.

JFP 35(e1). [[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]]

- Cyril Cohen, Kazuhiko Sakaguchi.

_A bargain for mergesorts -- How to prove your mergesort correct and stable, almost for free_.

ICFP 2025. [[https://arxiv.org/pdf/2403.08173][pdf]]

- Ana de Almeida Borges, Mireia González Bedmar, Juan Conejero Rodríguez, Eduardo Hermo Reyes, Joaquim Casals Buñuel, Joost J. Joosten.

_UTC time, formally verified_.

CPP 2024. [[https://arxiv.org/pdf/2209.14227.pdf][pdf]]

- Philipp G. Haselwarter, Exequiel Rivas, Antoine Van Muylder, Théo Winterhalter,

Carmine Abate, Nikolaj Sidorenco, Cătălin Hriţcu, Kenji Maillard, Bas Spitters.

_SSProve: A Foundational Framework for Modular Cryptographic Proofs in Coq_.

ACM Transactions on Programming Languages and Systems 45(3), 2023. [[https://dl.acm.org/doi/pdf/10.1145/3594735][pdf]]

- Ming-Hsien Tsai, Yu-Fu Fu, Jiaxiang Liu, Xiaomu Shi, Bow-Yaw Wang, Bo-Yin Yang.

_CoqCryptoLine: A Verified Model Checker with Certified Results_.

Conference on Computer-Aided Verification (CAV 2023). [[https://link.springer.com/chapter/10.1007/978-3-031-37703-7_11][doi]]

- Ayumu Saito, Reynald Affeldt.

_Towards a Practical Library for Monadic Equational Reasoning in Coq_.

Mathematics of Program Construction (MPC 2022). [[https://staff.aist.go.jp/reynald.affeldt/documents/monae-mpc2022.pdf][pdf]]

- Reynald Affeldt, David Nowak.

_Extending equational monadic reasoning with monad transformers_.

TYPES 2020. [[https://arxiv.org/pdf/2011.03463.pdf][pdf]]

- Reynald Affeldt, David Nowak, Takafumi Saikawa.

_A Hierarchy of Monadic Effects for Program Verification Using Equational Reasoning_.

Mathematics of Program Construction (MPC 2019)

- Ran Chen, Cyril Cohen, Jean-Jacques Levy, Stephan Merz, Laurent Thery.

_Formal Proof of Tarjan’s Strongly Connected Components Algorithm in Why3, Coq, and Isabelle_.

ITP 2019. [[http://drops.dagstuhl.de/opus/volltexte/2019/11068/pdf/LIPIcs-ITP-2019-13.pdf][pdf]]

- Reynald Affeldt, Jacques Garrigue, Xuanrui Qi, Kazunari Tanaka.

_Proving tree algorithms for succinct data structures_.

ITP 2019. [[https://arxiv.org/pdf/1904.02809.pdf][pdf]]

- Reynald Affeldt, Jacques Garrigue, Xuanrui Qi, Kazunari Tanaka.

_Experience Report: Type-Driven Development of Certified Tree Algorithms in Coq_.

Coq Workshop 2019. [[https://staff.aist.go.jp/reynald.affeldt/coq2019/coqws2019-affeldt-garrigue-qi-tanaka.pdf][pdf]]

- Cyril Cohen, Damien Rouhling.

_A refinement-based approach to large scale reflection for algebra_.

28ème Journées Francophones des Langages Applicatifs (JFLA 2017). [[https://hal.inria.fr/hal-01414881/document][pdf]]

- Timmy Weerwag.

_Verifying an elliptic curve cryptographic algorithm using Coq and the Ssreflect extension_.

Master’s thesis, Mathematics, Radboud University, 2016. [[https://www.ru.nl/publish/pages/813286/weerwag_timmy_-1a.pdf][pdf]]

- Beta Ziliani, Derek Dreyer, Neelakantan R. Krishnaswami, Aleksandar Nanevski, Viktor Vafeiadis.

_Mtac: A Monad for Typed Tactic Programming in Coq_. JFP 25, 2015. [[https://people.mpi-sws.org/~dreyer/papers/mtac/journal.pdf][pdf]]

- Cyril Cohen, Maxime Dénès, Anders Mörtberg.

_Refinements for free!_. CPP 2013. [[https://hal.inria.fr/hal-01113453/document][pdf]]

- Andrew Kennedy, Nick Benton, Jonas B. Jensen, Pierre-Evariste Dagand.

_Coq: the world's best macro assembler?_ PPDP 2013. [[http://nickbenton.name/coqasm.pdf][pdf]]

- Germán Andrés Delbianco, Aleksandar Nanevski.

_Hoare-Style Reasoning with (Algebraic) Continuations_. ICFP 2013. [[https://doi.org/10.1145/2544174.2500593][doi]]

- Beta Ziliani, Derek Dreyer, Neelakantan R. Krishnaswami, Aleksandar Nanevski, Viktor Vafeiadis.

_Mtac: A Monad for Typed Tactic Programming in Coq_. ICFP 2013. [[https://doi.org/10.1017/S0956796815000118][doi]]

- Aleksandar Nanevski, Viktor Vafeiadis, Josh Berdine.

_Structuring the Verification of Heap-Manipulating Programs_. POPL 2010. [[https://doi.org/10.1145/1706299.1706331][doi]]

** Concurrency

- Mohit Tekriwal, Avi Tachna-Fram, Jean-Baptiste Jeannin, Manos Kapritsos, Dimitra Panagou.

_Formally verified asymptotic consensus in robust networks_.

TACAS 2024. [[https://arxiv.org/pdf/2202.13833.pdf][pdf]]

- Søren Eller Thomsen, Bas Spitters.

_Formalizing Nakamoto-Style Proof of Stake_.

34th IEEE Computer Security Foundations Symposium (CSF 2021). [[https://arxiv.org/pdf/2007.12105][pdf]]

- Musab A. Alturki, Jing Chen, Victor Luchangco, Brandon Moore, Karl Palmskog, Lucas Peña, Grigore Roşu.

_Towards a Verified Model of the Algorand Consensus Protocol in Coq_.

1st Workshop on Formal Methods for Blockchains (FMBC 2019). [[https://arxiv.org/pdf/1907.05523][pdf]]

- Joseph Tassarotti, Robert Harper.

_A Separation Logic for Concurrent Randomized Programs_.

POPL 2019. [[http://www.cs.bc.edu/~tassarot/papers/iris-prob-paper/paper.pdf][pdf]]

- Ilya Sergey, James R. Wilcox, Zachary Tatlock.

_Programming and Proving with Distributed Protocols_. POPL 2018. [[https://dl.acm.org/citation.cfm?doid=3177123.3158116][pdf]]

- George Pîrlea, Ilya Sergey. _Mechanising Blockchain Consensus_. CPP 2018. [[https://dl.acm.org/citation.cfm?id=3167086][pdf]]

- Germán Andrés Delbianco, Ilya Sergey, Aleksandar Nanevski, Anindya Banerjee.

_Concurrent Data Structures Linked in Time_.

European Conference on Object-Oriented Programming (ECOOP 2017). [[https://drops.dagstuhl.de/opus/volltexte/2017/7255/pdf/LIPIcs-ECOOP-2017-8.pdf][pdf]]

- Mitsuharu Yamamoto, Shogo Sekine, Saki Matsumoto.

_Formalization of Karp-Miller Tree Construction on Petri Nets_. CPP 2017. [[https://doi.org/10.1145/3018610.3018626][doi]]

- Germán Andrés Delbianco.

_Hoare-style Reasoning with Higher-order Control: Continuations and Concurrency_.

PhD thesis, Computer Science, Universidad Politécnica de Madrid, 2017. [[http://oa.upm.es/47796/1/GERMAN_ANDRES_DELBIANCO.pdf][pdf]]

- Ralf Jung, Robbert Krebbers, Lars Birkedal, Derek Dreyer.

_Higher-Order Ghost State_.

ICFP 2016. [[https://dl.acm.org/doi/pdf/10.1145/2951913.2951943][pdf]]

- Ilya Sergey, Aleksandar Nanevski, Anindya Banerjee, Germán Andrés Delbianco.

_Hoare-style Specifications as Correctness Conditions for Non-linearizable Concurrent Objects_.

Object-oriented Programming, Systems, Languages, and Applications (OOPSLA 2016). [[https://arxiv.org/pdf/1509.06220.pdf][pdf]]

- Ilya Sergey, Aleksandar Nanevski, Anindya Banerjee.

_Mechanized Verification of Fine-grained Concurrent Programs_.

Programming Language Design and Implementation (PLDI 2015). [[https://doi.org/10.1145/2737924.2737964][doi]]

- Ilya Sergey, Aleksandar Nanevski, Anindya Banerjee.

_Specifying and Verifying Concurrent Algorithms with Histories and Subjectivity_.

ESOP 2015. [[https://arxiv.org/pdf/1410.0306.pdf][pdf]]

- Aleksandar Nanevski, Ruy Ley-Wild, Ilya Sergey, Germán Andrés Delbianco.

_Communicating State Transition Systems for Fine-Grained Concurrent Resources_.

ESOP 2014. [[https://doi.org/10.1007/978-3-642-54833-8_16][doi]]

- Ruy Ley-Wild, Aleksandar Nanevski.

_Subjective Auxiliary State for Coarse-Grained Concurrency_. POPL 2013. [[https://doi.org/10.1145/2429069.2429134][doi]]

** Information Flow

- Aleksandar Nanevski, Anindya Banerjee, Deepak Garg.

_Dependent Type Theory for Verification of Information Flow and Access Control Policies_.

ACM Transactions on Programming Languages and Systems, 35(2):6:1-6:41, 2013. [[https://doi.org/10.1145/2491522.2491523][doi]]

- Gordon Stewart, Anindya Banerjee, Aleksandar Nanevski.

_Dependent Types for Enforcement of Information Flow and Erasure Policies in Heterogeneous Data Structures_.

PPDP 2013. [[https://doi.org/10.1145/2505879.2505895][doi]]

- Aleksandar Nanevski, Anindya Banerjee, Deepak Garg.

_Verification of Information Flow and Access Control Policies with Dependent Types_.

2011 IEEE Symposium on Security and Privacy. [[https://ieeexplore.ieee.org/document/5958028][IEEE Xplore]]

** Probabilistic Reasoning

- Reynald Affeldt, Yoshihiro Ishiguro, Zachary Stone.

_A Formal Foundation for Equational Reasoning on Probabilistic Programs_.

Asian Symposium on Programming Languages and Systems (APLAS 2025). [[https://doi.org/10.1007/978-981-95-3585-9_3][doi]]

- Reynald Affeldt, Cyril Cohen, Ayumu Saito.

_Semantics of Probabilistic Programs Using s-Finite Kernels in Dependent Type Theory_.

ACM Transactions on Probabilistic Machine Learning 1(3), 2025. [[https://dl.acm.org/doi/pdf/10.1145/3732291][pdf]]

- Reynald Affeldt, Clark Barrett, Alessandro Bruni, Ieva Daukantas, Harun Khan, Takafumi Saikawa, Carsten Schürmann.

_Robust Mean Estimation by All Means (short paper)_.

ITP 2024. [[https://drops.dagstuhl.de/storage/00lipics/lipics-vol309-itp2024/LIPIcs.ITP.2024.39/LIPIcs.ITP.2024.39.pdf][pdf]]

- Filip Markovic, Pierre Roux, Sergey Bozhko, Alessandro V. Papadopoulos, Björn B. Brandenburg.

_CTA: A Correlation-Tolerant Analysis of the Deadline-Failure Probability of Dependent Tasks_.

IEEE Real-Time Systems Symposium (RTSS 2023). [[https://people.mpi-sws.org/~bbb/papers/pdf/rtss23-CTA.pdf][pdf]]

- Ayumu Saito, Reynald Affeldt.

_Experimenting with an Intrinsically-Typed Probabilistic Programming Language in Coq_.

Asian Symposium on Programming Languages and Systems (APLAS 2023). [[https://link.springer.com/chapter/10.1007/978-981-99-8311-7_9][doi]]

- Reynald Affeldt, Cyril Cohen, Ayumu Saito.

_Semantics of Probabilistic Programs using s-Finite Kernels in Coq_.

CPP 2023. [[https://hal.inria.fr/hal-03917948/document][pdf]]

- Ieva Daukantas, Alessandro Bruni, Carsten Schürmann.

_Trimming Data Sets: a Verified Algorithm for Robust Mean Estimation_.

PPDP 2021. [[https://doi.org/10.1145/3479394.3479412][doi]]

- Reynald Affeldt, Jacques Garrigue, David Nowak, Takafumi Saikawa.

_A trustful monad for axiomatic reasoning with probability and nondeterminism_.

JFP 31(E17), 2021. [[https://arxiv.org/pdf/2003.09993.pdf][pdf]]

- Kiran Gopinathan, Ilya Sergey.

_Certifying Certainty and Uncertainty in Approximate Membership Query Structures_.

32nd International Conference on Computer-Aided Verification (CAV 2020). [[https://arxiv.org/pdf/2004.13312.pdf][pdf]]

- Reynald Affeldt, Jacques Garrigue, Takafumi Saikawa.

_Formal adventures in convex and conical spaces_.

CICM 2020. [[https://arxiv.org/pdf/2004.12713.pdf][pdf]]

- Reynald Affeldt, Jacques Garrigue, Takafumi Saikawa.

_Reasoning with conditional probabilities and joint distributions_.

Computer Software 37(3):79-95, 2020. [[https://staff.aist.go.jp/reynald.affeldt/documents/cproba_preprint.pdf][pdf]]

- Joseph Tassarotti, Robert Harper.

_Verified Tail Bounds for Randomized Programs_. ITP 2018. [[https://www.cs.cmu.edu/~rwh/papers/tail-bounds/paper.pdf][pdf]]

** Quantum Computing

- Jacques Garrigue, Takafumi Saikawa.

_Typed Compositional Quantum Computation with Lenses_.

JAR 70(10). [[https://link.springer.com/article/10.1007/s10817-026-09750-3][pdf]]

- Yingte Xu, Gilles Barthe, Li Zhou.

_Automating Equational Proofs in Dirac Notation_.

POPL 2025. [[https://arxiv.org/pdf/2411.11617][pdf]]

- Jacques Garrigue and Takafumi Saikawa.

_Typed compositional quantum computation with lenses_.

ITP 2024. [[https://drops.dagstuhl.de/storage/00lipics/lipics-vol309-itp2024/LIPIcs.ITP.2024.15/LIPIcs.ITP.2024.15.pdf][pdf]]

- Li Zhou, Gilles Barthe, Pierre-Yves Strub, Junyi Liu, Mingsheng Ying.

_CoqQ: Foundational Verification of Quantum Programs_.

POPL 2023. [[https://arxiv.org/pdf/2207.11350.pdf][pdf]]

* Other Applications

- Pierre-Léo Bégay, Pierre Crégut, Jean-François Monin.

_Developing and certifying Datalog optimizations in Coq/MathComp_. CPP 2021. [[https://hal.archives-ouvertes.fr/hal-03065304v1/document][pdf]]

- Gallego Arias, Emilio Jesús, Olivier Hermant, Pierre Jouvelot.

_A Taste of Sound Reasoning in Faust_.

Linux Audio Conference 2015. [[https://github.com/ejgallego/mini-faust-coq][paper, code, slides]]

- Maxime Dénès, Benjamin Lesage, Yves Bertot, Adrien Richard.

_Formal proof of theorems on genetic regulatory networks_.

11th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing (SYNACS 2009).

[[https://ieeexplore.ieee.org/document/5460865][IEEE Xplore]]

** Logic, Types, and Verification

- Jan Bessai, Jakob Rehof, Boris Düdder.

_Fast Verified BCD Subtyping_.

Models, Mindsets, Meta: The What, the How, and the Why Not? LNCS 11200, 2019. [[https://doi.org/10.1007/978-3-030-22348-9_21][doi]]

- Christian Doczkal, Gert Smolka.

_Regular Language Representations in the Constructive Type Theory of Coq_.

JAR 61, 2018. [[https://hal.archives-ouvertes.fr/hal-01832031/document][pdf]]

- Christian Doczkal, Joachim Bard.

_Completeness and Decidability of Converse PDL in the Constructive Type Theory of Coq_.

CPP 2018. [[https://hal.archives-ouvertes.fr/hal-01646782/document][pdf]]

- Angela Bonifati, Stefania Dumbrava, Emilio Jesús Gallego Arias.

_Certified Graph View Maintenance with Regular Datalog_.

34th International Conference on Logic Programming (ICLP 2018). [[https://hal.archives-ouvertes.fr/hal-01932818/document][pdf]]

- Véronique Benzaken, Evelyne Contejean, Stefania Dumbrava.

_Certifying Standard and Stratified Datalog Inference Engines in SSReflect_. ITP 2017. [[https://hal.archives-ouvertes.fr/hal-01745566/file/ITP2017.pdf][pdf]]

- Felipe Cerqueira, Felix Stutz, Björn Brandenburg.

_Prosa: A Case for Readable Mechanized Schedulability Analysis_.

28th Euromicro Conference on Real-Time Systems (ECRTS 2016). [[https://ieeexplore.ieee.org/document/7557887][IEEE Xplore]]

- Christian Doczkal, Gert Smolka.

_Completeness and Decidability Results for CTL in Constructive Type Theory_.

JAR 56, 2016. [[https://doi.org/10.1007/s10817-016-9361-9][doi]]

- Christian Doczkal, Gert Smolka.

_Completeness and Decidability Results for CTL in Coq_. ITP 2014. [[https://www.ps.uni-saarland.de/Publications/documents/DoczkalSmolka_2014_comp-dec-CTL.pdf][pdf]]

- Christian Doczkal, Gert Smolka.

_Constructive Completeness for Modal Logic with Transitive Closure_. CPP 2012. [[https://doi.org/10.1007/978-3-642-35308-6_18][doi]]

- Christian Doczkal, Gert Smolka.

_Constructive Formalization of Hybrid Logic with Eventualities_. CPP 2011. [[https://www.ps.uni-saarland.de/Publications/documents/DoczkalSmolka_2011_Constructive_0.pdf][pdf]]

- Thierry Coquand, Vincent Siles.

_A Decision Procedure for Regular Expression Equivalence in Type Theory_. CPP 2011. [[https://doi.org/10.1007/978-3-642-25379-9_11][doi]]

- Kasper Svendsen, Lars Birkedal, Aleksandar Nanevski.

_Partiality, State and Dependent Types_.

International Conference on Typed Lambda Calculi and Applications (TLCA 2011). [[https://doi.org/10.1007/978-3-642-21691-6_17][doi]]

** Information Theory

- Joshua M. Cohen, Qinshi Wang, Andrew W. Appel.

_Verified Erasure Correction in Coq with MathComp and VST_.

34th International Conference on Computer-Aided Verification (CAV 2022). [[https://www.cs.princeton.edu/~appel/papers/FECVerification.pdf][pdf]]

- Reynald Affeldt, Jacques Garrigue, Takafumi Saikawa.

_A library for formalization of linear error-correcting codes_.

JAR 64:1123-1164, 2020. [[https://staff.aist.go.jp/reynald.affeldt/documents/ecc.pdf][pdf]]

- Kyosuke Nakano, Manabu Hagiwara.

_Formalization of binary symmetric erasure channel based on infotheo_.

International Symposium on Information Theory and its Application 2016 (ISITA 2016).

[[https://ieeexplore.ieee.org/document/7840477][IEEE Xplore]]

- Reynald Affeldt, Jacques Garrigue, Takafumi Saikawa.

_Formalization of Reed-Solomon codes and progress report on formalization of LDPC codes_.

International Symposium on Information Theory and its Application 2016 (ISITA 2016)

- Reynald Affeldt, Jacques Garrigue.

_Formalization of error-correcting codes: from Hamming to modern coding theory_. ITP 2015. [[https://staff.aist.go.jp/reynald.affeldt/documents/eccITP2015_authorsversion.pdf][pdf]]

- Ryosuke Obi, Manabu Hagiwara, Reynald Affeldt.

_Formalization of the variable-length source coding theorem: Direct part_.

International Symposium on Information Theory and its Application 2014 (ISITA 2014). [[https://ieeexplore.ieee.org/document/6979832][IEEE Xplore]]

- Reynald Affeldt, Manabu Hagiwara, Jonas Sénizergues.

_Formalization of Shannon's theorems_. JAR 53(1), 2014. [[https://staff.aist.go.jp/reynald.affeldt/documents/shannon_theorems.pdf][pdf]]

- Reynald Affeldt, Manabu Hagiwara.

_Formalization of Shannon's Theorems in SSReflect-Coq_. ITP 2012. [[https://staff.aist.go.jp/reynald.affeldt/documents/affeldt-itp2012-preprint.pdf][pdf]]

* Tooling

- Cyril Cohen, Enzo Crance, Assia Mahboubi.

_Trocq: Proof Transfer for Free, With or Without Univalence_.

ESOP 2024. [[https://arxiv.org/pdf/2310.14022][pdf]]

- Xavier Allamigeon, Quentin Canu, Cyril Cohen, Kazuhiko Sakaguchi, Pierre-Yves Strub.

_Design patterns of hierarchies for order structures_.

HAL 2023. [[https://inria.hal.science/hal-04008820/document][pdf]]

- Valentin Blot, Denis Cousineau, Enzo Crance, Louise Dubois de Prisque, Chantal Keller, Assia Mahboubi, Pierre Vial.

_Compositional Pre-processing for Automated Reasoning in Dependent Type Theory_.

CPP 2023. [[https://arxiv.org/pdf/2204.02643.pdf][pdf]]

- Benjamin Grégoire, Jean-Christophe Léchenet, Enrico Tassi.

_Practical and sound equality tests, automatically_.

CPP 2023. [[https://hal.inria.fr/hal-03800154/document][pdf]]

- Kazuhiko Sakaguchi. _Reflexive tactics for algebra, revisited_. ITP 2022. [[https://arxiv.org/pdf/2202.04330.pdf][pdf]]

- Reynald Affeldt, Xavier Allamigeon, Yves Bertot, Quentin Canu, Cyril Cohen, Pierre Roux, Kazuhiko Sakaguchi, Enrico Tassi, Laurent Théry, Anton Trunov.

_Porting the Mathematical Components library to Hierarchy Builder_. Coq Workshop 2021. [[https://coq-workshop.gitlab.io/2021/abstracts/Coq2021-01-02-mathcomp-hierarchy-builder.pdf][pdf]]

- Pierre-Léo Bégay, Pierre Crégut, Jean-Francois Monin.

_Developing sequence and tree fintypes in MathComp_. Coq Workshop 2020. [[https://coq-workshop.gitlab.io/2020/abstracts/Coq2020_03-03-seq-fintype.pdf][pdf]]

- Xavier Allamigeon, Cyril Cohen, Kazuhiko Sakaguchi, Pierre-Yves Strub.

_A hierarchy of ordered types in Mathematical Components_. Coq Workshop 2020. [[https://coq-workshop.gitlab.io/2020/abstracts/Coq2020_03-02-ordered.pdf][pdf]]

- Cyril Cohen, Kazuhiko Sakaguchi, Enrico Tassi.

_Hierarchy Builder: algebraic hierarchies made easy in Coq with Elpi_.

FSCD 2020. [[https://hal.inria.fr/hal-02478907v4/document][pdf]]

- Karl Palmskog, Ahmet Celik, Milos Gligoric.

_Practical Machine-Checked Formalization of Change Impact Analysis_.

TACAS 2020. [[https://users.ece.utexas.edu/~gligoric/papers/PalmskogETAL20Chip.pdf][pdf]]

- Kazuhiko Sakaguchi. _Validating Mathematical Structures_. IJCAR 2020. [[https://arxiv.org/pdf/2002.00620.pdf][pdf]]

- Kazuhiko Sakaguchi. _Program extraction for mutable arrays_. Science of Computer Programming 191, 2020. [[https://doi.org/10.1016/j.scico.2019.102372][doi]]

- Erik Martin-Dorel, Enrico Tassi. _SSReflect in Coq 8.10_. Coq Workshop 2019. [[https://staff.aist.go.jp/reynald.affeldt/coq2019/coqws2019-martindorel-tassi.pdf][pdf]]

- Kazuhiko Sakaguchi. _Program Extraction for Mutable Arrays_.

15th International Symposium on Functional and Logic Programming (FLOPS 2018). [[https://doi.org/10.1007/978-3-319-90686-7_4][doi]]

- Kazuhiko Sakaguchi, Yukiyoshi Kameyama.

_Efficient Finite-Domain Function Library for the Coq Proof Assistant_.

IPSJ Transactions on Programming 10(1), 2017. [[http://logic.cs.tsukuba.ac.jp/~sakaguchi/papers/ipsj-pro-2016-1-7.pdf][pdf (long, in Japanese)]], [[http://logic.cs.tsukuba.ac.jp/~sakaguchi/papers/ipsj-pro-2016-1-7.en.pdf][pdf (short, in English)]]

- Georges Gonthier, Beta Ziliani, Aleksandar Nanevski, Derek Dreyer.

_How to make ad hoc proof automation less ad hoc_. JFP 23(4), 2013. [[https://doi.org/10.1017/S0956796813000051][doi]]

- Vladimir Komendantsky, Alexander Konovalov, Steve Linton.

_Interfacing Coq + SSReflect with GAP_. Electronic Notes in Theoretical Computer Science 285, 2012. [[https://www.sciencedirect.com/science/article/pii/S1571066112000230][pdf]]

- Iain Whiteside, David Aspinall, Gudmund Grov.

_An Essence of SSReflect_. CICM 2012. [[https://doi.org/10.1007/978-3-642-31374-5_13][doi]]

- Georges Gonthier, Enrico Tassi.

_A Language of Patterns for Subterm Selection_. ITP 2012. [[https://hal.inria.fr/hal-00652286/file/rew.pdf][pdf]]

- Georges Gonthier, Assia Mahboubi.

_An introduction to small scale reflection in Coq_. Journal of Formalized Reasoning 3(2), 2010. [[https://hal.inria.fr/inria-00515548v4/document][pdf]]

- François Garillot, Georges Gonthier, Assia Mahboubi, Laurence Rideau.

_Packaging Mathematical Structures_. TPHOLs 2009. [[https://hal.inria.fr/inria-00368403v1/document][pdf]]

** Machine Learning

- Reynald Affeldt, Alessandro Bruni, Ekaterina Komendantskaya, Natalia Ślusarz, Kathrin Stark.

_Taming Differentiable Logics with Coq Formalisation_.

ITP 2024. [[https://drops.dagstuhl.de/storage/00lipics/lipics-vol309-itp2024/LIPIcs.ITP.2024.4/LIPIcs.ITP.2024.4.pdf][pdf]]

- Pengyu Nie, Karl Palmskog, Junyi Jessy Li, Milos Gligoric.

_Deep Generation of Coq Lemma Names Using Elaborated Terms_. IJCAR 2020. [[https://arxiv.org/pdf/2004.07761.pdf][pdf]]

- Jónathan Heras, Ekaterina Komendantskaya.

_Recycling Proof Patterns in Coq: Case Studies_. Mathematics in Computer Science 8(1), 2014. [[https://arxiv.org/pdf/1301.6039v4.pdf][pdf]]

- Jónathan Heras, Ekaterina Komendantskaya.

_Proof Pattern Search in Coq/SSReflect_. [[https://arxiv.org/pdf/1402.0081.pdf][CoRR abs/1402.0081]], 2014

- Jónathan Heras, Ekaterina Komendantskaya.

_ML4PG in Computer Algebra Verification_. CICM 2013. [[https://arxiv.org/pdf/1302.6421.pdf][pdf]]

* PhD theses and Habilitation theses

- Cyril Cohen.

_Structuring Mathematics in Dependent Type Theory_

Habilitation thesis, 2026. [[https://perso.crans.org/cohen/hdr.pdf][pdf]]

- Enrico Tassi.

_Elpi: rule-based extension language_

Habilitation thesis, 2026. [[https://inria.hal.science/hal-05294918v1][pdf]]

- Pierre Roux.

_Numerical Computations and Proofs: from Proof-Assistants to Aerospace Applications_

Habilitation thesis, 2025. [[https://www.onera.fr/sites/default/files/447/hdr.pdf][pdf]]

- Assia Mahboubi.

_Machine-checked computer-aided mathematics_

Habilitation thesis, 2021. [[https://theses.hal.science/tel-03107626v2][pdf]]