Yves Bertot
Refine list

refinements active!
zoomed in on ?? of ?? records
view refined list in
export refined list as
showing all ?? records
2010 – today
- 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) - [c31]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]
- 2016
- [c30]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]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) - 2013
- [c28]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]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]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]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]
- [i9]Jean-François Dufourd, Yves Bertot:
Formal study of plane Delaunay triangulation. CoRR abs/1007.3350 (2010)
2000 – 2009
- 2009
- [c25]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
- [j9]Yves Bertot, Ekaterina Komendantskaya:
Inductive and Coinductive Components of Corecursive Functions in Coq. Electr. Notes Theor. Comput. Sci. 203(5): 25-47 (2008) - [c24]Yves Bertot:
Structural Abstract Interpretation: A Formal Study Using Coq. LerNet ALFA Summer School 2008: 153-194 - [c23]Yves Bertot, Vladimir Komendantsky:
Fixed point semantics and partial recursion in Coq. PPDP 2008: 89-96 - [c22]
- [c21]Yves Bertot, Georges Gonthier, Sidi Ould Biha, Ioana Pasca:
Canonical Big Operators. TPHOLs 2008: 86-101 - [c20]Yves Bertot, Ekaterina Komendantskaya:
Using Structural Recursion for Corecursion. TYPES 2008: 220-236 - [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. Mathematical Structures in Computer Science 17(1): 37-63 (2007) - [i5]
- 2006
- [i4]
- [i3]
- [i2]
- [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. Electr. 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. Electr. 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]
- [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]
- 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. ACM SIGSAM Bulletin 33(3): 21-22 (1999) - [j2]
- [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]
- 1996
- [c8]
- [c7]
- 1995
- [c6]
- 1994
- [c5]
- 1992
- [c4]
- [c3]Laurent Théry, Yves Bertot, Gilles Kahn:
Real theorem provers deserve real user-interfaces. SDE 1992: 120-129 - 1991
- [c2]
- 1990
- [c1]
Coauthor Index
last updated on 2019-01-09 01:11 CET by the dblp team
data released under the ODC-BY 1.0 license
see also: Terms of Use | Privacy Policy | Imprint