Yves Bertot

Orcid: 0000-0001-5052-3019

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

Collaborative distances:

Timeline

Legend:

Book 
In proceedings 
Article 
PhD thesis 
Dataset
Other 

Links

On csauthors.net:

Bibliography

2024
Safe Smooth Paths Between Straight Line Obstacles.
Proceedings of the Logics and Type Systems in Theory and Practice, 2024

2020
Corrigendum: C floating-point proofs layered with VST and Flocq.
J. Formaliz. Reason., 2020

C floating-point proofs layered with VST and Flocq.
J. Formaliz. Reason., 2020

2018
Distant Decimals of π : Formal Proofs of Some Algorithms Computing Them and Guarantees of Exact Computation.
J. Autom. Reason., 2018

Formal Verification of a Geometry Algorithm: A Quest for Abstract Views and Symmetry in Coq Proofs.
Proceedings of the Theoretical Aspects of Computing - ICTAC 2018, 2018

2017
Distant decimals of $π$.
CoRR, 2017

2016
Formal proofs of transcendence for e and pi as an application of multivariate and symmetric polynomials.
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.
CoRR, 2015

Fixed Precision Patterns for the Formal Verification of Mathematical Constant Approximations.
Proceedings of the 2015 Conference on Certified Programs and Proofs, 2015

2014
Views of PI: Definition and computation.
J. Formaliz. Reason., 2014

2013
A Machine-Checked Proof of the Odd Order Theorem.
Proceedings of the Interactive Theorem Proving - 4th International Conference, 2013

2011
A formal study of Bernstein coefficients and polynomials.
Math. Struct. Comput. Sci., 2011

A Coq-Based Library for Interactive and Automated Theorem Proving in Plane Geometry.
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.
Proceedings of the 9th International Workshop On User Interfaces for Theorem Provers, 2010

Formal Study of Plane Delaunay Triangulation.
Proceedings of the Interactive Theorem Proving, First International Conference, 2010

2009
Formal Proof of Theorems on Genetic Regulatory Networks.
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.
Proceedings of the Ninth Workshop on Coalgebraic Methods in Computer Science, 2008

Using Structural Recursion for Corecursion.
Proceedings of the Types for Proofs and Programs, International Conference, 2008

Canonical Big Operators.
Proceedings of the Theorem Proving in Higher Order Logics, 21st International Conference, 2008

A Short Presentation of Coq.
Proceedings of the Theorem Proving in Higher Order Logics, 21st International Conference, 2008

Fixed point semantics and partial recursion in Coq.
Proceedings of the 10th International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming, 2008

Structural Abstract Interpretation: A Formal Study Using Coq.
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.
Math. Struct. Comput. Sci., 2007

Theorem proving support in programming language semantics
CoRR, 2007

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

CoInduction in Coq
CoRR, 2006

Coq in a Hurry
CoRR, 2006

2005
Vérification formelle d'extractions de racines entières.
Tech. Sci. Informatiques, 2005

Dependent Types, Theorem Proving, and Applications for a Verifying Compiler.
Proceedings of the Verified Software: Theories, 2005

Filters on CoInductive Streams, an Application to Eratosthenes' Sieve.
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
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.
Proceedings of the Types for Proofs and Programs, International Workshop, 2004

2003
Visualizing Geometrical Statements with GeoView.
Proceedings of the User Interfaces for Theorem Provers Workshop, 2003

Simple canonical representation of rational numbers.
Proceedings of the Mathematics, 2003

QArith: Coq Formalisation of Lazy Rational Arithmetic.
Proceedings of the Types for Proofs and Programs, International Workshop, 2003

2002
A Proof of GMP Square Root.
J. Autom. Reason., 2002

Type-Theoretic Functional Semantics.
Proceedings of the Theorem Proving in Higher Order Logics, 15th International Conference, 2002

2001
Formalizing Convex Hull Algorithms.
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.
Proceedings of the Journées francophones des langages applicatifs (JFLA'01), 2001

Formalizing a JVML Verifier for Initialization in a Theorem Prover.
Proceedings of the Computer Aided Verification, 13th International Conference, 2001

2000
Changing Data Structures in Type Theory: A Study of Natural Numbers.
Proceedings of the Types for Proofs and Programs, International Workshop, 2000

Fix-Point Equations for Well-Founded Recursion in Type Theory.
Proceedings of the Theorem Proving in Higher Order Logics, 13th International Conference, 2000

1999
The CtCoq System: Design and Architecture.
Formal Aspects Comput., 1999

CtCoq: an environment for mathematical reasoning.
SIGSAM Bull., 1999

1998
A Generic Approach to Building User Interfaces for Theorem Provers.
J. Symb. Comput., 1998

1997
Head-Tactics Simplification.
Proceedings of the Algebraic Methodology and Software Technology, 1997

1996
CtCoq: A System Presentation.
Proceedings of the Algebraic Methodology and Software Technology, 1996

1995
Reasoning with Executable Specifications.
Proceedings of the TAPSOFT'95: Theory and Practice of Software Development, 1995

1994
Proof by Pointing.
Proceedings of the Theoretical Aspects of Computer Software, 1994

1992
Real theorem provers deserve real user-interfaces.
Proceedings of the 5th ACM SIGSOFT Symposium on Software Development Environments, 1992

Origin Functions in Lambda-Calculus and Term Rewriting Systems.
Proceedings of the CAAP '92, 1992

1991
Occurences in Debugger Specifications.
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.
Proceedings of the ESOP'90, 1990


  Loading...