Yves Bertot

Publication Activity (10 Years)

Years Active: 1990-2024
Publications (10 Years): 8

Top Topics

Fast Fourier Transform

Empirical Bayes

Top Venues

J. Formaliz. Reason.

Publications

Yves Bertot
Safe Smooth Paths Between Straight Line Obstacles. Logics and Type Systems in Theory and Practice (2024)
Andrew W. Appel, Yves Bertot
Corrigendum: C floating-point proofs layered with VST and Flocq. J. Formaliz. Reason. 13 (1) (2020)
Andrew W. Appel, Yves Bertot
C floating-point proofs layered with VST and Flocq. J. Formaliz. Reason. 13 (1) (2020)
Yves Bertot
Formal Verification of a Geometry Algorithm: A Quest for Abstract Views and Symmetry in Coq Proofs. ICTAC (2018)
Yves Bertot
Formal Verification of a Geometry Algorithm: A Quest for Abstract Views and Symmetry in Coq Proofs. CoRR (2018)
Yves Bertot, Laurence Rideau, Laurent Théry
Distant Decimals of π : Formal Proofs of Some Algorithms Computing Them and Guarantees of Exact Computation. J. Autom. Reason. 61 (1-4) (2018)
Yves Bertot, Laurence Rideau, Laurent Théry
Distant decimals of $π$. CoRR (2017)
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)
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 (2015)
Yves Bertot
Fixed Precision Patterns for the Formal Verification of Mathematical Constant Approximations. CPP (2015)
Yves Bertot, Guillaume Allais
Views of PI: Definition and computation. J. Formaliz. Reason. 7 (1) (2014)
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)
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 (2012)
Yves Bertot, Frédérique Guilhot, Assia Mahboubi
A formal study of Bernstein coefficients and polynomials. Math. Struct. Comput. Sci. 21 (4) (2011)
Tuan-Minh Pham, Yves Bertot, Julien Narboux
A Coq-Based Library for Interactive and Automated Theorem Proving in Plane Geometry. ICCSA (4) (2011)
Jean-François Dufourd, Yves Bertot
Formal Study of Plane Delaunay Triangulation. ITP (2010)
Jean-François Dufourd, Yves Bertot
Formal study of plane Delaunay triangulation CoRR (2010)
Maxime Dénès, Benjamin Lesage, Yves Bertot, Adrien Richard
Formal Proof of Theorems on Genetic Regulatory Networks. SYNASC (2009)
Yves Bertot, Ekaterina Komendantskaya
Using Structural Recursion for Corecursion CoRR (2009)
Yves Bertot, Ekaterina Komendantskaya
Inductive and Coinductive Components of Corecursive Functions in Coq CoRR (2008)
Yves Bertot
Structural abstract interpretation, A formal study using Coq CoRR (2008)
Yves Bertot, Ekaterina Komendantskaya
Inductive and Coinductive Components of Corecursive Functions in Coq. CMCS (2008)
Yves Bertot
A Short Presentation of Coq. TPHOLs (2008)
Yves Bertot
Structural Abstract Interpretation: A Formal Study Using Coq. LerNet ALFA Summer School (2008)
Yves Bertot, Georges Gonthier, Sidi Ould Biha, Ioana Pasca
Canonical Big Operators. TPHOLs (2008)
Yves Bertot, Vladimir Komendantsky
Fixed point semantics and partial recursion in Coq. PPDP (2008)
Yves Bertot, Ekaterina Komendantskaya
Using Structural Recursion for Corecursion. TYPES (2008)
Yves Bertot
Affine functions and series with co-inductive real numbers. Math. Struct. Comput. Sci. 17 (1) (2007)
Yves Bertot
Theorem proving support in programming language semantics CoRR (2007)
Yves Bertot
Extending the Calculus of Constructions with Tarski's fix-point theorem CoRR (2006)
Yves Bertot
Affine functions and series with co-inductive real numbers CoRR (2006)
Yves Bertot
CoInduction in Coq CoRR (2006)
Yves Bertot
Coq in a Hurry CoRR (2006)
Yves Bertot
Filters on CoInductive Streams, an Application to Eratosthenes' Sieve. TLCA (2005)
Yves Bertot, Laurent Théry
Dependent Types, Theorem Proving, and Applications for a Verifying Compiler. VSTTE (2005)
Yves Bertot
Vérification formelle d'extractions de racines entières. Tech. Sci. Informatiques 24 (9) (2005)
Yves Bertot, Frédérique Guilhot, Loic Pottier
Visualizing Geometrical Statements with GeoView. Electron. Notes Theor. Comput. Sci. 103 (2004)
Yves Bertot, Benjamin Grégoire, Xavier Leroy
A Structured Approach to Proving Compiler Optimizations Based on Dataflow Analysis. TYPES (2004)
Milad Niqui, Yves Bertot
QArith: Coq Formalisation of Lazy Rational Arithmetic. TYPES (2003)
Yves Bertot
Simple canonical representation of rational numbers. Electron. Notes Theor. Comput. Sci. 85 (7) (2003)
Yves Bertot, Nicolas Magaud, Paul Zimmermann
A Proof of GMP Square Root. J. Autom. Reason. 29 (3-4) (2002)
Yves Bertot, Venanzio Capretta, Kuntal Das Barman
Type-Theoretic Functional Semantics. TPHOLs (2002)
Yves Bertot
Formalizing a JVML Verifier for Initialization in a Theorem Prover. CAV (2001)
Nicolas Magaud, Yves Bertot
Changement de représentation des structures de données en Coq: le cas des entiers naturels. JFLA (2001)
David Pichardie, Yves Bertot
Formalizing Convex Hull Algorithms. TPHOLs (2001)
Nicolas Magaud, Yves Bertot
Changing Data Structures in Type Theory: A Study of Natural Numbers. TYPES (2000)
Antonia Balaa, Yves Bertot
Fix-Point Equations for Well-Founded Recursion in Type Theory. TPHOLs (2000)
Yves Bertot, Laurence Rideau, Loïc Pottier, Laurent Thiry
CtCoq: an environment for mathematical reasoning. SIGSAM Bull. 33 (3) (1999)
Yves Bertot
The CtCoq System: Design and Architecture. Formal Aspects Comput. 11 (3) (1999)
Yves Bertot, Laurent Théry
A Generic Approach to Building User Interfaces for Theorem Provers. J. Symb. Comput. 25 (2) (1998)
Yves Bertot
Head-Tactics Simplification. AMAST (1997)
Janet Bertot, Yves Bertot
CtCoq: A System Presentation. CADE (1996)
Janet Bertot, Yves Bertot
CtCoq: A System Presentation. AMAST (1996)
Yves Bertot, Ranan Fraer
Reasoning with Executable Specifications. TAPSOFT (1995)
Yves Bertot, Gilles Kahn, Laurent Théry
Proof by Pointing. TACS (1994)
Yves Bertot
Origin Functions in Lambda-Calculus and Term Rewriting Systems. CAAP (1992)
Laurent Théry, Yves Bertot, Gilles Kahn
Real theorem provers deserve real user-interfaces. SDE (1992)
Yves Bertot
Occurences in Debugger Specifications. PLDI (1991)
Yves Bertot
Implementation of an Interpreter for a Parallel Language in Centaur. ESOP (1990)