×
Author ID: bertot.yves Recent zbMATH articles by "Bertot, Yves"
Published as: Bertot, Yves
Homepage: https://www-sop.inria.fr/members/Yves.Bertot/
External Links: ORCID · ResearchGate · dblp
all top 5

Co-Authors

9 single-authored
4 Théry, Laurent
3 Gonthier, Georges
3 Mahboubi, Assia
2 Appel, Andrew W.
2 Avigad, Jeremy
2 Cohen, Cyril
2 Komendantskaya, Ekaterina
2 Magaud, Nicolas
2 Ould Biha, Sidi
2 Paşca, Ioana
1 Aczel, Peter
1 Ahrens, Benedikt
1 Allais, Guillaume
1 Altenkirch, Thorsten
1 Angiuli, Carlo
1 Asperti, Andrea
1 Awodey, Steve
1 Balaa, Antonia
1 Barman, Kuntal Das
1 Barras, Bruno
1 Bauer, Andrej
1 Bertot, Janet
1 Bezem, Marc
1 Bordg, Anthony
1 Brunerie, Guillaume
1 Capretta, Venanzio
1 Casteran, Pierre
1 Constable, Robert Lee
1 Coquand, Thierry
1 Curien, Pierre-Louis
1 Dowek, Gilles
1 Dufourd, Jean-François
1 Dybjer, Peter
1 Finster, Eric
1 Gambino, Nicola
1 Garillot, François
1 Garner, Richard
1 Grayson, Daniel Richard
1 Grégoire, Benjamin
1 Guilhot, Frédérique
1 Hales, Thomas Callister
1 Harper, Robert
1 Herbelin, Hugo
1 Hirschowitz, André
1 Hofmann, Martin
1 Hofstra, Pieter J. W.
1 Hötzel Escardó, Martín
1 Hou (Favonia), Kuen-Bang
1 Huet, Gerard P.
1 Joyal, André
1 Kahn, Gilles
1 Kapulkin, Krzysztof
1 Kock, Joachim
1 Kraus, Nicolai
1 Leroux, Stéphane
1 Leroy, Xavier
1 Levy, Jean-Jacques
1 Li, Nuo
1 Licata, Dan
1 Lumsdaine, Peter LeFanu
1 Luo, Zhaohui
1 Martin-Löf, Per
1 Melikhov, Sergey Aleksandrovich
1 Nahas, Michael
1 Niqui, Milad
1 O’Connor, Russell
1 Palmgren, Erik
1 Paulin, Christine
1 Pelayo, Alvaro
1 Pham, Tuan Minh
1 Pichardie, David
1 Plotkin, Gordon D.
1 Polonsky, Andrew
1 Rideau, Laurence
1 Rideau, Laurence
1 Riehl, Emily
1 Rijke, Egbert
1 Scott, Dana Stewart
1 Scott, Philip J.
1 Shulman, Michael A.
1 Sojakova, Kristina
1 Solov’ëv, Sergeĭ Vladimirovich
1 Solovyev, Alexey
1 Sozeau, Matthieu
1 Spitters, Bas
1 Tassi, Enrico
1
1 Van den Berg, Benno
1 Voevodskiĭ, Vladimir Aleksandrovich
1 Warren, Michael Alton
1 Zeilberger, Noam
1 Zimmermann, Paul

Publications by Year

Citations contained in zbMATH Open

