| Publication | Date of Publication | Type |
|---|
| Proof Pearl : Playing with the Tower of Hanoi Formally | 2023-06-20 | Paper |
| Quantitative continuity and Computable Analysis in Coq | 2023-02-03 | Paper |
scientific article; zbMATH DE number 7649962 (Why is no real title available?)
(available as arXiv preprint) | 2023-02-03 | Paper |
Formal correctness of comparison algorithms between binary64 and decimal64 floating-point numbers
Numerical Software Verification | 2022-07-01 | Paper |
Computable analysis and notions of continuity in \textsc{Coq}
(available as arXiv preprint) | 2021-05-25 | Paper |
| Computable analysis and notions of continuity in \textsc{Coq} | 2021-05-25 | Paper |
Distant decimals of \(\pi \): formal proofs of some algorithms computing them and guarantees of exact computation
Journal of Automated Reasoning | 2018-08-21 | Paper |
Formally verified certificate checkers for hardest-to-round computation
Journal of Automated Reasoning | 2015-07-02 | Paper |
Implementing geometric algebra products with binary trees
Advances in Applied Clifford Algebras | 2014-09-18 | Paper |
A machine-checked proof of the odd order theorem
Interactive Theorem Proving | 2013-08-07 | Paper |
A formalization of Grassmann-Cayley algebra in Coq and its application to theorem proving in projective geometry
Automated Deduction in Geometry | 2011-11-25 | Paper |
A Modular Integration of SAT/SMT Solvers to Coq through Proof Witnesses
Certified Programs and Proofs | 2011-11-22 | Paper |
Proof certificates for algebra and their application to automatic geometry theorem proving
Automated Deduction in Geometry | 2011-05-26 | Paper |
Extending Coq with Imperative Features and Its Application to SAT Verification
Interactive Theorem Proving | 2010-09-14 | Paper |
Proving pearl: Knuth's algorithm for prime numbers
Lecture Notes in Computer Science | 2010-05-07 | Paper |
A Purely Functional Library for Modular Arithmetic and Its Application to Certifying Large Prime Numbers
Automated Reasoning | 2009-03-12 | Paper |
Proof Pearl: Revisiting the Mini-rubik in Coq
Lecture Notes in Computer Science | 2008-12-04 | Paper |
A Modular Formalisation of Finite Group Theory
Lecture Notes in Computer Science | 2008-09-02 | Paper |
Primality Proving with Elliptic Curves
Lecture Notes in Computer Science | 2008-09-02 | Paper |
A Computational Approach to Pocklington Certificates in Type Theory
Functional and Logic Programming | 2007-05-02 | Paper |
| scientific article; zbMATH DE number 2185656 (Why is no real title available?) | 2005-07-04 | Paper |
| scientific article; zbMATH DE number 1863384 (Why is no real title available?) | 2003-02-04 | Paper |
| scientific article; zbMATH DE number 1670755 (Why is no real title available?) | 2001-11-11 | Paper |
A machine-checked implementation of Buchberger's algorithm
Journal of Automated Reasoning | 2001-02-18 | Paper |
| scientific article; zbMATH DE number 1479613 (Why is no real title available?) | 2000-07-20 | Paper |
| scientific article; zbMATH DE number 1303350 (Why is no real title available?) | 1999-11-15 | Paper |
Interactive theorem proving with temporal logic
Journal of Symbolic Computation | 1997-10-13 | Paper |
