ask others

Yves Bertot

> Home > Persons

Refine list

refinements active!

zoomed in on ?? of ?? records

view refined list in

showing all ?? records

2010 – today

see FAQ

What is the meaning of the colors in the publication lists?

2018
[j12]
- view
  - electronic edition via DOI
- export record
  dblp key:
  - journals/jar/BertotRT18
- ask others
- share record
  short URL:
  - https://dblp.org/rec/journals/jar/BertotRT18
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)
[c31]
- view
  - electronic edition via DOI
- export record
  dblp key:
  - conf/ictac/Bertot18
- ask others
- share record
  short URL:
  - https://dblp.org/rec/conf/ictac/Bertot18
Yves Bertot:
Formal Verification of a Geometry Algorithm: A Quest for Abstract Views and Symmetry in Coq Proofs. ICTAC 2018: 3-10
[i12]
- view
  - electronic edition @ arxiv.org
- export record
  dblp key:
  - journals/corr/abs-1809-00559
- ask others
- share record
  short URL:
  - https://dblp.org/rec/journals/corr/abs-1809-00559
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]
- view
  - table of contents in dblp
  - electronic edition via DOI
- export record
  dblp key:
  - conf/cpp/2017
- ask others
- share record
  short URL:
  - https://dblp.org/rec/conf/cpp/2017
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]
- view
  - electronic edition @ arxiv.org
- export record
  dblp key:
  - journals/corr/abs-1709-01743
- ask others
- share record
  short URL:
  - https://dblp.org/rec/journals/corr/abs-1709-01743
Yves Bertot, Laurence Rideau, Laurent Théry:
Distant decimals of $π$. CoRR abs/1709.01743 (2017)
2016
[c30]
- view
  - electronic edition via DOI
- export record
  dblp key:
  - conf/cpp/BernardBRS16
- ask others
- share record
  short URL:
  - https://dblp.org/rec/conf/cpp/BernardBRS16
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
[c29]
- view
  - electronic edition via DOI
- export record
  dblp key:
  - conf/cpp/Bertot15
- ask others
- share record
  short URL:
  - https://dblp.org/rec/conf/cpp/Bertot15
Yves Bertot:
Fixed Precision Patterns for the Formal Verification of Mathematical Constant Approximations. CPP 2015: 147-155
[i10]
- view
  - electronic edition @ arxiv.org
- export record
  dblp key:
  - journals/corr/BernardBRS15
- ask others
- share record
  short URL:
  - https://dblp.org/rec/journals/corr/BernardBRS15
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)
2013
[c28]
- view
  - electronic edition via DOI
  - electronic edition @ wikidata.org
- export record
  dblp key:
  - conf/itp/GonthierAABCGRMOBPRSTT13
- ask others
- share record
  short URL:
  - https://dblp.org/rec/conf/itp/GonthierAABCGRMOBPRSTT13
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
[j11]
- view
  - electronic edition via DOI
- export record
  dblp key:
  - journals/entcs/PhamB12
- ask others
- share record
  short URL:
  - https://dblp.org/rec/journals/entcs/PhamB12
Tuan-Minh Pham, Yves Bertot:
A Combination of a Dynamic Geometry Software With a Proof Assistant for Interactive Formal Proofs. Electr. Notes Theor. Comput. Sci. 285: 43-55 (2012)
2011
[j10]
- view
  - electronic edition via DOI
- export record
  dblp key:
  - journals/mscs/BertotGM11
- ask others
- share record
  short URL:
  - https://dblp.org/rec/journals/mscs/BertotGM11
Yves Bertot, Frédérique Guilhot, Assia Mahboubi:
A formal study of Bernstein coefficients and polynomials. Mathematical Structures in Computer Science 21(4): 731-761 (2011)
[c27]
- view
  - electronic edition via DOI
- export record
  dblp key:
  - conf/iccsa/PhamBN11
- ask others
- share record
  short URL:
  - https://dblp.org/rec/conf/iccsa/PhamBN11
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
[c26]
- view
  - electronic edition via DOI
- export record
  dblp key:
  - conf/itp/DufourdB10
