Laurent Théry

According to our database¹, Laurent Théry authored at least 46 papers between 1992 and 2022.

Collaborative distances:

Dijkstra number² of three.
Erdős number³ of three.

Timeline

Legend:

Book

In proceedings

Article

PhD thesis

Dataset

Other

Links

On csauthors.net:

Bibliography

2022

A Formalisation of a Fast Fourier Transform.

[BibT_eX]

[DOI]

Laurent Théry

CoRR, 2022

Primality Tests and Prime Certificate.

[BibT_eX]

[DOI]

Laurent Théry

Sophia Antipolis

CoRR, 2022

A Formalisation of Algorithms for Sorting Network.

[BibT_eX]

[DOI]

Laurent Théry

CoRR, 2022

2021

Computable analysis and notions of continuity in Coq.

[BibT_eX]

[DOI]

Florian Steinberg

Laurent Théry

Holger Thies

Log. Methods Comput. Sci., 2021

Proof Pearl : Playing with the Tower of Hanoi Formally.

[BibT_eX]

[DOI]

Laurent Théry

Proceedings of the 12th International Conference on Interactive Theorem Proving, 2021

2019

Quantitative Continuity and Computable Analysis in Coq.

[BibT_eX]

[DOI]

Florian Steinberg

Laurent Théry

Holger Thies

Proceedings of the 10th International Conference on Interactive Theorem Proving, 2019

Formal Proofs of Tarjan's Strongly Connected Components Algorithm in Why3, Coq and Isabelle.

[BibT_eX]

[DOI]

Proceedings of the 10th International Conference on Interactive Theorem Proving, 2019

2018

Distant Decimals of π : Formal Proofs of Some Algorithms Computing Them and Guarantees of Exact Computation.

[BibT_eX]

[DOI]

Yves Bertot

Laurence Rideau

Laurent Théry

J. Autom. Reason., 2018

Formal Proofs of Tarjan's Algorithm in Why3, Coq, and Isabelle.

[BibT_eX]

[DOI]

CoRR, 2018

2017

Distant decimals of $π$.

[BibT_eX]

[DOI]

Yves Bertot

Laurence Rideau

Laurent Théry

CoRR, 2017

Formal Correctness of Comparison Algorithms Between Binary64 and Decimal64 Floating-Point Numbers.

[BibT_eX]

[DOI]

Arthur Blot

Jean-Michel Muller

Laurent Théry

Proceedings of the Numerical Software Verification - 10th International Workshop, 2017

2015

Foreword to the Special Focus on Formal Proofs for Mathematics and Computer Science.

[BibT_eX]

[DOI]

Laurent Théry

Freek Wiedijk

Math. Comput. Sci., 2015

Formally Verified Certificate Checkers for Hardest-to-Round Computation.

[BibT_eX]

[DOI]

J. Autom. Reason., 2015

2013

Certified, Efficient and Sharp Univariate Taylor Models in COQ.

[BibT_eX]

[DOI]

Proceedings of the 15th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, 2013

A Machine-Checked Proof of the Odd Order Theorem.

[BibT_eX]

[DOI]

Proceedings of the Interactive Theorem Proving - 4th International Conference, 2013

2012

Rigorous Polynomial Approximation Using Taylor Models in Coq.

[BibT_eX]

[DOI]

Proceedings of the NASA Formal Methods, 2012

2011

A Flexible Proof Format for SMT: a Proposal.

[BibT_eX]

[DOI]

Frédéric Besson

Pascal Fontaine

Laurent Théry

Proceedings of the PxTP 2011: First International Workshop on Proof eXchange for Theorem Proving, 2011

A Modular Integration of SAT/SMT Solvers to Coq through Proof Witnesses.

[BibT_eX]

[DOI]

Proceedings of the Certified Programs and Proofs - First International Conference, 2011

2010

Extending Coq with Imperative Features and Its Application to SAT Verification.

[BibT_eX]

[DOI]

Proceedings of the Interactive Theorem Proving, First International Conference, 2010

A Formalization of Grassmann-Cayley Algebra in COQ and Its Application to Theorem Proving in Projective Geometry.

[BibT_eX]

[DOI]

Laurent Fuchs

Laurent Théry

Proceedings of the Automated Deduction in Geometry - 8th International Workshop, 2010

2009

A distributed editing environment for XML documents

[BibT_eX]

[DOI]

Claude Pasquier

Laurent Théry

CoRR, 2009

2008

Proof Pearl: Revisiting the Mini-rubik in Coq.

[BibT_eX]

[DOI]

Laurent Théry

Proceedings of the Theorem Proving in Higher Order Logics, 21st International Conference, 2008

Proof Certificates for Algebra and Their Application to Automatic Geometry Theorem Proving.

[BibT_eX]

[DOI]

Benjamin Grégoire

Loïc Pottier

Laurent Théry

