Publications (Yves Bertot)

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.

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, 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.

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
``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.

Nicolas Magaud and Yves Bertot,
``Changement de représentation des structures de données en Coq: le cas des entiers naturels'', Proceedings of JFLA'2001, INRIA (in French). Also available as INRIA Research Report RR-4039.

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'',
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).

Research Reports

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.

Yves Bertot
Last modified: Fri Apr 15 15:36:19 MEST 2005