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
https://portal.mardi4nfdi.de/entity/Q5875421	2023-02-03	Paper
Quantitative continuity and Computable Analysis in Coq	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

Doctoral students

No records found.

Known relations from the MaRDI Knowledge Graph

Property	Value
MaRDI profile type	MaRDI person profile
instance of	human

This page was built for person: Laurent Théry