Edit Profile (opens in new tab) Théry, Laurent Co-Author Distance Author ID: thery.laurent Published as: Théry, Laurent; Thery, Laurent; Théry, L. more...less Documents Indexed: 28 Publications since 1993 2 Contributions as Editor Co-Authors: 40 Co-Authors with 23 Joint Publications 609 Co-Co-Authors all top 5 Co-Authors 5 single-authored 5 Grégoire, Benjamin 4 Bertot, Yves 4 Rideau, Laurence 2 Armand, Michaël 2 Cohen, Cyril 2 Fuchs, Laurent 2 Gonthier, Georges 2 Hanrot, Guillaume 2 Kahn, Gilles 2 Mahboubi, Assia 2 Steinberg, Florian 2 Tassi, Enrico 2 Thies, Holger 2 Werner, Benjamin 1 Asperti, Andrea 1 Avigad, Jeremy 1 Blot, Arthur 1 Chen, Ran 1 Coscoy, Yann 1 Daumas, Marc 1 Dowek, Gilles 1 Faure, Germain 1 Felty, Amy P. 1 Garillot, François 1 Hirschowitz, André 1 Keller, Chantal 1 Leroux, Stéphane 1 Letouzey, Pierre 1 Levy, Jean-Jacques 1 Martin-Dorel, Érik 1 Mayero, Micaela 1 Muller, Jean-Michel 1 O’Connor, Russell 1 Ould Biha, Sidi 1 Paşca, Ioana 1 Paulin, Christine 1 Pottier, Loïc 1 Solovyev, Alexey 1 Spiwack, Arnaud 1 Wiedijk, Freek all top 5 Serials 4 Journal of Automated Reasoning 1 Journal of Symbolic Computation 1 Advances in Applied Clifford Algebras 1 Lecture Notes in Computer Science 1 Mathematics in Computer Science 1 Logical Methods in Computer Science all top 5 Fields 30 Computer science (68-XX) 9 Mathematical logic and foundations (03-XX) 6 Number theory (11-XX) 4 Numerical analysis (65-XX) 2 General and overarching topics; collections (00-XX) 2 Group theory and generalizations (20-XX) 1 Commutative algebra (13-XX) 1 Linear and multilinear algebra; matrix theory (15-XX) 1 Geometry (51-XX) Publications by Year all cited Publications top 5 cited Publications 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 cited Publications top 5 cited Publications 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 all top 5 Cited in 40 Serials 37 Journal of Automated Reasoning 14 Journal of Symbolic Computation 9 MSCS. Mathematical Structures in Computer Science 7 Formal Methods in System Design 7 Advances in Applied Clifford Algebras 6 Mathematics in Computer Science 4 Annals of Mathematics and Artificial Intelligence 3 Theoretical Computer Science 3 Annals of Pure and Applied Logic 3 Logical Methods in Computer Science 3 Journal of Formalized Reasoning 2 Artificial Intelligence 2 Synthese 2 Information and Computation 2 Formal Aspects of Computing 2 Experimental Mathematics 2 Formalized Mathematics 2 Philosophical Transactions of the Royal Society of London. A. Mathematical, Physical and Engineering Sciences 1 Acta Informatica 1 Computers & Mathematics with Applications 1 The Mathematical Intelligencer 1 ACM Transactions on Mathematical Software 1 BIT 1 Journal of Mathematical Economics 1 Science of Computer Programming 1 Computational Geometry 1 Bulletin of the American Mathematical Society. New Series 1 Indagationes Mathematicae. New Series 1 Applicable Algebra in Engineering, Communication and Computing 1 Journal of Functional Programming 1 Higher-Order and Symbolic Computation 1 Theory and Practice of Logic Programming 1 JP Journal of Algebra, Number Theory and Applications 1 ACM Transactions on Computational Logic 1 Journal of Applied Logic 1 Acta Numerica 1 Groups, Complexity, Cryptology 1 The Review of Symbolic Logic 1 Forum of Mathematics, Pi 1 Journal of Membrane Computing all top 5 Cited in 30 Fields 193 Computer science (68-XX) 56 Mathematical logic and foundations (03-XX) 17 Numerical analysis (65-XX) 11 Number theory (11-XX) 9 Commutative algebra (13-XX) 9 Linear and multilinear algebra; matrix theory (15-XX) 9 Geometry (51-XX) 7 General and overarching topics; collections (00-XX) 5 Category theory; homological algebra (18-XX) 5 Algebraic topology (55-XX) 4 Field theory and polynomials (12-XX) 4 Algebraic geometry (14-XX) 4 Real functions (26-XX) 3 Group theory and generalizations (20-XX) 2 Special functions (33-XX) 2 Partial differential equations (35-XX) 2 Convex and discrete geometry (52-XX) 2 Operations research, mathematical programming (90-XX) 2 Game theory, economics, finance, and other social and behavioral sciences (91-XX) 2 Information and communication theory, circuits (94-XX) 2 Mathematics education (97-XX) 1 History and biography (01-XX) 1 Order, lattices, ordered algebraic structures (06-XX) 1 Associative rings and algebras (16-XX) 1 Functions of a complex variable (30-XX) 1 Ordinary differential equations (34-XX) 1 Functional analysis (46-XX) 1 Optics, electromagnetic theory (78-XX) 1 Quantum theory (81-XX) 1 Systems theory; control (93-XX) Citations by Year