- ask others
- share record
  short URL:
  - https://dblp.org/rec/conf/itp/DufourdB10
Jean-François Dufourd, Yves Bertot:
Formal Study of Plane Delaunay Triangulation. ITP 2010: 211-226
[i9]
- view
  - electronic edition @ arxiv.org
- export record
  dblp key:
  - journals/corr/abs-1007-3350
- ask others
- share record
  short URL:
  - https://dblp.org/rec/journals/corr/abs-1007-3350
Jean-François Dufourd, Yves Bertot:
Formal study of plane Delaunay triangulation. CoRR abs/1007.3350 (2010)

2000 – 2009

see FAQ

What is the meaning of the colors in the publication lists?

2009
[c25]
- view
  - electronic edition via DOI
  - electronic edition @ ieeecomputersociety.org
- export record
  dblp key:
  - conf/synasc/DenesLBR09
- ask others
- share record
  short URL:
  - https://dblp.org/rec/conf/synasc/DenesLBR09
Maxime Dénès, Benjamin Lesage, Yves Bertot, Adrien Richard:
Formal Proof of Theorems on Genetic Regulatory Networks. SYNASC 2009: 69-76
[i8]
- view
  - electronic edition @ arxiv.org
- export record
  dblp key:
  - journals/corr/abs-0903-3850
- ask others
- share record
  short URL:
  - https://dblp.org/rec/journals/corr/abs-0903-3850
Yves Bertot, Ekaterina Komendantskaya:
Using Structural Recursion for Corecursion. CoRR abs/0903.3850 (2009)
2008
[j9]
- view
  - electronic edition via DOI
- export record
  dblp key:
  - journals/entcs/BertotK08
- ask others
- share record
  short URL:
  - https://dblp.org/rec/journals/entcs/BertotK08
Yves Bertot, Ekaterina Komendantskaya:
Inductive and Coinductive Components of Corecursive Functions in Coq. Electr. Notes Theor. Comput. Sci. 203(5): 25-47 (2008)
[c24]
- view
  - electronic edition via DOI
- export record
  dblp key:
  - conf/lernet/Bertot08
- ask others
- share record
  short URL:
  - https://dblp.org/rec/conf/lernet/Bertot08
Yves Bertot:
Structural Abstract Interpretation: A Formal Study Using Coq. LerNet ALFA Summer School 2008: 153-194
[c23]
- view
  - electronic edition via DOI
- export record
  dblp key:
  - conf/ppdp/BertotK08
- ask others
- share record
  short URL:
  - https://dblp.org/rec/conf/ppdp/BertotK08
Yves Bertot, Vladimir Komendantsky:
Fixed point semantics and partial recursion in Coq. PPDP 2008: 89-96
[c22]
- view
  - electronic edition via DOI
- export record
  dblp key:
  - conf/tphol/Bertot08
- ask others
- share record
  short URL:
  - https://dblp.org/rec/conf/tphol/Bertot08
Yves Bertot:
A Short Presentation of Coq. TPHOLs 2008: 12-16
[c21]
- view
  - electronic edition via DOI
- export record
  dblp key:
  - conf/tphol/BertotGBP08
- ask others
- share record
  short URL:
  - https://dblp.org/rec/conf/tphol/BertotGBP08
Yves Bertot, Georges Gonthier, Sidi Ould Biha, Ioana Pasca:
Canonical Big Operators. TPHOLs 2008: 86-101
[c20]
- view
  - electronic edition via DOI
- export record
  dblp key:
  - conf/types/BertotK08
- ask others
- share record
  short URL:
  - https://dblp.org/rec/conf/types/BertotK08
Yves Bertot, Ekaterina Komendantskaya:
Using Structural Recursion for Corecursion. TYPES 2008: 220-236
[i7]
- view
  - electronic edition @ arxiv.org
- export record
  dblp key:
  - journals/corr/abs-0807-1524
- ask others
- share record
  short URL:
  - https://dblp.org/rec/journals/corr/abs-0807-1524
