×
Author ID: thery.laurent Recent zbMATH articles by "Théry, Laurent"
Published as: Théry, Laurent; Thery, Laurent; Théry, L.

Publications by Year

Citations contained in zbMATH Open

23 Publications have been cited 242 times in 213 Documents Cited by Year
A machine-checked proof of the odd order theorem. Zbl 1317.68211
Gonthier, Georges; Asperti, Andrea; Avigad, Jeremy; Bertot, Yves; Cohen, Cyril; Garillot, François; Le Roux, Stéphane; Mahboubi, Assia; O’Connor, Russell; Ould Biha, Sidi; Pasca, Ioana; Rideau, Laurence; Solovyev, Alexey; Tassi, Enrico; Théry, Laurent
64
2013
A Skeptic’s approach to combining HOL and Maple. Zbl 0916.68142
Harrison, J.; Théry, L.
26
1998
A modular integration of SAT/SMT solvers to Coq through proof witnesses. Zbl 1350.68223
Armand, Michael; Faure, Germain; Grégoire, Benjamin; Keller, Chantal; Théry, Laurent; Werner, Benjamin
21
2011
A modular formalisation of finite group theory. Zbl 1144.68356
Gonthier, Georges; Mahboubi, Assia; Rideau, Laurence; Tassi, Enrico; Théry, Laurent
21
2007
A generic library for floating-point numbers and its application to exact computing. Zbl 1005.68544
Daumas, Marc; Rideau, Laurence; Théry, Laurent
18
2001
Extending Coq with imperative features and its application to SAT verification. Zbl 1291.68318
Armand, Michaël; Grégoire, Benjamin; Spiwack, Arnaud; Théry, Laurent
15
2010
Implementing geometric algebra products with binary trees. Zbl 1311.68147
Fuchs, Laurent; Théry, Laurent
9
2014
A formalization of Grassmann-Cayley algebra in Coq and its application to theorem proving in projective geometry. Zbl 1350.68233
Fuchs, Laurent; Théry, Laurent
8
2011
Proof certificates for algebra and their application to automatic geometry theorem proving. Zbl 1302.68242
Grégoire, Benjamin; Pottier, Loïc; Théry, Laurent
8
2011
A machine-checked implementation of Buchberger’s algorithm. Zbl 0964.03012
Théry, Laurent
7
2001
Primality proving with elliptic curves. Zbl 1144.68367
Théry, Laurent; Hanrot, Guillaume
7
2007
A purely functional library for modular arithmetic and its application to certifying large prime numbers. Zbl 1222.68363
Grégoire, Benjamin; Théry, Laurent
6
2006
Reasoning about the reals: The marriage of HOL and Maple. Zbl 0793.68084
Harrison, John; Théry, Laurent
6
1993
A computational approach to Pocklington certificates in type theory. Zbl 1185.68621
Grégoire, Benjamin; Théry, Laurent; Werner, Benjamin
5
2006
Proof by pointing. Zbl 0942.03504
Bertot, Yves; Kahn, Gilles; Théry, Laurent
4
1994
Proving pearl: Knuth’s algorithm for prime numbers. Zbl 1279.68298
Théry, Laurent
3
2003
Extracting text from proofs. Zbl 1063.68647
Coscoy, Yann; Kahn, Gilles; Théry, Laurent
3
1995
Theorem proving in higher order logics. 12th international conference, TPHOLs ’99. Nice, France, September 14–17, 1999. Proceedings. Zbl 0929.00038
2
1999
A certified version of Buchberger’s algorithm. Zbl 0924.03025
Théry, Laurent
2
1998
Formally verified certificate checkers for hardest-to-round computation. Zbl 1315.68222
Martin-Dorel, Érik; Hanrot, Guillaume; Mayero, Micaela; Théry, Laurent
2
2015
Computable analysis and notions of continuity in Coq. Zbl 07350782
Steinberg, Florian; Thery, Laurent; Thies, Holger
2
2021
Formal proofs of Tarjan’s strongly connected components algorithm in Why3, Coq and Isabelle. Zbl 07649962
Chen, Ran; Cohen, Cyril; Lévy, Jean-Jacques; Merz, Stephan; Théry, Laurent
2
2019
Distant decimals of \(\pi \): formal proofs of some algorithms computing them and guarantees of exact computation. Zbl 1448.68455
Bertot, Yves; Rideau, Laurence; Théry, Laurent
1
2018
Computable analysis and notions of continuity in Coq. Zbl 07350782
Steinberg, Florian; Thery, Laurent; Thies, Holger
2
2021
Formal proofs of Tarjan’s strongly connected components algorithm in Why3, Coq and Isabelle. Zbl 07649962
Chen, Ran; Cohen, Cyril; Lévy, Jean-Jacques; Merz, Stephan; Théry, Laurent
2
2019
Distant decimals of \(\pi \): formal proofs of some algorithms computing them and guarantees of exact computation. Zbl 1448.68455
Bertot, Yves; Rideau, Laurence; Théry, Laurent
1
2018
Formally verified certificate checkers for hardest-to-round computation. Zbl 1315.68222
Martin-Dorel, Érik; Hanrot, Guillaume; Mayero, Micaela; Théry, Laurent
2
2015
Implementing geometric algebra products with binary trees. Zbl 1311.68147
Fuchs, Laurent; Théry, Laurent
9
2014
A machine-checked proof of the odd order theorem. Zbl 1317.68211
Gonthier, Georges; Asperti, Andrea; Avigad, Jeremy; Bertot, Yves; Cohen, Cyril; Garillot, François; Le Roux, Stéphane; Mahboubi, Assia; O’Connor, Russell; Ould Biha, Sidi; Pasca, Ioana; Rideau, Laurence; Solovyev, Alexey; Tassi, Enrico; Théry, Laurent
64
2013
A modular integration of SAT/SMT solvers to Coq through proof witnesses. Zbl 1350.68223
Armand, Michael; Faure, Germain; Grégoire, Benjamin; Keller, Chantal; Théry, Laurent; Werner, Benjamin
21
2011
A formalization of Grassmann-Cayley algebra in Coq and its application to theorem proving in projective geometry. Zbl 1350.68233
Fuchs, Laurent; Théry, Laurent
8
2011
Proof certificates for algebra and their application to automatic geometry theorem proving. Zbl 1302.68242
Grégoire, Benjamin; Pottier, Loïc; Théry, Laurent
8
2011
Extending Coq with imperative features and its application to SAT verification. Zbl 1291.68318
Armand, Michaël; Grégoire, Benjamin; Spiwack, Arnaud; Théry, Laurent
15
2010
A modular formalisation of finite group theory. Zbl 1144.68356
Gonthier, Georges; Mahboubi, Assia; Rideau, Laurence; Tassi, Enrico; Théry, Laurent
21
2007
Primality proving with elliptic curves. Zbl 1144.68367
Théry, Laurent; Hanrot, Guillaume
7
2007
A purely functional library for modular arithmetic and its application to certifying large prime numbers. Zbl 1222.68363
Grégoire, Benjamin; Théry, Laurent
6
2006
A computational approach to Pocklington certificates in type theory. Zbl 1185.68621
Grégoire, Benjamin; Théry, Laurent; Werner, Benjamin
5
2006
Proving pearl: Knuth’s algorithm for prime numbers. Zbl 1279.68298
Théry, Laurent
3
2003
A generic library for floating-point numbers and its application to exact computing. Zbl 1005.68544
Daumas, Marc; Rideau, Laurence; Théry, Laurent
18
2001
A machine-checked implementation of Buchberger’s algorithm. Zbl 0964.03012
Théry, Laurent
7
2001
Theorem proving in higher order logics. 12th international conference, TPHOLs ’99. Nice, France, September 14–17, 1999. Proceedings. Zbl 0929.00038
2
1999
A Skeptic’s approach to combining HOL and Maple. Zbl 0916.68142
Harrison, J.; Théry, L.
26
1998
A certified version of Buchberger’s algorithm. Zbl 0924.03025
Théry, Laurent
2
1998
Extracting text from proofs. Zbl 1063.68647
Coscoy, Yann; Kahn, Gilles; Théry, Laurent
3
1995
Proof by pointing. Zbl 0942.03504
Bertot, Yves; Kahn, Gilles; Théry, Laurent
4
1994
Reasoning about the reals: The marriage of HOL and Maple. Zbl 0793.68084
Harrison, John; Théry, Laurent
6
1993
all top 5