29 Publications have been cited 447 times in 387 Documents Cited by Year
Interactive theorem proving and program development. Coq’Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring. Zbl 1069.68095
Bertot, Yves; Castéran, Pierre
265
2004
Homotopy type theory. Univalent foundations of mathematics. Zbl 1298.03002
The Univalent Foundations Program
129
2013
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
59
2013
Canonical big operators. Zbl 1165.68450
Bertot, Yves; Gonthier, Georges; Ould Biha, Sidi; Pasca, Ioana
22
2008
Formalizing convex hull algorithms. Zbl 1005.68557
Pichardie, David; Bertot, Yves
13
2001
Inductive and coinductive components of corecursive functions in Coq. Zbl 1279.68285
Bertot, Yves; Komendantskaya, Ekaterina
10
2008
Affine functions and series with co-inductive real numbers. Zbl 1120.68095
Bertot, Yves
8
2007
A short presentation of Coq. Zbl 1165.68449
Bertot, Yves
8
2008
Filters on coinductive streams, an application to Eratosthenes’ sieve. Zbl 1114.68062
Bertot, Yves
7
2005
A structured approach to proving compiler optimizations based on dataflow analysis. Zbl 1172.68414
Bertot, Yves; Grégoire, Benjamin; Leroy, Xavier
7
2006
A proof of GMP square root. Zbl 1064.68093
Bertot, Yves; Magaud, Nicolas; Zimmermann, Paul
5
2002
Formal study of plane Delaunay triangulation. Zbl 1291.68337
Dufourd, Jean-François; Bertot, Yves
5
2010
A formal study of Bernstein coefficients and polynomials. Zbl 1236.33016
Bertot, Yves; Guilhot, Frédérique; Mahboubi, Assia
5
2011
Fix-point equations for well-founded recursion in type theory. Zbl 0974.68183
Balaa, Antonia; Bertot, Yves
4
2000
Proof by pointing. Zbl 0942.03504
Bertot, Yves; Kahn, Gilles; Théry, Laurent
4
1994
Using structural recursion for corecursion. Zbl 1246.68196
Bertot, Yves; Komendantskaya, Ekaterina
4
2009
QArith: Coq formalisation of lazy rational arithmetic. Zbl 1100.68619
Niqui, Milad; Bertot, Yves
3
2004
Changing data structures in type theory: A study of natural numbers. Zbl 1054.03500
Magaud, Nicolas; Bertot, Yves
2
2002
A combination of a dynamic geometry software with a proof assistant for interactive formal proofs. Zbl 1294.68126
Pham, Tuan Minh; Bertot, Yves
2
2012
Theorem-proving support in programming language semantics. Zbl 1195.68090
Bertot, Yves
2
2009
C-language floating-point proofs layered with VST and Flocq. Zbl 1508.68032
Appel, Andrew W.; Bertot, Yves
2
2020
Structural abstract interpretation: a formal study using Coq. Zbl 1250.68089
Bertot, Yves
2
2009
Formalizing a JVML verifier for initialization in a theorem prover. Zbl 0991.68508
Bertot, Yves
2
2001
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
Une automatisation du calcul des résidus en sémantique naturelle. (An automatization of residual computation in natural semantics.) Zbl 0851.68030
Bertot, Yves
1
1991
From semantics to computer science. Essays in honour of Gilles Kahn. Zbl 1177.68004
1
2009
Theorem proving in higher order logics. 12th international conference, TPHOLs ’99. Nice, France, September 14–17, 1999. Proceedings. Zbl 0929.00038
1
1999
Formal verification of a geometry algorithm: a quest for abstract views and symmetry in Coq proofs. Zbl 1518.68417
Bertot, Yves
1
2018
A simple canonical representation of rational numbers. Zbl 1264.68158
Bertot, Yves
1
2003
C-language floating-point proofs layered with VST and Flocq. Zbl 1508.68032
Appel, Andrew W.; Bertot, Yves
2
2020
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
Formal verification of a geometry algorithm: a quest for abstract views and symmetry in Coq proofs. Zbl 1518.68417
Bertot, Yves
1
2018
Homotopy type theory. Univalent foundations of mathematics. Zbl 1298.03002
The Univalent Foundations Program
129
2013
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
59
2013
A combination of a dynamic geometry software with a proof assistant for interactive formal proofs. Zbl 1294.68126
Pham, Tuan Minh; Bertot, Yves
2
2012
A formal study of Bernstein coefficients and polynomials. Zbl 1236.33016
Bertot, Yves; Guilhot, Frédérique; Mahboubi, Assia
5
2011
Formal study of plane Delaunay triangulation. Zbl 1291.68337
Dufourd, Jean-François; Bertot, Yves
5
2010
Using structural recursion for corecursion. Zbl 1246.68196
Bertot, Yves; Komendantskaya, Ekaterina
4
2009
Theorem-proving support in programming language semantics. Zbl 1195.68090
Bertot, Yves
2
2009
Structural abstract interpretation: a formal study using Coq. Zbl 1250.68089
Bertot, Yves
2
2009
From semantics to computer science. Essays in honour of Gilles Kahn. Zbl 1177.68004
1
2009
Canonical big operators. Zbl 1165.68450
Bertot, Yves; Gonthier, Georges; Ould Biha, Sidi; Pasca, Ioana
22
2008
Inductive and coinductive components of corecursive functions in Coq. Zbl 1279.68285
Bertot, Yves; Komendantskaya, Ekaterina
10
2008
A short presentation of Coq. Zbl 1165.68449
Bertot, Yves
8
2008
Affine functions and series with co-inductive real numbers. Zbl 1120.68095
Bertot, Yves
8
2007
A structured approach to proving compiler optimizations based on dataflow analysis. Zbl 1172.68414
Bertot, Yves; Grégoire, Benjamin; Leroy, Xavier
7
2006
Filters on coinductive streams, an application to Eratosthenes’ sieve. Zbl 1114.68062
Bertot, Yves
7
2005
Interactive theorem proving and program development. Coq’Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring. Zbl 1069.68095
Bertot, Yves; Castéran, Pierre
265
2004
QArith: Coq formalisation of lazy rational arithmetic. Zbl 1100.68619
Niqui, Milad; Bertot, Yves
3
2004
A simple canonical representation of rational numbers. Zbl 1264.68158
Bertot, Yves
1
2003
A proof of GMP square root. Zbl 1064.68093
Bertot, Yves; Magaud, Nicolas; Zimmermann, Paul
5
2002
Changing data structures in type theory: A study of natural numbers. Zbl 1054.03500
Magaud, Nicolas; Bertot, Yves
2
2002
Formalizing convex hull algorithms. Zbl 1005.68557
Pichardie, David; Bertot, Yves
13
2001
Formalizing a JVML verifier for initialization in a theorem prover. Zbl 0991.68508
Bertot, Yves
2
2001
Fix-point equations for well-founded recursion in type theory. Zbl 0974.68183
Balaa, Antonia; Bertot, Yves
4
2000
Theorem proving in higher order logics. 12th international conference, TPHOLs ’99. Nice, France, September 14–17, 1999. Proceedings. Zbl 0929.00038
1
1999
Proof by pointing. Zbl 0942.03504
Bertot, Yves; Kahn, Gilles; Théry, Laurent
4
1994
Une automatisation du calcul des résidus en sémantique naturelle. (An automatization of residual computation in natural semantics.) Zbl 0851.68030
Bertot, Yves
1
1991
all top 5

