Mathematical Components: Research Papers

Table of Contents

This is a list of research papers and theses using the Mathematical Components libraries and published (among others) in the following venues:

This list is non-exhaustive. Initial contents come from the official wiki.

Your paper or thesis is not in the list? Send us a message to correct this.


  • Xavier Allamigeon, Ricardo D. Katz, Pierre-Yves Strub. Formalizing the Face Lattice of Polyhedra. IJCAR 2020. 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. pdf, code
  • Florent Bréhard, Assia Mahboubi, Damien Pous. A certificate-based approach to formally verified approximations. ITP 2019. pdf
  • Reynald Affeldt, Cyril Cohen, Damien Rouhling. Formalization techniques for asymptotic reasoning in classical analysis. Journal of Formalized Reasoning 11(1), 2018. pdf
  • Reynald Affeldt, Cyril Cohen, Assia Mahboubi, Damien Rouhling, Pierre-Yves Strub. Classical Analysis with Coq. Coq Workshop 2018. pdf
  • Xavier Allamigeon, Ricardo D. Katz. A formalization of convex polyhedra based on the simplex method. ITP 2017. pdf
  • Evmorfia-Iro Bartzia. A Formalization of Elliptic Curves for Cryptography. PhD thesis, Université Paris-Saclay, 2017. 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. pdf
  • Cyril Cohen, Boris Djalal. Formalization of a newton series representation of polynomials. CPP 2016. pdf
  • Ken'ichi Kuga, Manabu Hagiwara, Mitsuharu Yamamoto. Formalization of Bing's Shrinking Method in Geometric Topology. CICM 2016. doi
  • Gallego Arias, Emilio Jesús, Pierre Jouvelot. Adventures in the (not so) Complex Space. Coq Workshop 2015. 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. pdf
  • Cyril Cohen, Anders Mörtberg. A Coq Formalization of Finitely Presented Modules. ITP 2014. pdf
  • Anders Mörtberg. Formalizing Refinements and Constructive Algebra in Type Theory. PhD, University of Gothenburg, 2014. pdf
  • Evmorfia-Iro Bartzia, Pierre-Yves Strub. A Formal Library for Elliptic Curves in the Coq Proof Assistant. ITP 2014. 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. 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. pdf
  • Maxime Dénès, Anders Mörtberg, Vincent Siles. A Refinement-Based Approach to Computational Algebra in Coq. ITP 2012. 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, 2012. pdf
  • Assia Mahboubi, Cyril Cohen. Formal proofs in real algebraic geometry: from ordered fields to quantifier elimination. LMCS 8(1), 2012. pdf
  • Thierry Coquand, Anders Mörtberg, Vincent Siles. Coherent and Strongly Discrete Rings in Type Theory. CPP 2012. pdf
  • Cyril Cohen. Formalized algebraic numbers: construction and first-order theory. PhD thesis, Ecole Polytechnique, 2012. pdf
  • Jónathan Heras, María Poza, Maxime Dénès, Laurence Rideau. Incidence Simplicial Matrices Formalized in Coq/SSReflect. Calculemus/MKM 2011: 30-44. pdf
  • Georges Gonthier. Point-Free, Set-Free Concrete Linear Algebra. ITP 2011. pdf
  • Georges Gonthier, Assia Mahboubi, Laurence Rideau, Enrico Tassi, Laurent Théry. A Modular Formalisation of Finite Group Theory. TPHOLs 2007. pdf

Graph Theory

  • Christian Doczkal, Damien Pous. Graph Theory in Coq: Minors, Treewidth, and Isomorphisms. JAR (special issue for ITP 2018), 2020. pdf
  • Christian Doczkal, Damien Pous. Completeness of an axiomatization of graph isomorphism via graph rewriting in Coq. CPP 2020. pdf
  • Daniel E. Severín. Formalization of the Domination Chain with Weighted Parameters. ITP 2019. pdf
  • Christian Doczkal, Guillaume Combette, Damien Pous. A Formal Proof of the Minor-Exclusion Property for Treewidth-Two Graphs. ITP 2018. pdf
  • George Gonthier. A computer-checked proof of the Four Colour Theorem. pdf


  • Cyril Cohen, Damien Rouhling. A Formal Proof in Coq of LaSalle's Invariance Principle. ITP 2017. pdf
  • Reynald Affeldt, Cyril Cohen. Formal Foundations of 3D Geometry to Model Robot Manipulators. CPP 2017. pdf