Cited by 368 Authors

9 Melquiond, Guillaume
7 Théry, Laurent
6 Asperti, Andrea
6 Boldo, Sylvie
6 Mahboubi, Assia
6 Narboux, Julien
6 Paulson, Lawrence Charles
6 Tahar, Sofiène
5 Cohen, Cyril
5 Sacerdoti Coen, Claudio
5 Schreck, Pascal
4 Affeldt, Reynald
4 Allamigeon, Xavier
4 Blanchette, Jasmin Christian
4 Doczkal, Christian
4 Kaliszyk, Cezary
4 Kohlhase, Michael
4 Rabe, Florian
4 Rideau, Laurence
4 Smolka, Gert
4 Tassi, Enrico
3 Armando, Alessandro
3 Avigad, Jeremy
3 Bertot, Yves
3 Böhme, Sascha
3 Breuils, Stéphane
3 Coquand, Thierry
3 Filliâtre, Jean-Christophe
3 Fleury, Mathias
3 Fuchs, Laurent
3 Gonthier, Georges
3 Heras, Jónathan
3 Janičić, Predrag
3 Katz, Ricardo David
3 Mayero, Micaela
3 Naumowicz, Adam
3 Nozick, Vincent
3 Ricciotti, Wilmer
3 Rouhling, Damien
3 Thies, Holger
2 Akbarpour, Behzad
2 Aransay, Jesús
2 Ballarin, Clemens
2 Barbosa, Haniel
2 Boutry, Pierre
2 Braibant, Thomas
2 Braun, Gabriel
2 Caprotti, Olga
2 Chan, Hing-Lun
2 Clément, François
2 Coghetto, Roland
2 Coglio, Alessandro
2 Cohen, Arjeh Marcel
2 Czajka, Łukasz
2 Divasón, Jose
2 Dumbrava, Stefania
2 Eid, Ahmad Hosny
2 Farmer, William M.
2 Giunchiglia, Fausto
2 Grégoire, Benjamin
2 Gunther, Emmanuel
2 Hales, Thomas Callister
2 Hasan, Osman
2 Kapulkin, Krzysztof
2 Khan Afshar, Sanaz
2 Komendantsky, Vladimir
2 Konovalov, Olexandr
2 Li, Liming
2 Li, Wenda
2 Linton, Stephen A.
2 Magaud, Nicolas
2 Magron, Victor
2 Malecha, Gregory
2 Maletzky, Alexander
2 Marché, Claude
2 Marić, Filip
2 Martin-Dorel, Érik
2 Monniaux, David P.
2 Muller, Jean-Michel
2 Nipkow, Tobias
2 Norrish, Michael
2 Oe, Duckki
2 Ould Biha, Sidi
2 Pagano, Miguel
2 Paşca, Ioana
2 Pous, Damien
2 Ranta, Aarne
2 Reynolds, Andrew
2 Roux, Pierre
2 Rubio García, Julio Jesús
2 Sakaguchi, Kazuhiko
2 Seddiki, Ons
2 Shankar, Natarajan
2 Sibut-Pinote, Thomas
2 Siddique, Umair
2 Solovyev, Alexey
2 Spitters, Bas
2 Steinberg, Florian
2 Stojanović Đurđević, Sana
2 Strub, Pierre-Yves
...and 268 more Authors

Citations by Year