Cited by 678 Authors

8 Bertot, Yves
8 Leroy, Xavier
8 Melquiond, Guillaume
8 Popescu, Andrei
7 Boldo, Sylvie
7 Dufourd, Jean-François
6 Berger, Ulrich
6 Kaliszyk, Cezary
6 Narboux, Julien
6 Paulson, Lawrence Charles
6 Rabe, Florian
6 Schneider-Kamp, Peter
6 Théry, Laurent
5 Affeldt, Reynald
5 Asperti, Andrea
5 Blanchette, Jasmin Christian
5 Cruz-Filipe, Luís
5 Duan, Zhenhua
5 Kunčar, Ondřej
5 Miller, Dale Allen
5 Moreira, Nelma
5 Nipkow, Tobias
5 Sacerdoti Coen, Claudio
5 Urban, Josef
5 Zhang, Nan
4 Avigad, Jeremy
4 Bove, Ana
4 Cohen, Liron
4 Constable, Robert Lee
4 Danvy, Olivier
4 Fuchs, Laurent
4 Heras, Jónathan
4 Kohlhase, Michael
4 Komendantskaya, Ekaterina
4 Magaud, Nicolas
4 Mayero, Micaela
4 Pereira, David P.
4 Pichardie, David
4 Tassi, Enrico
4 Tian, Cong
3 Aransay, Jesús
3 Bentkamp, Alexander
3 Bickford, Mark
3 Blazy, Sandrine
3 Clément, François
3 Cohen, Cyril
3 Dybjer, Peter
3 Filliâtre, Jean-Christophe
3 Gonthier, Georges
3 Janičić, Predrag
3 Jebelean, Tudor
3 Kosmatov, Nikolai
3 Kumar, Ramana
3 Lescanne, Pierre
3 Mahboubi, Assia
3 Melo de Sousa, Simão
3 Muñoz, César A.
3 Nadathur, Gopalan
3 Niqui, Milad
3 Paşca, Ioana
3 Quaresma, Pedro
3 Ricciotti, Wilmer
3 Rideau, Laurence
3 Rubio García, Julio Jesús
3 Rusu, Vlad
3 Spitters, Bas
3 Traytel, Dmitry
3 Weber, Tjark
2 Appel, Andrew W.
2 Ayala-Rincón, Mauricio
2 Bacelar Almeida, José
2 Benzmüller, Christoph Ewald
2 Berghammer, Rudolf
2 Böhme, Sascha
2 Brady, Edwin C.
2 Braun, David J.
2 Cachera, David
2 Capretta, Venanzio
2 Cho, Kenta
2 Chollet, Agathe
2 Coquand, Thierry
2 Czajka, Łukasz
2 Dargaye, Zaynah
2 de Moura, Leonardo
2 Dehlinger, Christophe
2 Doczkal, Christian
2 Domínguez, César
2 Dubois, Catherine
2 Dumbrava, Stefania
2 Dutle, Aaron M.
2 Faissole, Florian
2 Farmer, William M.
2 Felsner, Stefan
2 Felty, Amy P.
2 Gacek, Andrew
2 Gransden, Thomas
2 Hales, Thomas Callister
2 Hasuo, Ichiro
2 Horozal, Fulya
2 Kammüller, Florian
...and 578 more Authors
all top 5

