Note: these publications are listed in reverse chronological order. Click here to see recent research reports
Les publications sont énumérées dans l'ordre chronologique inverse, mais les rapports de recherche apparaissent à la fin
Coq in a hurry, preprint, regularly updated.
Andrew W. Appel, Yves Bertot C floating-point proofs layered with VST and flocq Journal of Formalized Reasoning, December 2020 (open archive version)
Yves Bertot Formal Verification of a Geometry Algorithm: A Quest for Abstract Views and Symmetry in Coq Proofs, International Colloquium on Theoretical aspects of Computing, Oct 2018, Stellenbosch, South Africa (open archive version)
Yves Bertot, Laurence Rideau, Laurent Théry Distant decimals of π : Formal proofs of some algorithms computing them and guarantees of exact computation. Journal of Automated Reasoning, December 2017 (open archive version)
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 Certified Programs and Proofs (CPP'16) (2016), ACM.
(open archive version)
Yves Bertot
Fixed Precision Patterns for the Formal Verification of Mathematical Constant Approximations Certified Programs and Proofs (CPP'15) (2015), ACM. (open archive version)
Yves Bertot Links between homotopy theory and type theory Conference on Intelligent Computer Mathematics, Jul 2014, Coimbra, Portugal (open archive version)
Yves Bertot, Guillaume Allais Views of PI: Definition and computation Journal of Formalized Reasoning, Vol 7, No. 1 (2014) (open archive version)
Georges Gonthier, Andrea Asperti, Jeremy Avigad, et al. A Machine-Checked Proof of the Odd Order Theorem Proceedings of Interactive Theorem Proving, Springer Verlag, LNCS 7998, pp. 163-179, 2013. Open archive preprint
Yves Bertot, Frédérique Guilhot, Assia
Mahboubi
A formal study of Bernstein coefficients and
polynomials
Mathematical Structures in Computer Science 21(4), pp 731-762,
2011. (DOI:10.1017/S0960129511000090)
Open archive preprint
Jean-François Dufourd, Yves Bertot
Formal Study of Plane Delaunay Triangulation
Proceedings of Interactive Theorem Proving, Springer Verlag, LNCS 6172,
pp. 211-226, 2010.
Open archive preprint
Maxime Dénès, Benjamin Lesage, Yves Bertot, and Adrien
Richard
Formal proof of theorems on genetic regulatory
networks
In Proceedings of the 11th International Symposium on Symbolic and
Numeric Algorithms for Scientific Computing (SYNASC 2009), pages
69-76. IEEE, September 2009.
Yves Bertot Theorem-Proving Support in programming language semantics, From Semantics to Computer Science, essays in Honour of Gilles Kahn, Cambridge University Press, 2009. A preprint is available in an open archive [ bib].
Yves Bertot, Vladimir Komendantsky Fixed point semantics and partial recursion in coq PPDP '08: Proceedings of the 10th international ACM SIGPLAN conference on Principles and practice of declarative programming Valencia, Spain, 2008. pages 89-96, Open archive preprint, [bib]
Yves Bertot Structural Abstract Interpretation: A Formal Study Using Coq, Language Engineering and Rigorous Software Development, International LerNet ALFA Summer School 2008, Piriapolis, Uruguay, February 24 - March 1, 2008, Revised Tutorial Lectures, Springer Verlag, LNCS 5520, pp. 153-194, 2009. An updated preprint is available (less errors), [ bib ].
Yves Bertot, Ekaterina Komendantskaya Using Structural Recursion for Corecursion Types 2008 S. Berardi, F Damiani, and U. de'Liguoro (Eds.), LNCS 5497, pp. 220-239, 2009. A preprint is available on an open archive
Yves Bertot, Ekaterina Komendantskaya Inductive and Coinductive Components of Corecursive Functions in Coq, ENTCS proceedings of CMCS'08, the 9th International Workshop on Coalgebraic Methods in Computer Science, Budapest, Hungary, April 4 - April 6, 2008, 20 pages. A preprint is available on an open archive [ bib ].
Yves Bertot, Georges Gonthier, Sidi Ould Biha, Ioana Pasca Canonical Big Operators, Proceedings of TPHOLs'08, Springer LNCS 5170, 2008, available on an open archive [ bib ].
Yves Bertot Affine functions and series with co-inductive real numbers , Mathematical Structures in Computer Science, 17(1):37-63 (2007),Cambridge University Press, pre-print available on an open archive [ bib ]
Yves Bertot, Benjamin Grégoire, Xavier Leroy
A Structured Approach to Proving Compiler Optimizations Based on Dataflow Analysis, Types'04, Springer LNCS 3839, 2006.
Yves Bertot Vérification formelle d'extractions de racines entières, Technique et science informatiques, 24(9), pp. 1161--1185, 2005. A pre-print is available on an open archive [ bib ]
Yves Bertot Filters on CoInductive Streams, an Application to Eratosthenes' Sieve , Proceedings of TLCA'05, Springer LNCS 3461, 2005. A preliminary version is available as INRIA research report RR-5343
Yves Bertot, Pierre Castéran
Interactive Theorem Proving and Program Development:
Coq'Art: The Calculus of Inductive Constructions,
Springer Verlag, EATCS Texts in Theoretical Computer Science, ISBN
3-540-20854-2
(associated internet site).
Milad Niqui, Yves Bertot
``QArith: Coq Formalization of Lazy Rational Arithmetic",
Types 2003, LNCS 3085. open archive version
Y. Bertot, F. Guilhot, Loïc Pottier Visualizing Geometrical Statements with GeoView, Proceedings of the Workshop User Interfaces for Theorem Provers in connection withTPHOLs'2003, Rome, Italy, September 2003
Yves Bertot
``A Simple
canonical representation of rational numbers'', Mathematics, Logic
and Computation, ENTCS
Volume 85.7, September 2003.
Yves Bertot, Nicolas Magaud, and Paul Zimmermann
``A Proof of GMP Square Root'', Journal of Automated Reasoning
29(3-4):225-252, 2002. Special Issue on Automating and Mechanising
Mathematics: In honour of N.G. de Bruijn (an earlier version is
available as a research report).
Yves Bertot, Venanzio Capretta, and
Kuntal Das Barman
``
Type-theoretic functional semantics
'',
TPHOLs'2002, LNCS 2410, pp. 83-98.
Yves Bertot,
``
Des descriptions fonctionnelles aux implémentations impératives de
programmes'', Proceedings of Journées francophones des langages
applicatifs, JFLA'02, INRIA (in French).
Antonia Balaa and Yves
Bertot,
``
Fonctions récursives générales par itération en théorie des types'',
Proceedings of Journées francophones des langages applicatifs,
JFLA'02, INRIA (in French).
David Pichardie and Yves Bertot,
``
Formalizing Convex Hulls Algorithms
'',
Proceedings of TPHOLs'01, LNCS 2152, pp. 346-361.
Ahmed Amerkad, Yves Bertot, Laurence Rideau,
and Loïc Pottier,
``
Mathematics and proof presentation in Pcoq'', Proceedings of Proof
Transformation and Presentation and Proof Complexities (PTP'01),
Sienna, Italy.
Yves Bertot
``
Formalizing a JVML verifier for initialization in a theorem prover
'',
Proceedings of CAV'01, LNCS 2102, pp. 14--24, July 2001.
short version of INRIA Research Report RR-4047, November 2000.
Nicolas Magaud and Yves Bertot,
``Changing
Data Structures in Type Theory: A Study of Natural Numbers'',
Proceedings of Types2000, LNCS 2277, pp. 181-196.
Antonia Balaa and Yves Bertot,
``Fix-point
Equations for Well-Founded Recursion in Type Theory'',
Proceedings of TPHOLs'2000, LNCS 1869, 2000.
Yves Bertot, Gilles Dowek, André Hirschowitz, Christine Paulin,
and Laurent Théry,
Theorem Proving in Higher Order
Logics (TPHOLs99), volume 1690 of Lecture Notes on Computer
Science, Springer Verlag, Nice, France, September, 1999.
Yves Bertot,
``The CtCoq System: Design and
Architecture'',
Formal aspects of Computing, Vol. 11, pp. 225-243, 1999.
Yves Bertot and Laurent Théry,
``
A Generic Approach to Building User Interfaces for Theorem Provers'',
the Journal of Symbolic Computation Vol. 25, pp. 161-194, 1998.
Yves Bertot,
``
Head-tactics simplification''
Algebraic Methodology and Software Technology, volume 1349 of
Lecture Notes on Computer Science, Springer Verlag,
Sydney, Australia, December, 1997.
Yves Bertot,
``
Direct manipulation of Algebraic Formulae in Interactive Proof Systems
'',
Workshop on
User-Interfaces for Theorem Provers, September 1997.
Janet Bertot and Yves Bertot,
``
CtCoq: a system presentation'',
Automated Deduction (CADE-13), volume 1104 of Lecture Notes in
Artificial Intelligence, Springer-Verlag,
New Brunswick, NJ, USA, July 1996
Janet Bertot and Yves Bertot,
``
The CtCoq experience'',
User Interfaces for Theorem Provers'96,
York (UK), July 1996.
Yves Bertot and Ranan Fraer,
``
Reasoning with Executable Specifications'',
International Joint Conference of Theory and Practice of
Software Development (TAPSOFT/FASE'95), Springer-Verlag LNCS 915,
Aarhus (Denmark), May 1995.
Yves Bertot, Gilles Kahn, and Laurent Théry,
``
Proof by Pointing'' (pdf file),
Symposium on Theoretical Aspects Computer Software (STACS),
Sendai (Japan), LNCS 789, April 1994.
Also appears as Cambridge University Research Report (December 1993).
Laurent Théry, Yves Bertot, and Gilles Kahn,
``
Real Theorem Provers Deserve Real User-Interfaces''
The Fifth ACM Symposium on Software Development Environments (SDE5),
Washington D. C., December 1992.
Also appears as Inria Research Report no. 1684 (May 1992).
Yves Bertot,
``
A Canonical Calculus of Residuals'',
In Logical Environments, Gerard Huet and Gordon Plotkin, editors,
Cambridge University Press, December 1993.
Yves Bertot,
``
Origin Functions in Lambda-calculus and Term Rewriting Systems'',
Proceedings of CAAP'92, Caen (France), February 1992.
Also appears as Inria Research Report no. 1543 (October 1991).
Y. Bertot,
``
Occurrences in Debugger Specifications'',
Proceedings of the 1991 ACM SIGPLAN Programming Language Design and
Implementation (PLDI) Conference, Toronto, June 1991.
Also appears as Inria Research Report no. 1350 (December 1990).
Yves Bertot,
``
Implementation of an Interpreter for a Parallel Language in Centaur
'',
3rd European Symposium on Programming, Copenhague, Denmark,
LNCS 432, May 1990.
Also appears as Inria Research Report
no. 1076 (August 1989).
Yves Bertot,
``
Programming Languages Specifications and Environments
''
A course on describing programming languages for the Centaur
environment and proving properties of these languages,
INRIA Research Report RT-210,
December 1997.
Janet Bertot, Yves Bertot, Yann Coscoy, Healfdene Goguen, and
Francis Montagnac,
``
INRIA Research Report RT-210,
User Guide to the CtCoq Proof Environment'',
October 1997.
Yves Bertot, Thomas Kleymann-Schreiber, Dilip Sequeira,
``
Implementing Proof by Pointing without a Structure Editor
''
INRIA Research Report RR-3286, October 1997.
Yves Bertot,
``
A certified compiler for an imperative language
''
INRIA Research Report RR-3488, September 1998.
Yves Bertot and Olivier Pons and Loïc
Pottier
``
Dependency graphs for interactive theorem provers''
INRIA Research Report RR-4052, November 2000.
Yves Bertot
``
A Coq Formalization of a Type Checker for Object Initialization in the
Java Virtual Machine''
INRIA Research Report RR-4047, November 2000.
Yves Bertot and Nicolas Magaud
and Paul Zimmermann
``
A proof of GMP square root using the Coq assistant''
INRIA Research Report RR-4475, June 2002.