Yves Bertot, Ekaterina Komendantskaya:
Inductive and Coinductive Components of Corecursive Functions in Coq. CoRR abs/0807.1524 (2008)
[i6]
- view
  - electronic edition @ arxiv.org
- export record
  dblp key:
  - journals/corr/abs-0810-2179
- ask others
- share record
  short URL:
  - https://dblp.org/rec/journals/corr/abs-0810-2179
Yves Bertot:
Structural abstract interpretation, A formal study using Coq. CoRR abs/0810.2179 (2008)
2007
[j8]
- view
  - electronic edition via DOI
- export record
  dblp key:
  - journals/mscs/Bertot07
- ask others
- share record
  short URL:
  - https://dblp.org/rec/journals/mscs/Bertot07
Yves Bertot:
Affine functions and series with co-inductive real numbers. Mathematical Structures in Computer Science 17(1): 37-63 (2007)
[i5]
- view
  - electronic edition @ arxiv.org
- export record
  dblp key:
  - journals/corr/abs-0707-0926
- ask others
- share record
  short URL:
  - https://dblp.org/rec/journals/corr/abs-0707-0926
Yves Bertot:
Theorem proving support in programming language semantics. CoRR abs/0707.0926 (2007)
2006
[i4]
- view
  - electronic edition @ arxiv.org
- export record
  dblp key:
  - journals/corr/abs-cs-0603117
- ask others
- share record
  short URL:
  - https://dblp.org/rec/journals/corr/abs-cs-0603117
Yves Bertot:
Affine functions and series with co-inductive real numbers. CoRR abs/cs/0603117 (2006)
[i3]
- view
  - electronic edition @ arxiv.org
- export record
  dblp key:
  - journals/corr/abs-cs-0603118
- ask others
- share record
  short URL:
  - https://dblp.org/rec/journals/corr/abs-cs-0603118
Yves Bertot:
Coq in a Hurry. CoRR abs/cs/0603118 (2006)
[i2]
- view
  - electronic edition @ arxiv.org
- export record
  dblp key:
  - journals/corr/abs-cs-0603119
- ask others
- share record
  short URL:
  - https://dblp.org/rec/journals/corr/abs-cs-0603119
Yves Bertot:
CoInduction in Coq. CoRR abs/cs/0603119 (2006)
[i1]
- view
  - electronic edition @ arxiv.org
- export record
  dblp key:
  - journals/corr/abs-cs-0610055
- ask others
- share record
  short URL:
  - https://dblp.org/rec/journals/corr/abs-cs-0610055
Yves Bertot:
Extending the Calculus of Constructions with Tarski's fix-point theorem. CoRR abs/cs/0610055 (2006)
2005
[j7]
- view
  - electronic edition via DOI
- export record
  dblp key:
  - journals/tsi/Bertot05
- ask others
- share record
  short URL:
  - https://dblp.org/rec/journals/tsi/Bertot05
Yves Bertot:
Vérification formelle d'extractions de racines entières. Technique et Science Informatiques 24(9): 1161-1185 (2005)
[c19]
- view
  - electronic edition via DOI
- export record
  dblp key:
  - conf/tlca/Bertot05
- ask others
- share record
  short URL:
  - https://dblp.org/rec/conf/tlca/Bertot05
Yves Bertot:
Filters on CoInductive Streams, an Application to Eratosthenes' Sieve. TLCA 2005: 102-115
[c18]
- view
  - electronic edition via DOI
- export record
  dblp key:
  - conf/vstte/BertotT05
- ask others
- share record
  short URL:
  - https://dblp.org/rec/conf/vstte/BertotT05
Yves Bertot, Laurent Théry:
Dependent Types, Theorem Proving, and Applications for a Verifying Compiler. VSTTE 2005: 173-181
2004
[b1]
- view
  - electronic edition via DOI
- export record
  dblp key:
  - series/txtcs/BertotC04
- ask others
- share record
  short URL:
  - https://dblp.org/rec/series/txtcs/BertotC04
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]
- view
  - electronic edition via DOI
- export record
  dblp key:
  - journals/entcs/BertotGP04
- ask others
- share record
  short URL:
  - https://dblp.org/rec/journals/entcs/BertotGP04
