 |
 |
 |
 |
|
|
|
|---|---|---|
|
inria-00073199v1
Rapport
Yves Bertot. A certified Compiler for an Imperative Language RR-3488, INRIA. 1998 |
||
|
hal-01074926v1
Article dans une revue
Yves Bertot, Guillaume Allais. Views of Pi: definition and computation Journal of Formalized Reasoning, ASDD-AlmaDL, 2014, 7 (1), pp.105-129. <10.6092/issn.1972-5787/4343> |
||
|
inria-00073402v1
Rapport
Yves Bertot, Thomas Kleymann-Schreiber, Dilip Sequeira. Implementing Proof by Pointing without a Structure Editor RR-3286, INRIA. 1997 |
||
|
|
||
|
inria-00001173v5
Cours
Yves Bertot. Coq in a Hurry 3rd cycle. Types Summer School, also used at the University of Goteborg, Nice, Ecole Jeunes Chercheurs en Programmation, Universite de Nice, 2010, pp.43 |
||
|
inria-00075019v1
Rapport
Yves Bertot. The Origins of lambda-calculus and term rewriting systems [Research Report] RR-1543, INRIA. 1991, pp.19 |
||
|
inria-00075020v1
Rapport
Yves Bertot. A Canonical calculus of residuals [Research Report] RR-1542, INRIA. 1991, pp.12 |
||
|
inria-00329572v2
Communication dans un congrès
Yves Bertot. Structural abstract interpretation, A formal study using Coq Ana Bove and Jorge Sousa Pinto. LERNET Summer School, Feb 2008, Piriapolis, Uruguay. Springer, 2008, Lecture Notes in Computer Science |
||
|
inria-00076907v1
Rapport
Laurent Thery, Yves Bertot, Gilles Kahn. Real theorem provers deserve real user-interfaces [Research Report] RR-1684, INRIA. 1992 |
||
|
inria-00077041v1
Rapport
Milad Niqui, Yves Bertot. QArith: Coq Formalisation of Lazy Rational Arithmetic [Research Report] RR-5004, INRIA. 2003, pp.19 |
||
|
inria-00073912v1
Rapport
Yves Bertot, Ranan Fraer. Reasoning with Executable Specifications RR-2780, INRIA. 1996 |
||
|
inria-00075209v1
Rapport
Yves Bertot. Occurences in debugger specifications [Research Report] RR-1350, INRIA. 1990, pp.13 |
||
|
inria-00331193v1
Communication dans un congrès
Yves Bertot, Georges Gonthier, Sidi Ould Biha, Ioana Pasca. Canonical Big Operators Theorem Proving in Higher Order Logics, Aug 2008, Montreal, Canada. 5170/2008, 2008, LNCS. <10.1007/978-3-540-71067-7> |
||
|
inria-00585400v1
Communication dans un congrès
Tuan Minh Pham, Yves Bertot. A combination of a dynamic geometry software with a proof assistant for interactive formal proofs 9th International Workshop On User Interfaces for Theorem Provers FLOC'10 Satellite Workshop, Jul 2010, Edinburgh, Scotland, United Kingdom. Elsevier, 2010, Electronic Notes in Theoretical Computer Science (ENTCS); Proceedings 9th International Workshop On User Interfaces for Theorem Provers |
||
|
inria-00584918v1
Communication dans un congrès
Tuan Minh Pham, Yves Bertot, Julien Narboux. A Coq-based Library for Interactive and Automated Theorem Proving in Plane Geometry The 11th International Conference on Computational Science and Its Applications (ICCSA 2011), Jun 2011, Santander, Spain. Springer-Verlag, 6785, pp.368-383, 2011, Lecture Notes in Computer Science. <10.1007/978-3-642-21898-9_32> |
||
|
inria-00504027v1
Communication dans un congrès
Jean-François Dufourd, Yves Bertot. Formal study of plane Delaunay triangulation Paulson, Lawrence and Kaufmann, Matt. Interactive Theorem Proving, Jul 2010, Edinburgh, United Kingdom. Springer, 6172, pp.211-226, 2010, Lecture Notes in Computer Science; Interactive Theorem Proving. <http://www.springerlink.com/content/yk74674271411315/fulltext.pdf> |
||
|
inria-00190975v11
Communication dans un congrès
Yves Bertot, Vladimir Komendantsky. Fixed point semantics and partial recursion in Coq PPDP 2008, Jul 2008, Valencia, Spain. 2008 |
||
|
inria-00001174v1
Cours
Yves Bertot. CoInduction in Coq DEA. EU's coordination action Types Goteborg, 2005 |
||
|
inria-00083975v1
Cours
Yves Bertot. lambda-calcul et types Ecole Jeunes Chercheurs en Programmation (CNRS-INRIA) Toulouse, 2006 |
||
|
hal-00987248v1
Communication dans un congrès
Yves Bertot. Links between homotopy theory and type theory Stephen Watt; James Davenport; Alan Sexton; Petr Sojka; Josef Urban. CICM - Conference on Intelligent Computer Mathematics, Jul 2014, Coimbra, Portugal. Springer, 2014 |
||
|
inria-00277075v2
Communication dans un congrès
Yves Bertot, Ekaterina Komendantskaya. Inductive and Coinductive Components of Corecursive Functions in Coq Jiri Adamek. Coalgebraic Methods in Computer Science, Apr 2008, Budapest, Hungary. 2008 |
||
|
inria-00072599v1
Rapport
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-00072585v1
Rapport
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-00072591v1
Rapport
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-00072274v1
Rapport
Ahmed Amerkad, Yves Bertot, Loïc Pottier, Laurence Rideau. Mathematics and Proof Presentation in Pcoq RR-4313, INRIA. 2001 |
||
|
hal-01074927v1
Communication dans un congrès
Yves Bertot. Fixed Precision Patterns for the Formal Verification of Mathematical Constant Approximations Certified Programs and Proofs (CPP'15), Jan 2015, Mumbai, India. ACM, 2015, <10.1145/2676724.2693172> |
||
|
hal-00816699v1
Communication dans un congrès
Georges Gonthier, Andrea Asperti, Jeremy Avigad, Yves Bertot, Cyril Cohen et al. A Machine-Checked Proof of the Odd Order Theorem Sandrine Blazy and Christine Paulin and David Pichardie. ITP 2013, 4th Conference on Interactive Theorem Proving, Jul 2013, Rennes, France. Springer, 7998, pp.163-179, 2013, LNCS. <10.1007/978-3-642-39634-2_14> |
||
|
inria-00289549v1
Communication dans un congrès
Yves Bertot, Benjamin Grégoire, Xavier Leroy. A structured approach to proving compiler optimizations based on dataflow analysis Types for Proofs and Programs, Workshop TYPES 2004, Dec 2004, Jouy-en-Josas, France. Springer, 3839, pp.66-81, 2006, Lecture Notes in Computer Science; Types for Proofs and Programs International Workshop, TYPES 2004, Revised Selected Papers. <10.1007/11617990> |
||
|
cel-01130272v1
Cours
Yves Bertot. Semantics for programming languages with Coq encodings Master. France. 2015 |
||
|
hal-01240025v1
Communication dans un congrès
Sophie Bernard, Yves Bertot, Laurence Rideau, Pierre-Yves Strub. Formal Proofs of Transcendence for e and π as an Application of Multivariate and Symmetric Polynomials Jeremy Avigad and Adam Chlipala. Certified Programs and Proofs, Jan 2016, St Petersburg, Florida, United States. ACM Press, pp.12, 2016 |
||
|
|
|