default search action
Google
Google Scholar
Semantic Scholar
Internet Archive Scholar
CiteSeerX
ORCIDYves Bertot
Person information
Refine list
refinements active!
zoomed in on ?? of ?? records
view refined list in
export refined list as
Books and Theses
- 2004
[b1]Yves Bertot, Pierre Castéran:
Interactive Theorem Proving and Program Development - Coq'Art: The Calculus of Inductive Constructions. Texts in Theoretical Computer Science. An EATCS Series, Springer 2004, ISBN 978-3-642-05880-6, pp. 1-472
Journal Articles
- 2020
- [j11]Andrew W. Appel
, Yves Bertot:
C floating-point proofs layered with VST and Flocq. J. Formaliz. Reason. 13(1): 1-16 (2020) - [j10]Andrew W. Appel, Yves Bertot:
Corrigendum: C floating-point proofs layered with VST and Flocq. J. Formaliz. Reason. 13(1) (2020) - 2018
- [j9]Yves Bertot, Laurence Rideau, Laurent Théry:
Distant Decimals of π : Formal Proofs of Some Algorithms Computing Them and Guarantees of Exact Computation. J. Autom. Reason. 61(1-4): 33-71 (2018) - 2014
- [j8]Yves Bertot, Guillaume Allais:
Views of PI: Definition and computation. J. Formaliz. Reason. 7(1): 105-129 (2014) - 2011
- [j7]Yves Bertot, Frédérique Guilhot, Assia Mahboubi:
A formal study of Bernstein coefficients and polynomials. Math. Struct. Comput. Sci. 21(4): 731-761 (2011) - 2007
- [j6]Yves Bertot:
Affine functions and series with co-inductive real numbers. Math. Struct. Comput. Sci. 17(1): 37-63 (2007) - 2005
- [j5]Yves Bertot:
Vérification formelle d'extractions de racines entières. Tech. Sci. Informatiques 24(9): 1161-1185 (2005) - 2002
- [j4]Yves Bertot, Nicolas Magaud, Paul Zimmermann:
A Proof of GMP Square Root. J. Autom. Reason. 29(3-4): 225-252 (2002) - 1999
- [j3]Yves Bertot, Laurence Rideau, Loïc Pottier, Laurent Thiry:
CtCoq: an environment for mathematical reasoning. SIGSAM Bull. 33(3): 21-22 (1999) - [j2]Yves Bertot:
The CtCoq System: Design and Architecture. Formal Aspects Comput. 11(3): 225-243 (1999) - 1998
- [j1]Yves Bertot, Laurent Théry:
A Generic Approach to Building User Interfaces for Theorem Provers. J. Symb. Comput. 25(2): 161-194 (1998)
Conference and Workshop Papers
- 2024
- [c36]Yves Bertot:
Safe Smooth Paths Between Straight Line Obstacles. Logics and Type Systems in Theory and Practice 2024: 36-53 - 2018
- [c35]Yves Bertot:
Formal Verification of a Geometry Algorithm: A Quest for Abstract Views and Symmetry in Coq Proofs. ICTAC 2018: 3-10 - 2016
- [c34]Sophie Bernard, Yves Bertot, Laurence Rideau, Pierre-Yves Strub:
Formal proofs of transcendence for e and pi as an application of multivariate and symmetric polynomials. CPP 2016: 76-87 - 2015
- [c33]Yves Bertot:
Fixed Precision Patterns for the Formal Verification of Mathematical Constant Approximations. CPP 2015: 147-155 - 2013
- [c32]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:
A Machine-Checked Proof of the Odd Order Theorem. ITP 2013: 163-179 - 2011
- [c31]Tuan-Minh Pham, Yves Bertot, Julien Narboux:
A Coq-Based Library for Interactive and Automated Theorem Proving in Plane Geometry. ICCSA (4) 2011: 368-383 - 2010
- [c30]Jean-François Dufourd, Yves Bertot:
Formal Study of Plane Delaunay Triangulation. ITP 2010: 211-226 - [c29]Tuan-Minh Pham, Yves Bertot:
A Combination of a Dynamic Geometry Software With a Proof Assistant for Interactive Formal Proofs. UITP 2010: 43-55 - 2009
- [c28]Maxime Dénès, Benjamin Lesage, Yves Bertot, Adrien Richard:
Formal Proof of Theorems on Genetic Regulatory Networks. SYNASC 2009: 69-76 - 2008
- [c27]Yves Bertot:
Structural Abstract Interpretation: A Formal Study Using Coq. LerNet ALFA Summer School 2008: 153-194 - [c26]Yves Bertot, Vladimir Komendantsky:
Fixed point semantics and partial recursion in Coq. PPDP 2008: 89-96 - [c25]Yves Bertot:
A Short Presentation of Coq. TPHOLs 2008: 12-16 - [c24]Yves Bertot, Georges Gonthier, Sidi Ould Biha, Ioana Pasca:
Canonical Big Operators. TPHOLs 2008: 86-101 - [c23]Yves Bertot, Ekaterina Komendantskaya:
Using Structural Recursion for Corecursion. TYPES 2008: 220-236 - [c22]Yves Bertot, Ekaterina Komendantskaya:
Inductive and Coinductive Components of Corecursive Functions in Coq. CMCS 2008: 25-47 - 2005
- [c21]Yves Bertot:
Filters on CoInductive Streams, an Application to Eratosthenes' Sieve. TLCA 2005: 102-115 - [c20]Yves Bertot, Laurent Théry:
Dependent Types, Theorem Proving, and Applications for a Verifying Compiler. VSTTE 2005: 173-181 - 2004
- [c19]Yves Bertot, Benjamin Grégoire, Xavier Leroy:
A Structured Approach to Proving Compiler Optimizations Based on Dataflow Analysis. TYPES 2004: 66-81 - 2003
- [c18]Milad Niqui, Yves Bertot:
QArith: Coq Formalisation of Lazy Rational Arithmetic. TYPES 2003: 309-323 - [c17]Yves Bertot:
Simple canonical representation of rational numbers. Mathematics, Logic and Computation @ ICALP 2003: 1-16 - [c16]Yves Bertot, Frédérique Guilhot, Loic Pottier:
Visualizing Geometrical Statements with GeoView. UITP@TPHOLs 2003: 49-65 - 2002
- [c15]Yves Bertot, Venanzio Capretta, Kuntal Das Barman:
Type-Theoretic Functional Semantics. TPHOLs 2002: 83-98 - 2001
- [c14]Yves Bertot:
Formalizing a JVML Verifier for Initialization in a Theorem Prover. CAV 2001: 14-24 - [c13]Nicolas Magaud, Yves Bertot:
Changement de représentation des structures de données en Coq: le cas des entiers naturels. JFLA 2001: 1-16 - [c12]David Pichardie, Yves Bertot:
Formalizing Convex Hull Algorithms. TPHOLs 2001: 346-361 - 2000
- [c11]Antonia Balaa, Yves Bertot:
Fix-Point Equations for Well-Founded Recursion in Type Theory. TPHOLs 2000: 1-16 - [c10]Nicolas Magaud, Yves Bertot:
Changing Data Structures in Type Theory: A Study of Natural Numbers. TYPES 2000: 181-196 - 1997
- [c9]Yves Bertot:
Head-Tactics Simplification. AMAST 1997: 16-29 - 1996
- [c8]Janet Bertot, Yves Bertot:
CtCoq: A System Presentation. AMAST 1996: 600-603 - [c7]Janet Bertot, Yves Bertot:
CtCoq: A System Presentation. CADE 1996: 231-234 - 1995
- [c6]Yves Bertot, Ranan Fraer:
Reasoning with Executable Specifications. TAPSOFT 1995: 531-545 - 1994
- [c5]Yves Bertot, Gilles Kahn, Laurent Théry:
Proof by Pointing. TACS 1994: 141-160 - 1992
- [c4]Yves Bertot:
Origin Functions in Lambda-Calculus and Term Rewriting Systems. CAAP 1992: 49-65 - [c3]Laurent Théry, Yves Bertot, Gilles Kahn:
Real theorem provers deserve real user-interfaces. SDE 1992: 120-129 - 1991
- [c2]Yves Bertot:
Occurences in Debugger Specifications. PLDI 1991: 327-337 - 1990
- [c1]Yves Bertot:
Implementation of an Interpreter for a Parallel Language in Centaur. ESOP 1990: 57-69
Editorship
- 2024
- [e3]Yves Bertot, Temur Kutsia, Michael Norrish:
15th International Conference on Interactive Theorem Proving, ITP 2024, September 9-14, 2024, Tbilisi, Georgia. LIPIcs 309, Schloss Dagstuhl - Leibniz-Zentrum für Informatik 2024, ISBN 978-3-95977-337-9 [contents] - 2017
- [e2]Yves Bertot, Viktor Vafeiadis:
Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs, CPP 2017, Paris, France, January 16-17, 2017. ACM 2017, ISBN 978-1-4503-4705-1 [contents] - 1999
- [e1]Yves Bertot, Gilles Dowek, André Hirschowitz, Christine Paulin-Mohring, Laurent Théry:
Theorem Proving in Higher Order Logics, 12th International Conference, TPHOLs'99, Nice, France, September, 1999, Proceedings. Lecture Notes in Computer Science 1690, Springer 1999, ISBN 3-540-66463-7 [contents]
Informal and Other Publications
- 2018
- [i12]Yves Bertot:
Formal Verification of a Geometry Algorithm: A Quest for Abstract Views and Symmetry in Coq Proofs. CoRR abs/1809.00559 (2018) - 2017
- [i11]Yves Bertot, Laurence Rideau, Laurent Théry:
Distant decimals of $π$. CoRR abs/1709.01743 (2017) - 2015
- [i10]Sophie Bernard, Yves Bertot, Laurence Rideau, Pierre-Yves Strub:
Formal Proofs of Transcendence for e and $π$ as an Application of Multivariate and Symmetric Polynomials. CoRR abs/1512.02791 (2015) - 2010
- [i9]Jean-François Dufourd, Yves Bertot:
Formal study of plane Delaunay triangulation. CoRR abs/1007.3350 (2010) - 2009
- [i8]Yves Bertot, Ekaterina Komendantskaya:
Using Structural Recursion for Corecursion. CoRR abs/0903.3850 (2009) - 2008
- [i7]Yves Bertot, Ekaterina Komendantskaya:
Inductive and Coinductive Components of Corecursive Functions in Coq. CoRR abs/0807.1524 (2008) - [i6]Yves Bertot:
Structural abstract interpretation, A formal study using Coq. CoRR abs/0810.2179 (2008) - 2007
- [i5]Yves Bertot:
Theorem proving support in programming language semantics. CoRR abs/0707.0926 (2007) - 2006
- [i4]Yves Bertot:
Affine functions and series with co-inductive real numbers. CoRR abs/cs/0603117 (2006) - [i3]Yves Bertot:
Coq in a Hurry. CoRR abs/cs/0603118 (2006) - [i2]Yves Bertot:
CoInduction in Coq. CoRR abs/cs/0603119 (2006) - [i1]Yves Bertot:
Extending the Calculus of Constructions with Tarski's fix-point theorem. CoRR abs/cs/0610055 (2006)
Coauthor Index
manage site settings
To protect your privacy, all features that rely on external API calls from your browser are turned off by default. You need to opt-in for them to become active. All settings here will be stored as cookies with your web browser. For more information see our F.A.Q.
Unpaywalled article links
Add open access links from 
to the list of external document links (if available).
Privacy notice: By enabling the option above, your browser will contact the API of unpaywall.org to load hyperlinks to open access articles. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Unpaywall privacy policy.
Archived links via Wayback Machine
For web page which are no longer available, try to retrieve content from the 
of the Internet Archive (if available).
Privacy notice: By enabling the option above, your browser will contact the API of archive.org to check for archived content of web pages that are no longer available. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Internet Archive privacy policy.
Reference lists
Add a list of references from 
, 
, and 
to record detail pages.
load references from crossref.org and opencitations.net
Privacy notice: By enabling the option above, your browser will contact the APIs of crossref.org, opencitations.net, and semanticscholar.org to load article reference information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Crossref privacy policy and the OpenCitations privacy policy, as well as the AI2 Privacy Policy covering Semantic Scholar.
Citation data
Add a list of citing articles from and to record detail pages.
load citations from opencitations.net
Privacy notice: By enabling the option above, your browser will contact the API of opencitations.net and semanticscholar.org to load citation information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the OpenCitations privacy policy as well as the AI2 Privacy Policy covering Semantic Scholar.
OpenAlex data
Load additional information about publications from 
.
Privacy notice: By enabling the option above, your browser will contact the API of openalex.org to load additional information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the information given by OpenAlex.
last updated on 2024-09-04 00:28 CEST by the dblp team
all metadata released as open data under CC0 1.0 license
see also: Terms of Use | Privacy Policy | Imprint
dblp was originally created in 1993 at:
since 2018, dblp has been operated and maintained by:
the dblp computer science bibliography is funded and supported by:
