Yves Bertot

According to our database, Yves Bertot authored at least 53 papers between 1990 and 2024.

Collaborative distances:

• Dijkstra number of four.
• Erdős number of three.

2024

Safe Smooth Paths Between Straight Line Obstacles.

Yves Bertot

Proceedings of the Logics and Type Systems in Theory and Practice, 2024

2020

Corrigendum: C floating-point proofs layered with VST and Flocq.

Andrew W. Appel, Yves Bertot

J. Formaliz. Reason., 2020

C floating-point proofs layered with VST and Flocq.

Andrew W. Appel, Yves Bertot

J. Formaliz. Reason., 2020

2018

Distant Decimals of π : Formal Proofs of Some Algorithms Computing Them and Guarantees of Exact Computation.

Yves Bertot, Laurence Rideau, Laurent Théry

J. Autom. Reason., 2018

Formal Verification of a Geometry Algorithm: A Quest for Abstract Views and Symmetry in Coq Proofs.

Yves Bertot

Proceedings of the Theoretical Aspects of Computing - ICTAC 2018, 2018

2017

Distant decimals of $π$.

Yves Bertot, Laurence Rideau, Laurent Théry

CoRR, 2017

2016

Formal proofs of transcendence for e and pi as an application of multivariate and symmetric polynomials.

Sophie Bernard, Yves Bertot, Laurence Rideau, Pierre-Yves Strub

Proceedings of the 5th ACM SIGPLAN Conference on Certified Programs and Proofs, 2016

2015

Formal Proofs of Transcendence for e and $π$ as an Application of Multivariate and Symmetric Polynomials.

Sophie Bernard, Yves Bertot, Laurence Rideau, Pierre-Yves Strub

CoRR, 2015

Fixed Precision Patterns for the Formal Verification of Mathematical Constant Approximations.

Yves Bertot

Proceedings of the 2015 Conference on Certified Programs and Proofs, 2015

2014

Views of PI: Definition and computation.

Yves Bertot, Guillaume Allais

J. Formaliz. Reason., 2014

2013

A Machine-Checked Proof of the Odd Order Theorem.

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

Proceedings of the Interactive Theorem Proving - 4th International Conference, 2013

2011

A formal study of Bernstein coefficients and polynomials.

Yves Bertot, Frédérique Guilhot, Assia Mahboubi

Math. Struct. Comput. Sci., 2011

A Coq-Based Library for Interactive and Automated Theorem Proving in Plane Geometry.

Tuan-Minh Pham, Yves Bertot, Julien Narboux

Proceedings of the Computational Science and Its Applications - ICCSA 2011, 2011

2010

A Combination of a Dynamic Geometry Software With a Proof Assistant for Interactive Formal Proofs.

Tuan-Minh Pham, Yves Bertot

Proceedings of the 9th International Workshop On User Interfaces for Theorem Provers, 2010

Formal Study of Plane Delaunay Triangulation.

Jean-François Dufourd, Yves Bertot

Proceedings of the Interactive Theorem Proving, First International Conference, 2010

2009

Formal Proof of Theorems on Genetic Regulatory Networks.

Maxime Dénès, Benjamin Lesage, Yves Bertot, Adrien Richard

Proceedings of the 11th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, 2009

2008

Inductive and Coinductive Components of Corecursive Functions in Coq.

Yves Bertot, Ekaterina Komendantskaya

Proceedings of the Ninth Workshop on Coalgebraic Methods in Computer Science, 2008

Using Structural Recursion for Corecursion.

Yves Bertot, Ekaterina Komendantskaya

Proceedings of the Types for Proofs and Programs, International Conference, 2008

Canonical Big Operators.

Yves Bertot, Georges Gonthier, Sidi Ould Biha, Ioana Pasca

Proceedings of the Theorem Proving in Higher Order Logics, 21st International Conference, 2008

A Short Presentation of Coq.

Yves Bertot

Proceedings of the Theorem Proving in Higher Order Logics, 21st International Conference, 2008

Fixed point semantics and partial recursion in Coq.

Yves Bertot, Vladimir Komendantsky

Proceedings of the 10th International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming, 2008

Structural Abstract Interpretation: A Formal Study Using Coq.

Yves Bertot

Proceedings of the Language Engineering and Rigorous Software Development, International LerNet ALFA Summer School 2008, Piriapolis, Uruguay, February 24, 2008

2007

Affine functions and series with co-inductive real numbers.

Yves Bertot

Math. Struct. Comput. Sci., 2007

Theorem proving support in programming language semantics

Yves Bertot

CoRR, 2007

2006

Extending the Calculus of Constructions with Tarski's fix-point theorem

