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:

Your paper/thesis is not in the list? You have a suggestion about the organization of this page? Please, send us a message or issue/PR on github.

Mathematics

  • Reynald Affeldt, Zachary Stone. A Comprehensive Overview of the Lebesgue Differentiation Theorem in Coq. ITP 2024. pdf
  • Assia Mahboubi, Matthieu Piquerez. A First Order Theory of Diagram Chasing. 32nd EACSL Annual Conference on Computer Science Logic (CSL 2024). pdf
  • Benoît Guillemet, Assia Mahboubi, Matthieu Piquerez. Machine-Checked Categorical Diagrammatic Reasoning. FSCD 2024. pdf
  • Yoshihiro Ishiguro, Reynald Affeldt. The Radon-Nikodým Theorem and the Lebesgue-Stieltjes Measure in Coq. Computer Software 41(2), 2024. pdf
  • Reynald Affeldt, Cyril Cohen. Measure construction by extension in dependent type theory with application to integration. JAR 2023. 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. pdf
  • Xavier Allamigeon, Quentin Canu, Pierre-Yves Strub. A Formal Disproof of Hirsch Conjecture. CPP 2023. pdf
  • Xavier Allamigeon, Ricardo D. Katz, Pierre-Yves Strub. Formalizing the Face Lattice of Polyhedra. LMCS 18(2), 2022. pdf
  • Assia Mahboubi, Thomas Sibut-Pinote. A Formal Proof of the Irrationality of ζ(3). LMCS 17(1), 2021. pdf
  • Sophie Bernard, Cyril Cohen, Assia Mahboubi, Pierre-Yves Strub. Unsolvability of the Quintic Formalized in Dependent Type Theory ITP 2021. pdf
  • 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
  • Xavier Allamigeon, Ricardo D. Katz. A Formalization of Convex Polyhedra Based on the Simplex Method. JAR 63(2), 2019. doi
  • 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
  • Cyril Cohen. Pragmatic Quotient Types in Coq. ITP 2013. pdf
  • Assia Mahboubi. The Rooster and the Butterflies. CICM 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 (CTIC 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. 18th Symposium on Symposium on the Integration of Symbolic Computation and Mechanized Reasoning (Calculemus 2011). pdf
  • Georges Gonthier. Point-Free, Set-Free Concrete Linear Algebra. ITP 2011. pdf
  • Sidi Ould Biha. Finite groups representation theory with Coq. 8th International Conference on Mathematical Knowledge Management (MKM 2009). pdf
  • Yves Bertot, Georges Gonthier, Sidi Ould Biha, Ioana Pasca. Canonical Big Operators. ITP 2008. pdf
  • Georges Gonthier, Assia Mahboubi, Laurence Rideau, Enrico Tassi, Laurent Théry. A Modular Formalisation of Finite Group Theory. TPHOLs 2007. pdf
  • Laurent Théry, Laurence Rideau. Formalising Sylow’s theorems in Coq. RT-0327 INRIA 2006. pdf

Graph Theory

  • Christian Doczkal. A Variant of Wagner’s Theorem Based on Combinatorial Hypermaps. ITP 2021. pdf
  • 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

Robotics

  • Yves Bertot, Safe Smooth Paths Between Straight Line Obstacles. Logics and Type Systems in Theory and Practice, LNCS 14560, Springer, 2024. doi, 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

  • Cyril Cohen, Kazuhiko Sakaguchi. A bargain for mergesorts (functional pearl) – How to prove your mergesort correct and stable, almost for free. arXiv 2024. 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. 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. 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). doi
  • Ayumu Saito, Reynald Affeldt. Towards a Practical Library for Monadic Equational Reasoning in Coq. Mathematics of Program Construction (MPC 2022). pdf
  • Reynald Affeldt, David Nowak. Extending equational monadic reasoning with monad transformers. TYPES 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
  • Cyril Cohen, Damien Rouhling. A refinement-based approach to large scale reflection for algebra. 28ème Journées Francophones des Langages Applicatifs (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. JFP 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

Concurrency

  • Mohit Tekriwal, Avi Tachna-Fram, Jean-Baptiste Jeannin, Manos Kapritsos, Dimitra Panagou. Formally verified asymptotic consensus in robust networks. TACAS 2024. pdf
  • Søren Eller Thomsen, Bas Spitters. Formalizing Nakamoto-Style Proof of Stake. 34th IEEE Computer Security Foundations Symposium (CSF 2021). 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). pdf
  • Joseph Tassarotti, Robert Harper. A Separation Logic for Concurrent Randomized Programs. POPL 2019. pdf
  • Ilya Sergey, James R. Wilcox, Zachary Tatlock. Programming and Proving with Distributed Protocols. POPL 2018. pdf
  • George Pîrlea, Ilya Sergey. Mechanising Blockchain Consensus. CPP 2018. 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). 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
  • Ralf Jung, Robbert Krebbers, Lars Birkedal, Derek Dreyer. Higher-Order Ghost State. ICFP 2016. 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). pdf
  • Ilya Sergey, Aleksandar Nanevski, Anindya Banerjee. Mechanized Verification of Fine-grained Concurrent Programs. Programming Language Design and Implementation (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

Probabilistic Reasoning

  • 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. pdf
  • Ayumu Saito, Reynald Affeldt. Experimenting with an Intrinsically-Typed Probabilistic Programming Language in Coq. Asian Symposium on Programming Languages and Systems (APLAS 2023). doi
  • Reynald Affeldt, Cyril Cohen, Ayumu Saito. Semantics of Probabilistic Programs using s-Finite Kernels in Coq. CPP 2023. pdf
  • Ieva Daukantas, Alessandro Bruni, Carsten Schürmann. Trimming Data Sets: a Verified Algorithm for Robust Mean Estimation. PPDP 2021. doi
  • Reynald Affeldt, Jacques Garrigue, David Nowak, Takafumi Saikawa. A trustful monad for axiomatic reasoning with probability and nondeterminism. JFP 31(E17), 2021. pdf
  • 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, Jacques Garrigue, Takafumi Saikawa. Formal adventures in convex and conical spaces. CICM 2020. pdf
  • Reynald Affeldt, Jacques Garrigue, Takafumi Saikawa. Reasoning with conditional probabilities and joint distributions. Computer Software 37(3):79-95, 2020. pdf
  • Joseph Tassarotti, Robert Harper. Verified Tail Bounds for Randomized Programs. ITP 2018. pdf

Quantum Computing

  • Jacques Garrigue and Takafumi Saikawa. Typed compositional quantum computation with lenses. ITP 2024. pdf
  • Li Zhou, Gilles Barthe, Pierre-Yves Strub, Junyi Liu, Mingsheng Ying. CoqQ: Foundational Verification of Quantum Programs. POPL 2023. 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. 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

  • 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. doi
  • 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
  • Angela Bonifati, Stefania Dumbrava, Emilio Jesús Gallego Arias. Certified Graph View Maintenance with Regular Datalog. 34th International Conference on Logic Programming (ICLP 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
  • Thierry Coquand, Vincent Siles. A Decision Procedure for Regular Expression Equivalence in Type Theory. CPP 2011. doi
  • Kasper Svendsen, Lars Birkedal, Aleksandar Nanevski. Partiality, State and Dependent Types. International Conference on Typed Lambda Calculi and Applications (TLCA 2011). 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). pdf
  • Reynald Affeldt, Jacques Garrigue, Takafumi Saikawa. A library for formalization of linear error-correcting codes. JAR 64:1123-1164, 2020. 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). 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. JAR 53(1), 2014. pdf
  • Reynald Affeldt, Manabu Hagiwara. Formalization of Shannon's Theorems in SSReflect-Coq. ITP 2012. pdf

