Skip to Main content Skip to Navigation
  1. Search


...
inria-00000480v1  Conference papers
Yves Bertot. Calcul de formules affines et de séries entières en arithmétique exacte avec types co-inductifs
Journées Francophones des Langages Applicatifs, INRIA, Jan 2006, Pauillac, pp.41-55
...
inria-00073912v1  Reports
Yves Bertot, Ranan Fraer. Reasoning with Executable Specifications
RR-2780, INRIA. 1996
...
inria-00076907v1  Reports
Laurent Théry, Yves Bertot, Gilles Kahn. Real theorem provers deserve real user-interfaces
[Research Report] RR-1684, INRIA. 1992
...
inria-00072274v1  Reports
Ahmed Amerkad, Yves Bertot, Loïc Pottier, Laurence Rideau. Mathematics and Proof Presentation in Pcoq
RR-4313, INRIA. 2001
...
inria-00075019v1  Reports
Yves Bertot. The Origins of lambda-calculus and term rewriting systems
[Research Report] RR-1543, INRIA. 1991, pp.19
...
inria-00075020v1  Reports
Yves Bertot. A Canonical calculus of residuals
[Research Report] RR-1542, INRIA. 1991, pp.12
...
inria-00073402v1  Reports
Yves Bertot, Thomas Kleymann-Schreiber, Dilip Sequeira. Implementing Proof by Pointing without a Structure Editor
RR-3286, INRIA. 1997
...
inria-00072591v1  Reports
Yves Bertot. A Coq Formalization of a Type Checker for Object Initialization in the Java Virtual Machine
[Research Report] RR-4047, INRIA. 2000, pp.53
...
inria-00069961v1  Reports
Janet Bertot, Yves Bertot, Yann Coscoy, Healfdene Goguen, Francis Montagnac. User Guide to the CTCOQ Proof Environment
[Technical Report] RT-0210, INRIA. 1997, pp.63
...
inria-00073145v1  Reports
Yves Bertot. The CtCoq System: Design and Architecture
RR-3540, INRIA. 1998
...
inria-00069959v1  Reports
Yves Bertot. Programming Language Specifications and Environments
[Technical Report] RT-0212, INRIA. 1997, pp.47
...
inria-00073199v1  Reports
Yves Bertot. A certified Compiler for an Imperative Language
RR-3488, INRIA. 1998
...
inria-00072599v1  Reports
Nicolas Magaud, Yves Bertot. Changements de représentation des données dans le calcul des constructions inductives
[Rapport de recherche] RR-4039, INRIA. 2000, pp.29
...
inria-00077041v1  Reports
Milad Niqui, Yves Bertot. QArith: Coq Formalisation of Lazy Rational Arithmetic
[Research Report] RR-5004, INRIA. 2003, pp.19
...
inria-00072585v1  Reports
Yves Bertot, Olivier Pons, Loïc Pottier. Graphes de dépendance pour les démonstrateurs de théorèmes intéractifs
RR-4052, INRIA. 2000
...
inria-00071449v1  Reports
Kuntal das Barman, Yves Bertot. Proof by reflection in semantics
RR-5134, INRIA. 2004
...
inria-00070657v1  Reports
Yves Bertot. Vérification formelle d'extractions de racines
RR-5344, INRIA. 2004, pp.23
...
inria-00070658v1  Reports
Yves Bertot. Filters on Co-Inductive streams: an application to Eratosthenes' sieve
RR-5343, INRIA. 2004, pp.21
...
inria-00075483v1  Reports
Yves Bertot. Implementation of an interpreter for a parallel language in CENTAUR
[Research Report] RR-1076, INRIA. 1989, pp.27
...
inria-00075209v1  Reports
Yves Bertot. Occurences in debugger specifications
[Research Report] RR-1350, INRIA. 1990, pp.13
...
hal-00816699v1  Conference papers
Georges Gonthier, Andrea Asperti, Jeremy Avigad, Yves Bertot, Cyril Cohen et al.  A Machine-Checked Proof of the Odd Order Theorem
ITP 2013, 4th Conference on Interactive Theorem Proving, Jul 2013, Rennes, France. pp.163-179, ⟨10.1007/978-3-642-39634-2_14⟩
...
inria-00277075v2  Conference papers
Yves Bertot, Ekaterina Komendantskaya. Inductive and Coinductive Components of Corecursive Functions in Coq
Coalgebraic Methods in Computer Science, Apr 2008, Budapest, Hungary
...
hal-01074927v1  Conference papers
Yves Bertot. Fixed Precision Patterns for the Formal Verification of Mathematical Constant Approximations
Certified Programs and Proofs (CPP'15), Jan 2015, Mumbai, India. ⟨10.1145/2676724.2693172⟩
...
inria-00322331v4  Conference papers
Yves Bertot, Ekaterina Komendantskaya. Using Structural Recursion for Corecursion
Types 2008, 2008, Torino, Italy. pp.220-236
...
hal-01582524v2  Journal articles
Yves Bertot, Laurence Rideau, Laurent Théry. Distant decimals of $π$
Journal of Automated Reasoning, Springer Verlag, In press, pp.1-45
...
hal-00987248v1  Conference papers
Yves Bertot. Links between homotopy theory and type theory
CICM - Conference on Intelligent Computer Mathematics, Jul 2014, Coimbra, Portugal
...
inria-00329572v2  Conference papers
Yves Bertot. Structural abstract interpretation, A formal study using Coq
LERNET Summer School, Ana Bove and Jorge Sousa Pinto, Feb 2008, Piriapolis, Uruguay
...
hal-01866271v1  Conference papers
Yves Bertot. Formal Verification of a Geometry Algorithm: A Quest for Abstract Views and Symmetry in Coq Proofs
ICTAC 2018 - International Colloquium on Theoretical of Computing, Oct 2018, Stellenbosch, South Africa