Yves Bertot

CoRR, 2006

CoInduction in Coq

Yves Bertot

CoRR, 2006

Coq in a Hurry

Yves Bertot

CoRR, 2006

2005

Vérification formelle d'extractions de racines entières.

Yves Bertot

Tech. Sci. Informatiques, 2005

Dependent Types, Theorem Proving, and Applications for a Verifying Compiler.

Yves Bertot, Laurent Théry

Proceedings of the Verified Software: Theories, 2005

Filters on CoInductive Streams, an Application to Eratosthenes' Sieve.

Yves Bertot

Proceedings of the Typed Lambda Calculi and Applications, 7th International Conference, 2005

2004

Interactive Theorem Proving and Program Development - Coq'Art: The Calculus of Inductive Constructions

Yves Bertot, Pierre Castéran

Texts in Theoretical Computer Science. An EATCS Series, Springer, ISBN: 978-3-662-07964-5, 2004

A Structured Approach to Proving Compiler Optimizations Based on Dataflow Analysis.

Yves Bertot, Benjamin Grégoire, Xavier Leroy

Proceedings of the Types for Proofs and Programs, International Workshop, 2004

2003

Visualizing Geometrical Statements with GeoView.

Yves Bertot, Frédérique Guilhot, Loic Pottier

Proceedings of the User Interfaces for Theorem Provers Workshop, 2003

Simple canonical representation of rational numbers.

Yves Bertot

Proceedings of the Mathematics, 2003

QArith: Coq Formalisation of Lazy Rational Arithmetic.

Milad Niqui, Yves Bertot

Proceedings of the Types for Proofs and Programs, International Workshop, 2003

2002

A Proof of GMP Square Root.

Yves Bertot, Nicolas Magaud, Paul Zimmermann

J. Autom. Reason., 2002

Type-Theoretic Functional Semantics.

Yves Bertot, Venanzio Capretta, Kuntal Das Barman

Proceedings of the Theorem Proving in Higher Order Logics, 15th International Conference, 2002

2001

Formalizing Convex Hull Algorithms.

David Pichardie, Yves Bertot

Proceedings of the Theorem Proving in Higher Order Logics, 14th International Conference, 2001

Changement de représentation des structures de données en Coq: le cas des entiers naturels.

Nicolas Magaud, Yves Bertot

Proceedings of the Journées francophones des langages applicatifs (JFLA'01), 2001

Formalizing a JVML Verifier for Initialization in a Theorem Prover.

Yves Bertot

Proceedings of the Computer Aided Verification, 13th International Conference, 2001

2000

Changing Data Structures in Type Theory: A Study of Natural Numbers.

Nicolas Magaud, Yves Bertot

Proceedings of the Types for Proofs and Programs, International Workshop, 2000

Fix-Point Equations for Well-Founded Recursion in Type Theory.

Antonia Balaa, Yves Bertot

Proceedings of the Theorem Proving in Higher Order Logics, 13th International Conference, 2000

1999

The CtCoq System: Design and Architecture.

Yves Bertot

Formal Aspects Comput., 1999

CtCoq: an environment for mathematical reasoning.

Yves Bertot, Laurence Rideau, Loïc Pottier, Laurent Thiry

SIGSAM Bull., 1999

1998

A Generic Approach to Building User Interfaces for Theorem Provers.

Yves Bertot, Laurent Théry

J. Symb. Comput., 1998

1997

Head-Tactics Simplification.

Yves Bertot

Proceedings of the Algebraic Methodology and Software Technology, 1997

1996

CtCoq: A System Presentation.

Janet Bertot, Yves Bertot

Proceedings of the Algebraic Methodology and Software Technology, 1996

1995

Reasoning with Executable Specifications.

Yves Bertot, Ranan Fraer

Proceedings of the TAPSOFT'95: Theory and Practice of Software Development, 1995

1994

Proof by Pointing.

Yves Bertot, Gilles Kahn, Laurent Théry

Proceedings of the Theoretical Aspects of Computer Software, 1994

1992

Real theorem provers deserve real user-interfaces.

Laurent Théry, Yves Bertot, Gilles Kahn

Proceedings of the 5th ACM SIGSOFT Symposium on Software Development Environments, 1992

Origin Functions in Lambda-Calculus and Term Rewriting Systems.

Yves Bertot

Proceedings of the CAAP '92, 1992

1991

Occurences in Debugger Specifications.

Yves Bertot

Proceedings of the ACM SIGPLAN'91 Conference on Programming Language Design and Implementation (PLDI), 1991

1990

Implementation of an Interpreter for a Parallel Language in Centaur.

Yves Bertot

Proceedings of the ESOP'90, 1990