Cited in 58 Serials

69 Journal of Automated Reasoning
21 Theoretical Computer Science
16 MSCS. Mathematical Structures in Computer Science
11 Journal of Functional Programming
9 Journal of Symbolic Computation
8 Formal Aspects of Computing
8 Annals of Mathematics and Artificial Intelligence
8 Journal of Logical and Algebraic Methods in Programming
7 Mathematics in Computer Science
5 Journal of Applied Logic
3 Information and Computation
3 Computational Geometry
3 Theory of Computing Systems
3 Higher-Order and Symbolic Computation
3 ACM Transactions on Computational Logic
3 Journal of Formalized Reasoning
2 Artificial Intelligence
2 Synthese
2 Science of Computer Programming
2 Annals of Pure and Applied Logic
2 Bulletin of the American Mathematical Society. New Series
2 Applicable Algebra in Engineering, Communication and Computing
2 Experimental Mathematics
2 Journal of Combinatorial Optimization
2 The Journal of Logic and Algebraic Programming
2 Logical Methods in Computer Science
2 Philosophical Transactions of the Royal Society of London. A. Mathematical, Physical and Engineering Sciences
1 Acta Informatica
1 Computers & Mathematics with Applications
1 International Journal of General Systems
1 Information Processing Letters
1 Jahresbericht der Deutschen Mathematiker-Vereinigung (DMV)
1 The Mathematical Intelligencer
1 BIT
1 Journal of Computer and System Sciences
1 Journal of Mathematical Economics
1 Mathematics and Computers in Simulation
1 Algorithmica
1 Journal of the American Mathematical Society
1 International Journal of Computer Mathematics
1 Pattern Recognition
1 Indagationes Mathematicae. New Series
1 Formal Methods in System Design
1 Journal of Applied Non-Classical Logics
1 Advances in Applied Clifford Algebras
1 The Electronic Journal of Combinatorics
1 RAIRO. Theoretical Informatics and Applications
1 Theory and Practice of Logic Programming
1 Sādhanā
1 JP Journal of Algebra, Number Theory and Applications
1 Computer Languages, Systems & Structures
1 Journal of Discrete Algorithms
1 The Review of Symbolic Logic
1 European Journal for Philosophy of Science
1 Forum of Mathematics, Pi
1 Computer Science Review
1 Proceedings of the Royal Society of London. A. Mathematical, Physical and Engineering Sciences
1 Journal of Membrane Computing

Citations by Year