2009 |
38 | EE | Yves Bertot,
Ekaterina Komendantskaya:
Using Structural Recursion for Corecursion
CoRR abs/0903.3850: (2009) |
2008 |
37 | EE | Yves Bertot,
Vladimir Komendantsky:
Fixed point semantics and partial recursion in Coq.
PPDP 2008: 89-96 |
36 | EE | Yves Bertot:
A Short Presentation of Coq.
TPHOLs 2008: 12-16 |
35 | EE | Yves Bertot,
Georges Gonthier,
Sidi Ould Biha,
Ioana Pasca:
Canonical Big Operators.
TPHOLs 2008: 86-101 |
34 | EE | Yves Bertot,
Ekaterina Komendantskaya:
Inductive and Coinductive Components of Corecursive Functions in Coq
CoRR abs/0807.1524: (2008) |
33 | EE | Yves Bertot:
Structural abstract interpretation, A formal study using Coq
CoRR abs/0810.2179: (2008) |
32 | EE | Yves Bertot,
Ekaterina Komendantskaya:
Inductive and Coinductive Components of Corecursive Functions in Coq.
Electr. Notes Theor. Comput. Sci. 203(5): 25-47 (2008) |
2007 |
31 | EE | Yves Bertot:
Theorem proving support in programming language semantics
CoRR abs/0707.0926: (2007) |
30 | EE | Yves Bertot:
Affine functions and series with co-inductive real numbers.
Mathematical Structures in Computer Science 17(1): 37-63 (2007) |
2006 |
29 | EE | Yves Bertot:
Affine functions and series with co-inductive real numbers
CoRR abs/cs/0603117: (2006) |
28 | EE | Yves Bertot:
Coq in a Hurry
CoRR abs/cs/0603118: (2006) |
27 | EE | Yves Bertot:
CoInduction in Coq
CoRR abs/cs/0603119: (2006) |
26 | EE | Yves Bertot:
Extending the Calculus of Constructions with Tarski's fix-point theorem
CoRR abs/cs/0610055: (2006) |
2005 |
25 | EE | Yves Bertot:
Filters on CoInductive Streams, an Application to Eratosthenes' Sieve.
TLCA 2005: 102-115 |
24 | EE | Yves Bertot,
Laurent Théry:
Dependent Types, Theorem Proving, and Applications for a Verifying Compiler.
VSTTE 2005: 173-181 |
23 | EE | Yves Bertot:
Vérification formelle d'extractions de racines entières.
Technique et Science Informatiques 24(9): 1161-1185 (2005) |
2004 |
22 | EE | Yves Bertot,
Benjamin Grégoire,
Xavier Leroy:
A Structured Approach to Proving Compiler Optimizations Based on Dataflow Analysis.
TYPES 2004: 66-81 |
21 | EE | Yves Bertot,
Frédérique Guilhot,
Loic Pottier:
Visualizing Geometrical Statements with GeoView.
Electr. Notes Theor. Comput. Sci. 103: 49-65 (2004) |
2003 |
20 | EE | Milad Niqui,
Yves Bertot:
QArith: Coq Formalisation of Lazy Rational Arithmetic.
TYPES 2003: 309-323 |
19 | EE | Yves Bertot:
Simple canonical representation of rational numbers.
Electr. Notes Theor. Comput. Sci. 85(7): (2003) |
2002 |
18 | EE | Yves 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 |
16 | EE | Yves 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 |
14 | EE | David 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 |
12 | EE | Nicolas 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 |
10 | EE | Yves 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 |