Yves Bertot, Frédérique Guilhot, Loic Pottier:
Visualizing Geometrical Statements with GeoView. Electr. Notes Theor. Comput. Sci. 103: 49-65 (2004)
[c17]
- view
  - electronic edition via DOI
- export record
  dblp key:
  - conf/types/BertotGL04
- ask others
- share record
  short URL:
  - https://dblp.org/rec/conf/types/BertotGL04
Yves Bertot, Benjamin Grégoire, Xavier Leroy:
A Structured Approach to Proving Compiler Optimizations Based on Dataflow Analysis. TYPES 2004: 66-81
2003
[j5]
- view
  - electronic edition via DOI
- export record
  dblp key:
  - journals/entcs/Bertot03
- ask others
- share record
  short URL:
  - https://dblp.org/rec/journals/entcs/Bertot03
Yves Bertot:
Simple canonical representation of rational numbers. Electr. Notes Theor. Comput. Sci. 85(7): 1-16 (2003)
[c16]
- view
  - electronic edition via DOI
- export record
  dblp key:
  - conf/types/NiquiB03
- ask others
- share record
  short URL:
  - https://dblp.org/rec/conf/types/NiquiB03
Milad Niqui, Yves Bertot:
QArith: Coq Formalisation of Lazy Rational Arithmetic. TYPES 2003: 309-323
2002
[j4]
- view
  - electronic edition via DOI
- export record
  dblp key:
  - journals/jar/BertotMZ02
- ask others
- share record
  short URL:
  - https://dblp.org/rec/journals/jar/BertotMZ02
Yves Bertot, Nicolas Magaud, Paul Zimmermann:
A Proof of GMP Square Root. J. Autom. Reasoning 29(3-4): 225-252 (2002)
[c15]
- view
  - electronic edition via DOI
- export record
  dblp key:
  - conf/tphol/BertotCB02
- ask others
- share record
  short URL:
  - https://dblp.org/rec/conf/tphol/BertotCB02
Yves Bertot, Venanzio Capretta, Kuntal Das Barman:
Type-Theoretic Functional Semantics. TPHOLs 2002: 83-98
2001
[c14]
- view
  - electronic edition via DOI
- export record
  dblp key:
  - conf/cav/Bertot01
- ask others
- share record
  short URL:
  - https://dblp.org/rec/conf/cav/Bertot01
Yves Bertot:
Formalizing a JVML Verifier for Initialization in a Theorem Prover. CAV 2001: 14-24
[c13]
- no documents available
- export record
  dblp key:
  - conf/jfla/MagaudB01
- ask others
- share record
  short URL:
  - https://dblp.org/rec/conf/jfla/MagaudB01
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]
- view
  - electronic edition via DOI
- export record
  dblp key:
  - conf/tphol/PichardieB01
- ask others
- share record
  short URL:
  - https://dblp.org/rec/conf/tphol/PichardieB01
David Pichardie, Yves Bertot:
Formalizing Convex Hull Algorithms. TPHOLs 2001: 346-361
2000
[c11]
- view
  - electronic edition via DOI
- export record
  dblp key:
  - conf/tphol/BalaaB00
- ask others
- share record
  short URL:
  - https://dblp.org/rec/conf/tphol/BalaaB00
Antonia Balaa, Yves Bertot:
Fix-Point Equations for Well-Founded Recursion in Type Theory. TPHOLs 2000: 1-16
[c10]
- view
  - electronic edition via DOI
  - electronic edition @ wikidata.org
- export record
  dblp key:
  - conf/types/MagaudB00
- ask others
- share record
  short URL:
  - https://dblp.org/rec/conf/types/MagaudB00
Nicolas Magaud, Yves Bertot:
Changing Data Structures in Type Theory: A Study of Natural Numbers. TYPES 2000: 181-196

1990 – 1999

see FAQ

What is the meaning of the colors in the publication lists?

1999
[j3]
- view
  - electronic edition via DOI
- export record
  dblp key:
  - journals/cca/Group99
- ask others
- share record
  short URL:
  - https://dblp.org/rec/journals/cca/Group99
