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