Implementation of an Interpreter for a Parallel Language in Centaur. - Yves Bertot (ESOP, 1990)

Occurences in Debugger Specifications. - Yves Bertot (PLDI, 1991)

Origin Functions in Lambda-Calculus and Term Rewriting Systems. - Yves Bertot (CAAP, 1992)

Real theorem provers deserve real user-interfaces. - Laurent Théry; Yves Bertot; Gilles Kahn (SDE, 1992)

Proof by Pointing. - Yves Bertot; Gilles Kahn; Laurent Théry (TACS, 1994)

Reasoning with Executable Specifications. - Yves Bertot; Ranan Fraer (TAPSOFT, 1995)

CtCoq: A System Presentation. - Janet Bertot; Yves Bertot (AMAST, 1996)

Head-Tactics Simplification. - Yves Bertot (AMAST, 1997)

A Generic Approach to Building User Interfaces for Theorem Provers. - Yves Bertot; Laurent Théry (J. Symb. Comput., 1998)

CtCoq: an environment for mathematical reasoning. - Yves Bertot; Laurence Rideau; Loïc Pottier; Laurent Thiry (SIGSAM Bull., 1999)

The CtCoq System: Design and Architecture. - Yves Bertot (Formal Aspects Comput., 1999)

Fix-Point Equations for Well-Founded Recursion in Type Theory. - Antonia Balaa; Yves Bertot (TPHOLs, 2000)

Changing Data Structures in Type Theory: A Study of Natural Numbers. - Nicolas Magaud; Yves Bertot (TYPES, 2000)

Formalizing a JVML Verifier for Initialization in a Theorem Prover. - Yves Bertot (CAV, 2001)

Changement de représentation des structures de données en Coq: le cas des entiers naturels. - Nicolas Magaud; Yves Bertot (JFLA, 2001)

Formalizing Convex Hull Algorithms. - David Pichardie; Yves Bertot (TPHOLs, 2001)

Type-Theoretic Functional Semantics. - Yves Bertot; Venanzio Capretta; Kuntal Das Barman (TPHOLs, 2002)

A Proof of GMP Square Root. - Yves Bertot; Nicolas Magaud; Paul Zimmermann (J. Autom. Reason., 2002)

QArith: Coq Formalisation of Lazy Rational Arithmetic. - Milad Niqui; Yves Bertot (TYPES, 2003)

Simple canonical representation of rational numbers. - Yves Bertot (Mathematics, Logic and Computation @ ICALP, 2003)

Visualizing Geometrical Statements with GeoView. - Yves Bertot; Frédérique Guilhot; Loic Pottier (UITP@TPHOLs, 2003)

A Structured Approach to Proving Compiler Optimizations Based on Dataflow Analysis. - Yves Bertot; Benjamin Grégoire; Xavier Leroy (TYPES, 2004)

Interactive Theorem Proving and Program Development - Coq'Art: The Calculus of Inductive Constructions - Yves Bertot; Pierre Castéran (Springer, 2004)

Filters on CoInductive Streams, an Application to Eratosthenes' Sieve. - Yves Bertot (TLCA, 2005)

Dependent Types, Theorem Proving, and Applications for a Verifying Compiler. - Yves Bertot; Laurent Théry (VSTTE, 2005)

Vérification formelle d'extractions de racines entières. - Yves Bertot (Tech. Sci. Informatiques, 2005)

Coq in a Hurry - Yves Bertot (CoRR, 2006)

CoInduction in Coq - Yves Bertot (CoRR, 2006)

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

Theorem proving support in programming language semantics - Yves Bertot (CoRR, 2007)

Affine functions and series with co-inductive real numbers. - Yves Bertot (Math. Struct. Comput. Sci., 2007)

Structural Abstract Interpretation: A Formal Study Using Coq. - Yves Bertot (LerNet ALFA Summer School, 2008)

Fixed point semantics and partial recursion in Coq. - Yves Bertot; Vladimir Komendantsky (PPDP, 2008)

A Short Presentation of Coq. - Yves Bertot (TPHOLs, 2008)

Canonical Big Operators. - Yves Bertot; Georges Gonthier; Sidi Ould Biha; Ioana Pasca (TPHOLs, 2008)

Using Structural Recursion for Corecursion. - Yves Bertot; Ekaterina Komendantskaya (TYPES, 2008)

Inductive and Coinductive Components of Corecursive Functions in Coq. - Yves Bertot; Ekaterina Komendantskaya (CMCS, 2008)

Formal Proof of Theorems on Genetic Regulatory Networks. - Maxime Dénès; Benjamin Lesage; Yves Bertot; Adrien Richard (SYNASC, 2009)

Formal Study of Plane Delaunay Triangulation. - Jean-François Dufourd; Yves Bertot (ITP, 2010)

A Combination of a Dynamic Geometry Software With a Proof Assistant for Interactive Formal Proofs. - Tuan-Minh Pham; Yves Bertot (UITP, 2010)

A Coq-Based Library for Interactive and Automated Theorem Proving in Plane Geometry. - Tuan-Minh Pham; Yves Bertot; Julien Narboux (ICCSA (4), 2011)

A formal study of Bernstein coefficients and polynomials. - Yves Bertot; Frédérique Guilhot; Assia Mahboubi (Math. Struct. Comput. Sci., 2011)

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 001; Assia Mahboubi; Russell O'Connor; Sidi Ould Biha; Ioana Pasca; Laurence Rideau; et al. (ITP, 2013)

Views of PI: Definition and computation. - Yves Bertot; Guillaume Allais (J. Formaliz. Reason., 2014)

Fixed Precision Patterns for the Formal Verification of Mathematical Constant Approximations. - Yves Bertot (CPP, 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)

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 (CPP, 2016)

Distant decimals of $π$. - Yves Bertot; Laurence Rideau; Laurent Théry (CoRR, 2017)

Formal Verification of a Geometry Algorithm: A Quest for Abstract Views and Symmetry in Coq Proofs. - Yves Bertot (ICTAC, 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)

C floating-point proofs layered with VST and Flocq. - Andrew W. Appel; Yves Bertot (J. Formaliz. Reason., 2020)

Corrigendum: C floating-point proofs layered with VST and Flocq. - Andrew W. Appel; Yves Bertot (J. Formaliz. Reason., 2020)

Safe Smooth Paths Between Straight Line Obstacles. - Yves Bertot (Logics and Type Systems in Theory and Practice, 2024)