Laurent Théry

48 papers A 2B 7Misc 2Journal 17Unranked 18

Year	Rank	Type	Title / Venue / Authors
2022	J	`jnl`	A Formalisation of Algorithms for Sorting Network. CoRR Laurent Théry
2022	J	`jnl`	A Formalisation of a Fast Fourier Transform. CoRR Laurent Théry
2022	J	`jnl`	Primality Tests and Prime Certificate. CoRR Laurent Théry, Sophia Antipolis
2021	J	`jnl`	Computable analysis and notions of continuity in Coq. Log. Methods Comput. Sci. Florian Steinberg, Laurent Théry, Holger Thies
2021	B	`conf`	Proof Pearl : Playing with the Tower of Hanoi Formally. ITP Laurent Théry
2019	B	`conf`	Formal Proofs of Tarjan's Strongly Connected Components Algorithm in Why3, Coq and Isabelle. ITP Ran Chen, Cyril Cohen, Jean-Jacques Lévy, Stephan Merz, Laurent Théry
2019	B	`conf`	Quantitative Continuity and Computable Analysis in Coq. ITP Florian Steinberg, Laurent Théry, Holger Thies
2019	J	`jnl`	Quantitative continuity and computable analysis in Coq. CoRR Florian Steinberg, Laurent Théry, Holger Thies
2018	J	`jnl`	Distant Decimals of π : Formal Proofs of Some Algorithms Computing Them and Guarantees of Exact Computation. J. Autom. Reason. Yves Bertot, Laurence Rideau, Laurent Théry
2018	J	`jnl`	Formal Proofs of Tarjan's Algorithm in Why3, Coq, and Isabelle. CoRR Ran Chen, Cyril Cohen, Jean-Jacques Lévy, Stephan Merz, Laurent Théry
2017	J	`jnl`	Distant decimals of $π$. CoRR Yves Bertot, Laurence Rideau, Laurent Théry
2017	—	`conf`	Formal Correctness of Comparison Algorithms Between Binary64 and Decimal64 Floating-Point Numbers. NSV@CAV Arthur Blot, Jean-Michel Muller, Laurent Théry
2015	J	`jnl`	Foreword to the Special Focus on Formal Proofs for Mathematics and Computer Science. Math. Comput. Sci. Laurent Théry, Freek Wiedijk
2015	J	`jnl`	Formally Verified Certificate Checkers for Hardest-to-Round Computation. J. Autom. Reason. Érik Martin-Dorel, Guillaume Hanrot, Micaela Mayero, Laurent Théry
2013	B	`conf`	A Machine-Checked Proof of the Odd Order Theorem. ITP Georges Gonthier, Andrea Asperti, Jeremy Avigad, Yves Bertot, Cyril Cohen, François Garillot, Stéphane Le Roux, Assia Mahboubi, Russell O'Connor, Sidi Ould Biha, Ioana Pasca, Laurence Rideau, Alexey Solovyev, Enrico Tassi, Laurent Théry
2013	Misc	`conf`	Certified, Efficient and Sharp Univariate Taylor Models in COQ. SYNASC Érik Martin-Dorel, Laurence Rideau, Laurent Théry, Micaela Mayero, Ioana Pasca
2012	—	`conf`	Rigorous Polynomial Approximation Using Taylor Models in Coq. NASA Formal Methods Nicolas Brisebarre, Mioara Joldes, Érik Martin-Dorel, Micaela Mayero, Jean-Michel Muller, Ioana Pasca, Laurence Rideau, Laurent Théry
2011	—	`conf`	A Flexible Proof Format for SMT: a Proposal. PxTP Frédéric Besson, Pascal Fontaine, Laurent Théry
2011	B	`conf`	A Modular Integration of SAT/SMT Solvers to Coq through Proof Witnesses. CPP Michaël Armand, Germain Faure, Benjamin Grégoire, Chantal Keller, Laurent Théry, Benjamin Werner
2010	—	`conf`	A Formalization of Grassmann-Cayley Algebra in COQ and Its Application to Theorem Proving in Projective Geometry. Automated Deduction in Geometry Laurent Fuchs, Laurent Théry
2010	B	`conf`	Extending Coq with Imperative Features and Its Application to SAT Verification. ITP Michaël Armand, Benjamin Grégoire, Arnaud Spiwack, Laurent Théry
2009	J	`jnl`	A distributed editing environment for XML documents CoRR Claude Pasquier, Laurent Théry
2008	—	`conf`	Proof Certificates for Algebra and Their Application to Automatic Geometry Theorem Proving. Automated Deduction in Geometry Benjamin Grégoire, Loïc Pottier, Laurent Théry
2008	—	`conf`	Proof Pearl: Revisiting the Mini-rubik in Coq. TPHOLs Laurent Théry
2007	—	`conf`	A Modular Formalisation of Finite Group Theory. TPHOLs Georges Gonthier, Assia Mahboubi, Laurence Rideau, Enrico Tassi, Laurent Théry
2007	—	`conf`	Primality Proving with Elliptic Curves. TPHOLs Laurent Théry, Guillaume Hanrot
2006	Misc	`conf`	A Computational Approach to Pocklington Certificates in Type Theory. FLOPS Benjamin Grégoire, Laurent Théry, Benjamin Werner
2006	A	`conf`	A Purely Functional Library for Modular Arithmetic and Its Application to Certifying Large Prime Numbers. IJCAR Benjamin Grégoire, Laurent Théry
2006	—	`ch.`	Coq. The Seventeen Provers of the World Laurent Théry, Pierre Letouzey, Georges Gonthier
2006	J	`jnl`	Formalising Sylow's theorems in Coq CoRR Laurent Théry
2005	—	`conf`	Dependent Types, Theorem Proving, and Applications for a Verifying Compiler. VSTTE Yves Bertot, Laurent Théry
2003	—	`conf`	Colouring Proofs: A Lightweight Approach to Adding Formal Structure to Proofs. UITP@TPHOLs Laurent Théry
2003	—	`conf`	Proving Pearl: Knuth's Algorithm for Prime Numbers. TPHOLs Laurent Théry
2001	—	`conf`	A Generic Library for Floating-Point Numbers and Its Application to Exact Computing. TPHOLs Marc Daumas, Laurence Rideau, Laurent Théry
2001	J	`jnl`	A Machine-Checked Implementation of Buchberger's Algorithm. J. Autom. Reason. Laurent Théry
2001	J	`jnl`	Computer validated proofs of a toolset for adaptable arithmetic CoRR Sylvie Boldo, Marc Daumas, Claire Moreau-Finot, Laurent Théry
2000	—	`conf`	Formalizing Stålmarck's Algorithm in Coq. TPHOLs Pierre Letouzey, Laurent Théry
1999	—	`ed.`	Theorem Proving in Higher Order Logics, 12th International Conference, TPHOLs'99, Nice, France, September, 1999, Proceedings TPHOLs Yves Bertot, Gilles Dowek, André Hirschowitz, Christine Paulin-Mohring, Laurent Théry
1998	A	`conf`	A Certified Version of Buchberger's Algorithm. CADE Laurent Théry
1998	J	`jnl`	A Generic Approach to Building User Interfaces for Theorem Provers. J. Symb. Comput. Yves Bertot, Laurent Théry
1998	J	`jnl`	A Skeptic's Approach to Combining HOL and Maple. J. Autom. Reason. John Harrison, Laurent Théry
1997	J	`jnl`	Interactive Theorem Proving with Temporal Logic. J. Symb. Comput. Amy P. Felty, Laurent Théry
1995	—	`conf`	Extracting Text from Proofs. TLCA Yann Coscoy, Gilles Kahn, Laurent Théry
1994	—	`conf`	Proof by Pointing. TACS Yves Bertot, Gilles Kahn, Laurent Théry
1993	—	`conf`	A Proof Development System for HOL. HUG Laurent Théry
1993	—	`conf`	Extending the HOL Theorem Prover with a Computer Algebra System to Reason about the Reals. HUG John Harrison, Laurent Théry
1993	B	`conf`	Reasoning About the Reals: The Marriage of HOL and Maple. LPAR John Harrison, Laurent Théry
1992	—	`conf`	Real theorem provers deserve real user-interfaces. SDE Laurent Théry, Yves Bertot, Gilles Kahn