Search the dblp DataBase
Yves Bertot :
[Publications ]
[Author Rank by year ]
[Co-authors ]
[Prefers ]
[Cites ]
[Cited by ]
Publications of Author
Yves Bertot Head-Tactics Simplification. [Citation Graph (0, 0)][DBLP ] AMAST, 1997, pp:16-29 [Conf ] Janet Bertot , Yves Bertot CtCoq: A System Presentation. [Citation Graph (0, 0)][DBLP ] AMAST, 1996, pp:600-603 [Conf ] Yves Bertot Origin Functions in Lambda-Calculus and Term Rewriting Systems. [Citation Graph (0, 0)][DBLP ] CAAP, 1992, pp:49-65 [Conf ] Janet Bertot , Yves Bertot CtCoq: A System Presentation. [Citation Graph (0, 0)][DBLP ] CADE, 1996, pp:231-234 [Conf ] Yves Bertot Formalizing a JVML Verifier for Initialization in a Theorem Prover. [Citation Graph (0, 0)][DBLP ] CAV, 2001, pp:14-24 [Conf ] Yves Bertot Implementation of an Interpreter for a Parallel Language in Centaur. [Citation Graph (0, 0)][DBLP ] ESOP, 1990, pp:57-69 [Conf ] Nicolas Magaud , Yves Bertot Changement de représentation des structures de données en Coq: le cas des entiers naturels. [Citation Graph (0, 0)][DBLP ] JFLA, 2001, pp:1-16 [Conf ] Yves Bertot Occurences in Debugger Specifications. [Citation Graph (0, 0)][DBLP ] PLDI, 1991, pp:327-337 [Conf ] Yves Bertot , Gilles Kahn , Laurent Théry Proof by Pointing. [Citation Graph (0, 0)][DBLP ] TACS, 1994, pp:141-160 [Conf ] Yves Bertot , Ranan Fraer Reasoning with Executable Specifications. [Citation Graph (0, 0)][DBLP ] TAPSOFT, 1995, pp:531-545 [Conf ] Yves Bertot Filters on CoInductive Streams, an Application to Eratosthenes' Sieve. [Citation Graph (0, 0)][DBLP ] TLCA, 2005, pp:102-115 [Conf ] Antonia Balaa , Yves Bertot Fix-Point Equations for Well-Founded Recursion in Type Theory. [Citation Graph (0, 0)][DBLP ] TPHOLs, 2000, pp:1-16 [Conf ] Yves Bertot , Venanzio Capretta , Kuntal Das Barman Type-Theoretic Functional Semantics. [Citation Graph (0, 0)][DBLP ] TPHOLs, 2002, pp:83-98 [Conf ] David Pichardie , Yves Bertot Formalizing Convex Hull Algorithms. [Citation Graph (0, 0)][DBLP ] TPHOLs, 2001, pp:346-361 [Conf ] Milad Niqui , Yves Bertot QArith: Coq Formalisation of Lazy Rational Arithmetic. [Citation Graph (0, 0)][DBLP ] TYPES, 2003, pp:309-323 [Conf ] Yves Bertot , Benjamin Grégoire , Xavier Leroy A Structured Approach to Proving Compiler Optimizations Based on Dataflow Analysis. [Citation Graph (0, 0)][DBLP ] TYPES, 2004, pp:66-81 [Conf ] Nicolas Magaud , Yves Bertot Changing Data Structures in Type Theory: A Study of Natural Numbers. [Citation Graph (0, 0)][DBLP ] TYPES, 2000, pp:181-196 [Conf ] Yves Bertot Simple canonical representation of rational numbers. [Citation Graph (0, 0)][DBLP ] Electr. Notes Theor. Comput. Sci., 2003, v:85, n:7, pp:- [Journal ] Yves Bertot , Frédérique Guilhot , Loic Pottier Visualizing Geometrical Statements with GeoView. [Citation Graph (0, 0)][DBLP ] Electr. Notes Theor. Comput. Sci., 2004, v:103, n:, pp:49-65 [Journal ] Yves Bertot The CtCoq System: Design and Architecture. [Citation Graph (0, 0)][DBLP ] Formal Asp. Comput., 1999, v:11, n:3, pp:225-243 [Journal ] Yves Bertot , Nicolas Magaud , Paul Zimmermann A Proof of GMP Square Root. [Citation Graph (0, 0)][DBLP ] J. Autom. Reasoning, 2002, v:29, n:3-4, pp:225-252 [Journal ] Yves Bertot , Laurent Théry A Generic Approach to Building User Interfaces for Theorem Provers. [Citation Graph (0, 0)][DBLP ] J. Symb. Comput., 1998, v:25, n:2, pp:161-194 [Journal ] Yves Bertot Extending the Calculus of Constructions with Tarski's fix-point theorem [Citation Graph (0, 0)][DBLP ] CoRR, 2006, v:0, n:, pp:- [Journal ] Yves Bertot Affine functions and series with co-inductive real numbers [Citation Graph (0, 0)][DBLP ] CoRR, 2006, v:0, n:, pp:- [Journal ] Yves Bertot Coq in a Hurry [Citation Graph (0, 0)][DBLP ] CoRR, 2006, v:0, n:, pp:- [Journal ] Yves Bertot CoInduction in Coq [Citation Graph (0, 0)][DBLP ] CoRR, 2006, v:0, n:, pp:- [Journal ] Yves Bertot Theorem proving support in programming language semantics [Citation Graph (0, 0)][DBLP ] CoRR, 2007, v:0, n:, pp:- [Journal ] Yves Bertot Affine functions and series with co-inductive real numbers. [Citation Graph (0, 0)][DBLP ] Mathematical Structures in Computer Science, 2007, v:17, n:1, pp:37-63 [Journal ] Fixed point semantics and partial recursion in Coq. [Citation Graph (, )][DBLP ] A Short Presentation of Coq. [Citation Graph (, )][DBLP ] Canonical Big Operators. [Citation Graph (, )][DBLP ] Using Structural Recursion for Corecursion. [Citation Graph (, )][DBLP ] Dependent Types, Theorem Proving, and Applications for a Verifying Compiler. [Citation Graph (, )][DBLP ] Structural Abstract Interpretation: A Formal Study Using Coq. [Citation Graph (, )][DBLP ] Formal Study of Plane Delaunay Triangulation. [Citation Graph (, )][DBLP ] Inductive and Coinductive Components of Corecursive Functions in Coq [Citation Graph (, )][DBLP ] Structural abstract interpretation, A formal study using Coq [Citation Graph (, )][DBLP ] Using Structural Recursion for Corecursion [Citation Graph (, )][DBLP ] Formal study of plane Delaunay triangulation [Citation Graph (, )][DBLP ] Inductive and Coinductive Components of Corecursive Functions in Coq. [Citation Graph (, )][DBLP ] Search in 0.002secs, Finished in 0.341secs