Programming and Algorithms

  • Kiran Gopinathan, Ilya Sergey. Certifying Certainty and Uncertainty in Approximate Membership Query Structures. 32nd International Conference on Computer-Aided Verification (CAV 2020). 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. pdf
  • Reynald Affeldt, Jacques Garrigue, Xuanrui Qi, Kazunari Tanaka. Proving tree algorithms for succinct data structures. ITP 2019. pdf
  • Reynald Affeldt, Jacques Garrigue, Xuanrui Qi, Kazunari Tanaka. Experience Report: Type-Driven Development of Certified Tree Algorithms in Coq. Coq Workshop 2019. pdf
  • Joseph Tassarotti, Robert Harper. Verified Tail Bounds for Randomized Programs. ITP 2018. pdf
  • Cyril Cohen, Damien Rouhling. A refinement-based approach to large scale reflection for algebra. JFLA 2017. pdf
  • Timmy Weerwag. Verifying an elliptic curve cryptographic algorithm using Coq and the Ssreflect extension. Master’s thesis, Mathematics, Radboud University, 2016. pdf
  • Beta Ziliani, Derek Dreyer, Neelakantan R. Krishnaswami, Aleksandar Nanevski, Viktor Vafeiadis. Mtac: A Monad for Typed Tactic Programming in Coq. Journal of Functional Programming 25, 2015. pdf
  • Cyril Cohen, Maxime Dénès, Anders Mörtberg. Refinements for free!. CPP 2013. pdf
  • Andrew Kennedy, Nick Benton, Jonas B. Jensen, Pierre-Evariste Dagand. Coq: the world's best macro assembler? PPDP 2013. pdf
  • Germán Andrés Delbianco, Aleksandar Nanevski. Hoare-Style Reasoning with (Algebraic) Continuations. ICFP 2013. doi
  • Beta Ziliani, Derek Dreyer, Neelakantan R. Krishnaswami, Aleksandar Nanevski, Viktor Vafeiadis. Mtac: A Monad for Typed Tactic Programming in Coq. ICFP 2013. doi
  • Aleksandar Nanevski, Viktor Vafeiadis, Josh Berdine. Structuring the Verification of Heap-Manipulating Programs. POPL 2010. doi


  • Ilya Sergey, James R. Wilcox, Zachary Tatlock. Programming and Proving with Distributed Protocols. POPL 2018. pdf
  • Germán Andrés Delbianco, Ilya Sergey, Aleksandar Nanevski, Anindya Banerjee. Concurrent Data Structures Linked in Time. ECOOP 2017. pdf
  • Mitsuharu Yamamoto, Shogo Sekine, Saki Matsumoto. Formalization of Karp-Miller Tree Construction on Petri Nets. CPP 2017. 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. pdf
  • Ilya Sergey, Aleksandar Nanevski, Anindya Banerjee, Germán Andrés Delbianco. Hoare-style Specifications as Correctness Conditions for Non-linearizable Concurrent Objects. OOPSLA 2016. pdf
  • Ilya Sergey, Aleksandar Nanevski, Anindya Banerjee. Mechanized Verification of Fine-grained Concurrent Programs. PLDI 2015. doi
  • Ilya Sergey, Aleksandar Nanevski, Anindya Banerjee. Specifying and Verifying Concurrent Algorithms with Histories and Subjectivity. ESOP 2015. pdf
  • Aleksandar Nanevski, Ruy Ley-Wild, Ilya Sergey, Germán Andrés Delbianco. Communicating State Transition Systems for Fine-Grained Concurrent Resources. ESOP 2014. doi
  • Ruy Ley-Wild, Aleksandar Nanevski. Subjective Auxiliary State for Coarse-Grained Concurrency. POPL 2013. 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. doi
  • Gordon Stewart, Anindya Banerjee, Aleksandar Nanevski. Dependent Types for Enforcement of Information Flow and Erasure Policies in Heterogeneous Data Structures. PPDP 2013. 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. IEEE Xplore

Other Applications

  • George Pîrlea, Ilya Sergey. Mechanising Blockchain Consensus. CPP 2018. pdf
  • Gallego Arias, Emilio Jesús, Olivier Hermant, Pierre Jouvelot. A Taste of Sound Reasoning in Faust. Linux Audio Conference 2015. 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). IEEE Xplore