Tooling

  • Cyril Cohen, Enzo Crance, Assia Mahboubi. Trocq: Proof Transfer for Free, With or Without Univalence. ESOP 2024. pdf
  • Xavier Allamigeon, Quentin Canu, Cyril Cohen, Kazuhiko Sakaguchi, Pierre-Yves Strub. Design patterns of hierarchies for order structures. HAL 2023. 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. pdf
  • Benjamin Grégoire, Jean-Christophe Léchenet, Enrico Tassi. Practical and sound equality tests, automatically. CPP 2023. pdf
  • Kazuhiko Sakaguchi. Reflexive tactics for algebra, revisited. ITP 2022. 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. pdf
  • 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
  • Kazuhiko Sakaguchi. Program extraction for mutable arrays. Science of Computer Programming 191, 2020. doi
  • Erik Martin-Dorel, Enrico Tassi. SSReflect in Coq 8.10. Coq Workshop 2019. pdf
  • Kazuhiko Sakaguchi. Program Extraction for Mutable Arrays. 15th International Symposium on Functional and Logic Programming (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. JFP 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

  • Reynald Affeldt, Alessandro Bruni, Ekaterina Komendantskaya, Natalia Ślusarz, Kathrin Stark. Taming Differentiable Logics with Coq Formalisation. ITP 2024. pdf
  • 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