Yves Bertot, Laurence Rideau, Loïc Pottier, Laurent Thiry:
CtCoq: an environment for mathematical reasoning. ACM SIGSAM Bulletin 33(3): 21-22 (1999)
[j2]
- view
  - electronic edition via DOI
- export record
  dblp key:
  - journals/fac/Bertot99
- ask others
- share record
  short URL:
  - https://dblp.org/rec/journals/fac/Bertot99
Yves Bertot:
The CtCoq System: Design and Architecture. Formal Asp. Comput. 11(3): 225-243 (1999)
[e1]
- view
  - table of contents in dblp
  - electronic edition via DOI
- export record
  dblp key:
  - conf/tphol/1999
- ask others
- share record
  short URL:
  - https://dblp.org/rec/conf/tphol/1999
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]
- view
  - electronic edition via DOI
- export record
  dblp key:
  - journals/jsc/BertotT98
- ask others
- share record
  short URL:
  - https://dblp.org/rec/journals/jsc/BertotT98
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]
- view
  - electronic edition via DOI
- export record
  dblp key:
  - conf/amast/Bertot97
- ask others
- share record
  short URL:
  - https://dblp.org/rec/conf/amast/Bertot97
Yves Bertot:
Head-Tactics Simplification. AMAST 1997: 16-29
1996
[c8]
- view
  - electronic edition via DOI
- export record
  dblp key:
  - conf/amast/BertotB96
- ask others
- share record
  short URL:
  - https://dblp.org/rec/conf/amast/BertotB96
Janet Bertot, Yves Bertot:
CtCoq: A System Presentation. AMAST 1996: 600-603
[c7]
- view
  - electronic edition via DOI
- export record
  dblp key:
  - conf/cade/BertotB96
- ask others
- share record
  short URL:
  - https://dblp.org/rec/conf/cade/BertotB96
Janet Bertot, Yves Bertot:
CtCoq: A System Presentation. CADE 1996: 231-234
1995
[c6]
- view
  - electronic edition via DOI
- export record
  dblp key:
  - conf/tapsoft/BertotF95
- ask others
- share record
  short URL:
  - https://dblp.org/rec/conf/tapsoft/BertotF95
Yves Bertot, Ranan Fraer:
Reasoning with Executable Specifications. TAPSOFT 1995: 531-545
1994
[c5]
- view
  - electronic edition via DOI
- export record
  dblp key:
  - conf/tacs/BertotKT94
- ask others
- share record
  short URL:
  - https://dblp.org/rec/conf/tacs/BertotKT94
Yves Bertot, Gilles Kahn, Laurent Théry:
Proof by Pointing. TACS 1994: 141-160
1992
[c4]
- view
  - electronic edition via DOI
- export record
  dblp key:
  - conf/caap/Bertot92
- ask others
- share record
  short URL:
  - https://dblp.org/rec/conf/caap/Bertot92
Yves Bertot:
Origin Functions in Lambda-Calculus and Term Rewriting Systems. CAAP 1992: 49-65
[c3]
- view
  - electronic edition via DOI
- export record
  dblp key:
  - conf/sde/TheryBK92
- ask others
- share record
  short URL:
  - https://dblp.org/rec/conf/sde/TheryBK92
Laurent Théry, Yves Bertot, Gilles Kahn:
Real theorem provers deserve real user-interfaces. SDE 1992: 120-129
1991
[c2]
- view
  - electronic edition via DOI
- export record
  dblp key:
  - conf/pldi/Bertot91
- ask others
- share record
  short URL:
  - https://dblp.org/rec/conf/pldi/Bertot91
Yves Bertot:
Occurences in Debugger Specifications. PLDI 1991: 327-337
1990
[c1]
- view
  - electronic edition via DOI
- export record
  dblp key:
  - conf/esop/Bertot90
- ask others
- share record
  short URL:
  - https://dblp.org/rec/conf/esop/Bertot90
Yves Bertot:
Implementation of an Interpreter for a Parallel Language in Centaur. ESOP 1990: 57-69

Coauthor Index

see FAQ

maintained by

at