dblp.uni-trier.dewww.uni-trier.de

Yves Bertot

List of publications from the DBLP Bibliography Server - FAQ
Coauthor Index - Ask others: ACM DL/Guide - CiteSeer - CSB - Google - MSN - Yahoo

2009
38EEYves Bertot, Ekaterina Komendantskaya: Using Structural Recursion for Corecursion CoRR abs/0903.3850: (2009)
2008
37EEYves Bertot, Vladimir Komendantsky: Fixed point semantics and partial recursion in Coq. PPDP 2008: 89-96
36EEYves Bertot: A Short Presentation of Coq. TPHOLs 2008: 12-16
35EEYves Bertot, Georges Gonthier, Sidi Ould Biha, Ioana Pasca: Canonical Big Operators. TPHOLs 2008: 86-101
34EEYves Bertot, Ekaterina Komendantskaya: Inductive and Coinductive Components of Corecursive Functions in Coq CoRR abs/0807.1524: (2008)
33EEYves Bertot: Structural abstract interpretation, A formal study using Coq CoRR abs/0810.2179: (2008)
32EEYves Bertot, Ekaterina Komendantskaya: Inductive and Coinductive Components of Corecursive Functions in Coq. Electr. Notes Theor. Comput. Sci. 203(5): 25-47 (2008)
2007
31EEYves Bertot: Theorem proving support in programming language semantics CoRR abs/0707.0926: (2007)
30EEYves Bertot: Affine functions and series with co-inductive real numbers. Mathematical Structures in Computer Science 17(1): 37-63 (2007)
2006
29EEYves Bertot: Affine functions and series with co-inductive real numbers CoRR abs/cs/0603117: (2006)
28EEYves Bertot: Coq in a Hurry CoRR abs/cs/0603118: (2006)
27EEYves Bertot: CoInduction in Coq CoRR abs/cs/0603119: (2006)
26EEYves Bertot: Extending the Calculus of Constructions with Tarski's fix-point theorem CoRR abs/cs/0610055: (2006)
2005
25EEYves Bertot: Filters on CoInductive Streams, an Application to Eratosthenes' Sieve. TLCA 2005: 102-115
24EEYves Bertot, Laurent Théry: Dependent Types, Theorem Proving, and Applications for a Verifying Compiler. VSTTE 2005: 173-181
23EEYves Bertot: Vérification formelle d'extractions de racines entières. Technique et Science Informatiques 24(9): 1161-1185 (2005)
2004
22EEYves Bertot, Benjamin Grégoire, Xavier Leroy: A Structured Approach to Proving Compiler Optimizations Based on Dataflow Analysis. TYPES 2004: 66-81
21EEYves Bertot, Frédérique Guilhot, Loic Pottier: Visualizing Geometrical Statements with GeoView. Electr. Notes Theor. Comput. Sci. 103: 49-65 (2004)
2003
20EEMilad Niqui, Yves Bertot: QArith: Coq Formalisation of Lazy Rational Arithmetic. TYPES 2003: 309-323
19EEYves Bertot: Simple canonical representation of rational numbers. Electr. Notes Theor. Comput. Sci. 85(7): (2003)
2002
18EEYves Bertot, Venanzio Capretta, Kuntal Das Barman: Type-Theoretic Functional Semantics. TPHOLs 2002: 83-98
17 Yves Bertot, Nicolas Magaud, Paul Zimmermann: A Proof of GMP Square Root. J. Autom. Reasoning 29(3-4): 225-252 (2002)
2001
16EEYves Bertot: Formalizing a JVML Verifier for Initialization in a Theorem Prover. CAV 2001: 14-24
15 Nicolas Magaud, Yves Bertot: Changement de représentation des structures de données en Coq: le cas des entiers naturels. JFLA 2001: 1-16
14EEDavid Pichardie, Yves Bertot: Formalizing Convex Hull Algorithms. TPHOLs 2001: 346-361
2000
13 Antonia Balaa, Yves Bertot: Fix-Point Equations for Well-Founded Recursion in Type Theory. TPHOLs 2000: 1-16
12EENicolas Magaud, Yves Bertot: Changing Data Structures in Type Theory: A Study of Natural Numbers. TYPES 2000: 181-196
1999
11 Yves Bertot, Gilles Dowek, André Hirschowitz, C. Paulin, Laurent Théry: Theorem Proving in Higher Order Logics, 12th International Conference, TPHOLs'99, Nice, France, September, 1999, Proceedings Springer 1999
10EEYves Bertot: The CtCoq System: Design and Architecture. Formal Asp. Comput. 11(3): 225-243 (1999)
1998
9 Yves Bertot, Laurent Théry: A Generic Approach to Building User Interfaces for Theorem Provers. J. Symb. Comput. 25(2): 161-194 (1998)
1997
8 Yves Bertot: Head-Tactics Simplification. AMAST 1997: 16-29
1996
7 Janet Bertot, Yves Bertot: CtCoq: A System Presentation. AMAST 1996: 600-603
6 Janet Bertot, Yves Bertot: CtCoq: A System Presentation. CADE 1996: 231-234
1995
5 Yves Bertot, Ranan Fraer: Reasoning with Executable Specifications. TAPSOFT 1995: 531-545
1994
4 Yves Bertot, Gilles Kahn, Laurent Théry: Proof by Pointing. TACS 1994: 141-160
1992
3 Yves Bertot: Origin Functions in Lambda-Calculus and Term Rewriting Systems. CAAP 1992: 49-65
1991
2 Yves Bertot: Occurences in Debugger Specifications. PLDI 1991: 327-337
1990
1 Yves Bertot: Implementation of an Interpreter for a Parallel Language in Centaur. ESOP 1990: 57-69

Coauthor Index

1Antonia Balaa [13]
2Kuntal Das Barman [18]
3Janet Bertot [6] [7]
4Sidi Ould Biha [35]
5Venanzio Capretta [18]
6Gilles Dowek [11]
7Ranan Fraer [5]
8Georges Gonthier [35]
9Benjamin Grégoire [22]
10Frédérique Guilhot [21]
11André Hirschowitz [11]
12Gilles Kahn [4]
13Ekaterina Komendantskaya [32] [34] [38]
14Vladimir Komendantsky [37]
15Xavier Leroy [22]
16Nicolas Magaud [12] [15] [17]
17Milad Niqui [20]
18Ioana Pasca [35]
19C. Paulin [11]
20David Pichardie [14]
21Loic Pottier [21]
22Laurent Théry [4] [9] [11] [24]
23Paul Zimmermann [17]

Colors in the list of coauthors

Copyright © Sun May 17 03:24:02 2009 by Michael Ley (ley@uni-trier.de)