Proceedings of the Automated Deduction in Geometry - 7th International Workshop, 2008

2007

Primality Proving with Elliptic Curves.

[BibT_eX]

[DOI]

Laurent Théry

Guillaume Hanrot

Proceedings of the Theorem Proving in Higher Order Logics, 20th International Conference, 2007

A Modular Formalisation of Finite Group Theory.

[BibT_eX]

[DOI]

Proceedings of the Theorem Proving in Higher Order Logics, 20th International Conference, 2007

2006

Formalising Sylow's theorems in Coq

[BibT_eX]

[DOI]

Laurent Théry

CoRR, 2006

Coq.

[BibT_eX]

[DOI]

Laurent Théry

Pierre Letouzey

Georges Gonthier

Proceedings of the Seventeen Provers of the World, Foreword by Dana S. Scott, 2006

A Computational Approach to Pocklington Certificates in Type Theory.

[BibT_eX]

[DOI]

Benjamin Grégoire

Laurent Théry

Benjamin Werner

Proceedings of the Functional and Logic Programming, 8th International Symposium, 2006

A Purely Functional Library for Modular Arithmetic and Its Application to Certifying Large Prime Numbers.

[BibT_eX]

[DOI]

Benjamin Grégoire

Laurent Théry

Proceedings of the Automated Reasoning, Third International Joint Conference, 2006

2005

Dependent Types, Theorem Proving, and Applications for a Verifying Compiler.

[BibT_eX]

[DOI]

Yves Bertot

Laurent Théry

Proceedings of the Verified Software: Theories, 2005

2003

Colouring Proofs: A Lightweight Approach to Adding Formal Structure to Proofs.

[BibT_eX]

[DOI]

Laurent Théry

Proceedings of the User Interfaces for Theorem Provers Workshop, 2003

Proving Pearl: Knuth's Algorithm for Prime Numbers.

[BibT_eX]

[DOI]

Laurent Théry

Proceedings of the Theorem Proving in Higher Order Logics, 16th International Conference, 2003

2001

A Machine-Checked Implementation of Buchberger's Algorithm.

[BibT_eX]

[DOI]

Laurent Théry

J. Autom. Reason., 2001

Computer validated proofs of a toolset for adaptable arithmetic

[BibT_eX]

[DOI]

CoRR, 2001

A Generic Library for Floating-Point Numbers and Its Application to Exact Computing.

[BibT_eX]

[DOI]

Marc Daumas

Laurence Rideau

Laurent Théry

Proceedings of the Theorem Proving in Higher Order Logics, 14th International Conference, 2001

2000

Formalizing Stålmarck's Algorithm in Coq.

[BibT_eX]

[DOI]

Pierre Letouzey

Laurent Théry

Proceedings of the Theorem Proving in Higher Order Logics, 13th International Conference, 2000

1998

A Generic Approach to Building User Interfaces for Theorem Provers.

[BibT_eX]

[DOI]

Yves Bertot

Laurent Théry

J. Symb. Comput., 1998

A Skeptic's Approach to Combining HOL and Maple.

[BibT_eX]

[DOI]

John Harrison

Laurent Théry

J. Autom. Reason., 1998

A Certified Version of Buchberger's Algorithm.

[BibT_eX]

[DOI]

Laurent Théry

Proceedings of the Automated Deduction, 1998

1997

Interactive Theorem Proving with Temporal Logic.

[BibT_eX]

[DOI]

Amy P. Felty

Laurent Théry

J. Symb. Comput., 1997

1995

Extracting Text from Proofs.

[BibT_eX]

[DOI]

Yann Coscoy

Gilles Kahn

Laurent Théry

Proceedings of the Typed Lambda Calculi and Applications, 1995

1994

Proof by Pointing.

[BibT_eX]

[DOI]

Yves Bertot

Gilles Kahn

Laurent Théry

Proceedings of the Theoretical Aspects of Computer Software, 1994

1993

A Proof Development System for HOL.

[BibT_eX]

[DOI]

Laurent Théry

Proceedings of the Higher Order Logic Theorem Proving and its Applications, 1993

Extending the HOL Theorem Prover with a Computer Algebra System to Reason about the Reals.

[BibT_eX]

[DOI]

John Harrison

Laurent Théry

Proceedings of the Higher Order Logic Theorem Proving and its Applications, 1993

Reasoning About the Reals: The Marriage of HOL and Maple.

[BibT_eX]

[DOI]

John Harrison

Laurent Théry

Proceedings of the Logic Programming and Automated Reasoning,4th International Conference, 1993

1992

Real theorem provers deserve real user-interfaces.

[BibT_eX]

[DOI]

Laurent Théry

Yves Bertot

Gilles Kahn

Proceedings of the 5th ACM SIGSOFT Symposium on Software Development Environments, 1992

Laurent Théry

Timeline

Legend:

Links

On csauthors.net:

Bibliography

Loading...