| Publication | Date of Publication | Type |
|---|
| Mathematical structures in dependent type theory (invited talk) | 2026-03-23 | Paper |
| Machine-checked computational mathematics (invited talk) | 2024-11-26 | Paper |
| Gardening with the pythia a model of continuity in a dependent setting | 2024-04-10 | Paper |
Valuative Lattices and Spectra
Algebraic, Number Theoretic, and Topological Aspects of Ring Theory | 2024-02-06 | Paper |
| scientific article; zbMATH DE number 7699425 (Why is no real title available?) | 2023-06-20 | Paper |
| A certificate-based approach to formally verified approximations | 2023-02-03 | Paper |
Competing Inheritance Paths in Dependent Type Theory: A Case Study in Functional Analysis
Automated Reasoning | 2022-11-09 | Paper |
A formal proof of the irrationality of \(\zeta(3)\)
(available as arXiv preprint) | 2021-03-26 | Paper |
| A formal proof of the irrationality of \(\zeta(3)\) | 2021-03-26 | Paper |
Formally verified approximations of definite integrals
Journal of Automated Reasoning | 2019-02-18 | Paper |
Geometric theories for the algebra of real numbers
Ordered Algebraic Structures and Related Topics | 2018-04-16 | Paper |
| Machine-checked mathematics | 2017-05-18 | Paper |
Axiomatic constraint systems for proof search modulo theories
Frontiers of Combining Systems | 2017-02-27 | Paper |
An induction principle over real numbers
Archive for Mathematical Logic | 2017-02-24 | Paper |
Formally verified approximations of definite integrals
Interactive Theorem Proving | 2016-10-27 | Paper |
A Computer-Algebra-Based Formal Proof of the Irrationality of ζ(3)
Interactive Theorem Proving | 2014-09-08 | Paper |
The Rooster and the Butterflies
Lecture Notes in Computer Science | 2013-08-09 | Paper |
A machine-checked proof of the odd order theorem
Interactive Theorem Proving | 2013-08-07 | Paper |
Canonical structures for the working Coq user
Interactive Theorem Proving | 2013-08-07 | Paper |
A simplex-based extension of Fourier-Motzkin for solving linear integer arithmetic
Automated Reasoning | 2012-09-05 | Paper |
Formal proofs in real algebraic geometry: from ordered fields to quantifier elimination
Logical Methods in Computer Science | 2012-04-03 | Paper |
A formal study of Bernstein coefficients and polynomials
Mathematical Structures in Computer Science | 2011-10-21 | Paper |
| An introduction to small scale reflection in Coq | 2011-02-10 | Paper |
A formal quantifier elimination for algebraically closed fields
Lecture Notes in Computer Science | 2010-08-24 | Paper |
Packaging Mathematical Structures
Lecture Notes in Computer Science | 2009-10-20 | Paper |
Proving Formally the Implementation of an Efficient gcd Algorithm for Polynomials
Automated Reasoning | 2009-03-12 | Paper |
A Modular Formalisation of Finite Group Theory
Lecture Notes in Computer Science | 2008-09-02 | Paper |
Implementing the cylindrical algebraic decomposition within the Coq system
Mathematical Structures in Computer Science | 2007-04-12 | Paper |
Theorem Proving in Higher Order Logics
Lecture Notes in Computer Science | 2006-07-06 | Paper |