Logic, Types, and Verification

  • Christian Doczkal, Gert Smolka. Regular Language Representations in the Constructive Type Theory of Coq. JAR 61, 2018. pdf
  • Christian Doczkal, Joachim Bard. Completeness and Decidability of Converse PDL in the Constructive Type Theory of Coq. CPP 2018. pdf
  • Véronique Benzaken, Evelyne Contejean, Stefania Dumbrava. Certifying Standard and Stratified Datalog Inference Engines in SSReflect. ITP 2017. 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). IEEE Xplore
  • Christian Doczkal, Gert Smolka. Completeness and Decidability Results for CTL in Constructive Type Theory. JAR 56, 2016. doi
  • Christian Doczkal, Gert Smolka. Completeness and Decidability Results for CTL in Coq. ITP 2014. pdf
  • Christian Doczkal, Gert Smolka. Constructive Completeness for Modal Logic with Transitive Closure. CPP 2012. doi
  • Christian Doczkal, Gert Smolka. Constructive Formalization of Hybrid Logic with Eventualities. CPP 2011. pdf
  • Kasper Svendsen, Lars Birkedal, Aleksandar Nanevski. Partiality, State and Dependent Types. International Conference on Typed Lambda Calculi and Applications (TLCA 2011). doi

Information Theory

  • Kyosuke Nakano, Manabu Hagiwara. Formalization of binary symmetric erasure channel based on infotheo. International Symposium on Information Theory and its Application 2016 (ISITA 2016). 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. 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). IEEE Xplore
  • Reynald Affeldt, Manabu Hagiwara, Jonas Sénizergues. Formalization of Shannon's theorems. Journal of Automated Reasoning 53(1), 2014. pdf
  • Reynald Affeldt, Manabu Hagiwara. Formalization of Shannon's Theorems in SSReflect-Coq. ITP 2012. pdf

Tooling about SSReflect and Mathematical Components

  • Pierre-Léo Bégay, Pierre Crégut, Jean-Francois Monin. Developing sequence and tree fintypes in MathComp. Coq Workshop 2020. pdf
  • Xavier Allamigeon, Cyril Cohen, Kazuhiko Sakaguchi, Pierre-Yves Strub. A hierarchy of ordered types in Mathematical Components. Coq Workshop 2020. pdf
  • Cyril Cohen, Kazuhiko Sakaguchi, Enrico Tassi. Hierarchy Builder: algebraic hierarchies made easy in Coq with Elpi. FSCD 2020. pdf
  • Karl Palmskog, Ahmet Celik, Milos Gligoric. Practical Machine-Checked Formalization of Change Impact Analysis. TACAS 2020. pdf
  • Kazuhiko Sakaguchi. Validating Mathematical Structures. IJCAR 2020. pdf
  • Erik Martin-Dorel, Enrico Tassi. SSReflect in Coq 8.10. Coq Workshop 2019. pdf
  • Kazuhiko Sakaguchi. Program Extraction for Mutable Arrays. FLOPS 2018. doi
  • Kazuhiko Sakaguchi, Yukiyoshi Kameyama. Efficient Finite-Domain Function Library for the Coq Proof Assistant. IPSJ Transactions on Programming 10(1), 2017. pdf (long, in Japanese), pdf (short, in English)
  • Georges Gonthier, Beta Ziliani, Aleksandar Nanevski, Derek Dreyer. How to make ad hoc proof automation less ad hoc. Journal of Functional Programming 23(4), 2013. doi
  • Vladimir Komendantsky, Alexander Konovalov, Steve Linton. Interfacing Coq + SSReflect with GAP. Electronic Notes in Theoretical Computer Science 285, 2012. pdf
  • Iain Whiteside, David Aspinall, Gudmund Grov. An Essence of SSReflect. CICM 2012. doi
  • Georges Gonthier, Enrico Tassi. A Language of Patterns for Subterm Selection. ITP 2012. pdf
  • Georges Gonthier, Assia Mahboubi. An introduction to small scale reflection in Coq. Journal of Formalized Reasoning 3(2), 2010. pdf
  • François Garillot, Georges Gonthier, Assia Mahboubi, Laurence Rideau. Packaging Mathematical Structures. TPHOLs 2009. pdf

Machine Learning

  • Pengyu Nie, Karl Palmskog, Junyi Jessy Li, Milos Gligoric. Deep Generation of Coq Lemma Names Using Elaborated Terms. IJCAR 2020. pdf
  • Jónathan Heras, Ekaterina Komendantskaya. Recycling Proof Patterns in Coq: Case Studies. Mathematics in Computer Science 8(1), 2014. pdf
  • Jónathan Heras, Ekaterina Komendantskaya. Proof Pattern Search in Coq/SSReflect. CoRR abs/1402.0081, 2014
  • Jónathan Heras, Ekaterina Komendantskaya. ML4PG in Computer Algebra Verification. CICM 2013. pdf