Laurent Théry

Available identifiers

zbMath Open thery.laurentMaRDI QIDQ742366

List of research outcomes

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
https://portal.mardi4nfdi.de/entity/Q5875421	2023-02-03	Paper
Formal Correctness of Comparison Algorithms Between Binary64 and Decimal64 Floating-Point Numbers	2022-07-01	Paper
https://portal.mardi4nfdi.de/entity/Q4989411	2021-05-25	Paper
Distant decimals of \(\pi \): formal proofs of some algorithms computing them and guarantees of exact computation	2018-08-21	Paper
Formally verified certificate checkers for hardest-to-round computation	2015-07-02	Paper
Implementing geometric algebra products with binary trees	2014-09-18	Paper
A machine-checked proof of the odd order theorem	2013-08-07	Paper
A formalization of Grassmann-Cayley algebra in Coq and its application to theorem proving in projective geometry	2011-11-25	Paper
A Modular Integration of SAT/SMT Solvers to Coq through Proof Witnesses	2011-11-22	Paper
Proof certificates for algebra and their application to automatic geometry theorem proving	2011-05-26	Paper
Extending Coq with Imperative Features and Its Application to SAT Verification	2010-09-14	Paper
Proving pearl: Knuth's algorithm for prime numbers	2010-05-07	Paper
A Purely Functional Library for Modular Arithmetic and Its Application to Certifying Large Prime Numbers	2009-03-12	Paper
Proof Pearl: Revisiting the Mini-rubik in Coq	2008-12-04	Paper
A Modular Formalisation of Finite Group Theory	2008-09-02	Paper
Primality Proving with Elliptic Curves	2008-09-02	Paper
A Computational Approach to Pocklington Certificates in Type Theory	2007-05-02	Paper
https://portal.mardi4nfdi.de/entity/Q3024829	2005-07-04	Paper
https://portal.mardi4nfdi.de/entity/Q4790659	2003-02-04	Paper
https://portal.mardi4nfdi.de/entity/Q2754056	2001-11-11	Paper
A machine-checked implementation of Buchberger's algorithm	2001-02-18	Paper
https://portal.mardi4nfdi.de/entity/Q4490725	2000-07-20	Paper
https://portal.mardi4nfdi.de/entity/Q4249903	1999-11-15	Paper
Interactive theorem proving with temporal logic	1997-10-13	Paper

Research outcomes over time

This page was built for person: Laurent Théry