Yves Bertot

Tuan-Minh Pham, Yves Bertot: A Combination of a Dynamic Geometry Software With a Proof Assistant for Interactive Formal Proofs. Electr. Notes Theor. Comput. Sci. 285: 43-55 (2012)

Yves Bertot, Frédérique Guilhot, Assia Mahboubi: A formal study of Bernstein coefficients and polynomials. Mathematical Structures in Computer Science 21(4): 731-761 (2011)

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

Jean-François Dufourd, Yves Bertot: Formal Study of Plane Delaunay Triangulation. ITP 2010: 211-226

Jean-François Dufourd, Yves Bertot: Formal study of plane Delaunay triangulation. CoRR abs/1007.3350 (2010)

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

Yves Bertot, Ekaterina Komendantskaya: Using Structural Recursion for Corecursion. CoRR abs/0903.3850 (2009)

Yves Bertot, Ekaterina Komendantskaya: Inductive and Coinductive Components of Corecursive Functions in Coq. Electr. Notes Theor. Comput. Sci. 203(5): 25-47 (2008)

Yves Bertot: Structural Abstract Interpretation: A Formal Study Using Coq. LerNet ALFA Summer School 2008: 153-194

Yves Bertot, Vladimir Komendantsky: Fixed point semantics and partial recursion in Coq. PPDP 2008: 89-96

Yves Bertot: A Short Presentation of Coq. TPHOLs 2008: 12-16

Yves Bertot, Georges Gonthier, Sidi Ould Biha, Ioana Pasca: Canonical Big Operators. TPHOLs 2008: 86-101

Yves Bertot, Ekaterina Komendantskaya: Using Structural Recursion for Corecursion. TYPES 2008: 220-236

Yves Bertot, Ekaterina Komendantskaya: Inductive and Coinductive Components of Corecursive Functions in Coq. CoRR abs/0807.1524 (2008)

Yves Bertot: Structural abstract interpretation, A formal study using Coq. CoRR abs/0810.2179 (2008)

Yves Bertot: Affine functions and series with co-inductive real numbers. Mathematical Structures in Computer Science 17(1): 37-63 (2007)

Yves Bertot: Theorem proving support in programming language semantics. CoRR abs/0707.0926 (2007)

Yves Bertot: Affine functions and series with co-inductive real numbers. CoRR abs/cs/0603117 (2006)

Yves Bertot: Coq in a Hurry. CoRR abs/cs/0603118 (2006)

Yves Bertot: CoInduction in Coq. CoRR abs/cs/0603119 (2006)

Yves Bertot: Extending the Calculus of Constructions with Tarski's fix-point theorem. CoRR abs/cs/0610055 (2006)

Yves Bertot: Vérification formelle d'extractions de racines entières. Technique et Science Informatiques 24(9): 1161-1185 (2005)

Yves Bertot: Filters on CoInductive Streams, an Application to Eratosthenes' Sieve. TLCA 2005: 102-115

Yves Bertot, Laurent Théry: Dependent Types, Theorem Proving, and Applications for a Verifying Compiler. VSTTE 2005: 173-181

Yves Bertot, Frédérique Guilhot, Loic Pottier: Visualizing Geometrical Statements with GeoView. Electr. Notes Theor. Comput. Sci. 103: 49-65 (2004)

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

Yves Bertot: Simple canonical representation of rational numbers. Electr. Notes Theor. Comput. Sci. 85(7): 1-16 (2003)

Milad Niqui, Yves Bertot: QArith: Coq Formalisation of Lazy Rational Arithmetic. TYPES 2003: 309-323

Yves Bertot, Nicolas Magaud, Paul Zimmermann: A Proof of GMP Square Root. J. Autom. Reasoning 29(3-4): 225-252 (2002)

Yves Bertot, Venanzio Capretta, Kuntal Das Barman: Type-Theoretic Functional Semantics. TPHOLs 2002: 83-98

Yves Bertot: Formalizing a JVML Verifier for Initialization in a Theorem Prover. CAV 2001: 14-24

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

David Pichardie, Yves Bertot: Formalizing Convex Hull Algorithms. TPHOLs 2001: 346-361

Antonia Balaa, Yves Bertot: Fix-Point Equations for Well-Founded Recursion in Type Theory. TPHOLs 2000: 1-16

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

Yves Bertot: The CtCoq System: Design and Architecture. Formal Asp. Comput. 11(3): 225-243 (1999)

Yves Bertot, Gilles Dowek, André Hirschowitz, C. Paulin, Laurent Théry (Eds.): Theorem Proving in Higher Order Logics, 12th International Conference, TPHOLs'99, Nice, France, September, 1999, Proceedings. Lecture Notes in Computer Science 1690, Springer 1999, isbn 3-540-66463-7

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

Yves Bertot: Head-Tactics Simplification. AMAST 1997: 16-29

Janet Bertot, Yves Bertot: CtCoq: A System Presentation. AMAST 1996: 600-603

Janet Bertot, Yves Bertot: CtCoq: A System Presentation. CADE 1996: 231-234

Yves Bertot, Ranan Fraer: Reasoning with Executable Specifications. TAPSOFT 1995: 531-545

Yves Bertot, Gilles Kahn, Laurent Théry: Proof by Pointing. TACS 1994: 141-160

Yves Bertot: Origin Functions in Lambda-Calculus and Term Rewriting Systems. CAAP 1992: 49-65

Laurent Théry, Yves Bertot, Gilles Kahn: Real theorem provers deserve real user-interfaces. SDE 1992: 120-129

Yves Bertot: Occurences in Debugger Specifications. PLDI 1991: 327-337

Yves Bertot: Implementation of an Interpreter for a Parallel Language in Centaur. ESOP 1990: 57-69