Google
Google Scholar
MS Academic
CiteSeerX
CORE
Semantic ScholarYves Bertot
Refine list
refinements active!
zoomed in on ?? of ?? records
view refined list in
export refined list as
2010 – 2019
- 2018
[j12]Yves Bertot
, Laurence Rideau, Laurent Théry:
Distant Decimals of π : Formal Proofs of Some Algorithms Computing Them and Guarantees of Exact Computation. J. Autom. Reasoning 61(1-4): 33-71 (2018)- [c32]Yves Bertot:
Formal Verification of a Geometry Algorithm: A Quest for Abstract Views and Symmetry in Coq Proofs. ICTAC 2018: 3-10 - [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
- [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] - [i11]Yves Bertot, Laurence Rideau, Laurent Théry:
Distant decimals of $π$. CoRR abs/1709.01743 (2017) - 2016
- [c31]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
- [c30]Yves Bertot:
Fixed Precision Patterns for the Formal Verification of Mathematical Constant Approximations. CPP 2015: 147-155 - [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) - 2014
- [j11]Yves Bertot, Guillaume Allais:
Views of PI: Definition and computation. J. Formalized Reasoning 7(1): 105-129 (2014) - 2013
- [c29]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 - 2012
- [j10]Tuan-Minh Pham, Yves Bertot:
A Combination of a Dynamic Geometry Software With a Proof Assistant for Interactive Formal Proofs. Electron. Notes Theor. Comput. Sci. 285: 43-55 (2012) - 2011
- [j9]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) - [c28]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
- [c27]Jean-François Dufourd, Yves Bertot:
Formal Study of Plane Delaunay Triangulation. ITP 2010: 211-226 - [i9]Jean-François Dufourd, Yves Bertot:
Formal study of plane Delaunay triangulation. CoRR abs/1007.3350 (2010)
2000 – 2009
- 2009
- [c26]Maxime Dénès, Benjamin Lesage, Yves Bertot, Adrien Richard:
Formal Proof of Theorems on Genetic Regulatory Networks. SYNASC 2009: 69-76 - [i8]Yves Bertot, Ekaterina Komendantskaya:
Using Structural Recursion for Corecursion. CoRR abs/0903.3850 (2009) - 2008
- [c25]Yves Bertot:
Structural Abstract Interpretation: A Formal Study Using Coq. LerNet ALFA Summer School 2008: 153-194 - [c24]Yves Bertot, Vladimir Komendantsky:
Fixed point semantics and partial recursion in Coq. PPDP 2008: 89-96 - [c23]Yves Bertot:
A Short Presentation of Coq. TPHOLs 2008: 12-16 - [c22]Yves Bertot, Georges Gonthier, Sidi Ould Biha, Ioana Pasca:
Canonical Big Operators. TPHOLs 2008: 86-101 - [c21]Yves Bertot, Ekaterina Komendantskaya:
Using Structural Recursion for Corecursion. TYPES 2008: 220-236 - [c20]Yves Bertot, Ekaterina Komendantskaya:
Inductive and Coinductive Components of Corecursive Functions in Coq. CMCS 2008: 25-47 - [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
- [j8]Yves Bertot:
Affine functions and series with co-inductive real numbers. Math. Struct. Comput. Sci. 17(1): 37-63 (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) - 2005
- [j7]Yves Bertot:
Vérification formelle d'extractions de racines entières. Technique et Science Informatiques 24(9): 1161-1185 (2005) - [c19]Yves Bertot:
Filters on CoInductive Streams, an Application to Eratosthenes' Sieve. TLCA 2005: 102-115 - [c18]Yves Bertot, Laurent Théry:
Dependent Types, Theorem Proving, and Applications for a Verifying Compiler. VSTTE 2005: 173-181 - 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 - [j6]Yves Bertot, Frédérique Guilhot, Loic Pottier:
Visualizing Geometrical Statements with GeoView. Electron. Notes Theor. Comput. Sci. 103: 49-65 (2004) - [c17]Yves Bertot, Benjamin Grégoire, Xavier Leroy:
A Structured Approach to Proving Compiler Optimizations Based on Dataflow Analysis. TYPES 2004: 66-81 - 2003
- [j5]Yves Bertot:
Simple canonical representation of rational numbers. Electron. Notes Theor. Comput. Sci. 85(7): 1-16 (2003) - [c16]Milad Niqui, Yves Bertot:
QArith: Coq Formalisation of Lazy Rational Arithmetic. TYPES 2003: 309-323 - 2002
- [j4]Yves Bertot, Nicolas Magaud, Paul Zimmermann:
A Proof of GMP Square Root. J. Autom. Reasoning 29(3-4): 225-252 (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
1990 – 1999
- 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 Asp. Comput. 11(3): 225-243 (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] - 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) - 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
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).
load content from web.archive.org
Privacy notice: By enabling the option above, your browser will contact the API of web.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 and opencitations.net 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 Crossref privacy policy and the OpenCitations privacy policy.
Citation data
Add a list of citing articles from 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 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.
Tweets on dblp homepage
Show tweets from 
on the dblp homepage.
Privacy notice: By enabling the option above, your browser will contact twitter.com and twimg.com to load tweets curated by our Twitter accout. At the same time, Twitter will persitently store several cookies with your web browser. While we did signal Twitter to not track our users by setting the "dnt" flag, we do not have any control over how Twitter uses your data. So please proceed with care and consider checking the Twitter privacy policy.
last updated on 2020-05-20 00:13 CEST by the dblp team
all metadata released as open data under CC0 1.0 license
see also: Terms of Use | Privacy Policy | Imprint
the dblp computer science bibliography is funded by:
