The SCEAS System
Navigation Menu

Search the dblp DataBase

Title:
Author:

Yves Bertot: [Publications] [Author Rank by year] [Co-authors] [Prefers] [Cites] [Cited by]

Publications of Author

  1. Yves Bertot
    Head-Tactics Simplification. [Citation Graph (0, 0)][DBLP]
    AMAST, 1997, pp:16-29 [Conf]
  2. Janet Bertot, Yves Bertot
    CtCoq: A System Presentation. [Citation Graph (0, 0)][DBLP]
    AMAST, 1996, pp:600-603 [Conf]
  3. Yves Bertot
    Origin Functions in Lambda-Calculus and Term Rewriting Systems. [Citation Graph (0, 0)][DBLP]
    CAAP, 1992, pp:49-65 [Conf]
  4. Janet Bertot, Yves Bertot
    CtCoq: A System Presentation. [Citation Graph (0, 0)][DBLP]
    CADE, 1996, pp:231-234 [Conf]
  5. Yves Bertot
    Formalizing a JVML Verifier for Initialization in a Theorem Prover. [Citation Graph (0, 0)][DBLP]
    CAV, 2001, pp:14-24 [Conf]
  6. Yves Bertot
    Implementation of an Interpreter for a Parallel Language in Centaur. [Citation Graph (0, 0)][DBLP]
    ESOP, 1990, pp:57-69 [Conf]
  7. 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]
  8. Yves Bertot
    Occurences in Debugger Specifications. [Citation Graph (0, 0)][DBLP]
    PLDI, 1991, pp:327-337 [Conf]
  9. Yves Bertot, Gilles Kahn, Laurent Théry
    Proof by Pointing. [Citation Graph (0, 0)][DBLP]
    TACS, 1994, pp:141-160 [Conf]
  10. Yves Bertot, Ranan Fraer
    Reasoning with Executable Specifications. [Citation Graph (0, 0)][DBLP]
    TAPSOFT, 1995, pp:531-545 [Conf]
  11. Yves Bertot
    Filters on CoInductive Streams, an Application to Eratosthenes' Sieve. [Citation Graph (0, 0)][DBLP]
    TLCA, 2005, pp:102-115 [Conf]
  12. 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]
  13. Yves Bertot, Venanzio Capretta, Kuntal Das Barman
    Type-Theoretic Functional Semantics. [Citation Graph (0, 0)][DBLP]
    TPHOLs, 2002, pp:83-98 [Conf]
  14. David Pichardie, Yves Bertot
    Formalizing Convex Hull Algorithms. [Citation Graph (0, 0)][DBLP]
    TPHOLs, 2001, pp:346-361 [Conf]
  15. Milad Niqui, Yves Bertot
    QArith: Coq Formalisation of Lazy Rational Arithmetic. [Citation Graph (0, 0)][DBLP]
    TYPES, 2003, pp:309-323 [Conf]
  16. 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]
  17. 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]
  18. 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]
  19. 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]
  20. 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]
  21. 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]
  22. 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]
  23. 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]
  24. Yves Bertot
    Affine functions and series with co-inductive real numbers [Citation Graph (0, 0)][DBLP]
    CoRR, 2006, v:0, n:, pp:- [Journal]
  25. Yves Bertot
    Coq in a Hurry [Citation Graph (0, 0)][DBLP]
    CoRR, 2006, v:0, n:, pp:- [Journal]
  26. Yves Bertot
    CoInduction in Coq [Citation Graph (0, 0)][DBLP]
    CoRR, 2006, v:0, n:, pp:- [Journal]
  27. Yves Bertot
    Theorem proving support in programming language semantics [Citation Graph (0, 0)][DBLP]
    CoRR, 2007, v:0, n:, pp:- [Journal]
  28. 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]

  29. Fixed point semantics and partial recursion in Coq. [Citation Graph (, )][DBLP]


  30. A Short Presentation of Coq. [Citation Graph (, )][DBLP]


  31. Canonical Big Operators. [Citation Graph (, )][DBLP]


  32. Using Structural Recursion for Corecursion. [Citation Graph (, )][DBLP]


  33. Dependent Types, Theorem Proving, and Applications for a Verifying Compiler. [Citation Graph (, )][DBLP]


  34. Structural Abstract Interpretation: A Formal Study Using Coq. [Citation Graph (, )][DBLP]


  35. Formal Study of Plane Delaunay Triangulation. [Citation Graph (, )][DBLP]


  36. Inductive and Coinductive Components of Corecursive Functions in Coq [Citation Graph (, )][DBLP]


  37. Structural abstract interpretation, A formal study using Coq [Citation Graph (, )][DBLP]


  38. Using Structural Recursion for Corecursion [Citation Graph (, )][DBLP]


  39. Formal study of plane Delaunay triangulation [Citation Graph (, )][DBLP]


  40. Inductive and Coinductive Components of Corecursive Functions in Coq. [Citation Graph (, )][DBLP]


Search in 0.002secs, Finished in 0.341secs
NOTICE1
System may not be available sometimes or not working properly, since it is still in development with continuous upgrades
NOTICE2
The rankings that are presented on this page should NOT be considered as formal since the citation info is incomplete in DBLP
 
System created by asidirop@csd.auth.gr [http://users.auth.gr/~asidirop/] © 2002
for Data Engineering Laboratory, Department of Informatics, Aristotle University © 2002