Skip to Main content Skip to Navigation

inria-00503017v2  Journal articles
Yves BertotFrédérique GuilhotAssia Mahboubi. A formal study of Bernstein coefficients and polynomials
Mathematical Structures in Computer Science, Cambridge University Press (CUP), 2011, 21 (04), pp.731-761. ⟨10.1017/S0960129511000090⟩
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
hal-01702679v1  Conference papers
David PichardieYves Bertot. Formalizing Convex Hulls Algorithms
TPHOLs 2001 - 14th International Conference Theorem Proving in Higher Order Logics, Sep 2001, Edinburgh, United Kingdom. pp.346-361, ⟨10.1007/3-540-44755-5_24⟩
hal-03130704v2  Journal articles
Andrew AppelYves Bertot. C-language floating-point proofs layered with VST and Flocq
Journal of Formalized Reasoning, ASDD-AlmaDL, 2020, 13 (1), pp.1-16. ⟨10.6092/issn.1972-5787/11442⟩
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-00069959v1  Reports
Yves Bertot. Programming Language Specifications and Environments
[Technical Report] RT-0212, INRIA. 1997, pp.47
inria-00077041v1  Reports
Milad NiquiYves Bertot. QArith: Coq Formalisation of Lazy Rational Arithmetic
[Research Report] RR-5004, INRIA. 2003, pp.19
inria-00075209v1  Reports
Yves Bertot. Occurences in debugger specifications
[Research Report] RR-1350, INRIA. 1990, pp.13
hal-00816699v1  Conference papers
Georges GonthierAndrea AspertiJeremy AvigadYves BertotCyril 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 BertotEkaterina Komendantskaya. Inductive and Coinductive Components of Corecursive Functions in Coq
Coalgebraic Methods in Computer Science, Apr 2008, Budapest, Hungary
inria-00322331v4  Conference papers
Yves BertotEkaterina Komendantskaya. Using Structural Recursion for Corecursion
Types 2008, 2008, Torino, Italy. pp.220-236
hal-01582524v2  Journal articles
Yves BertotLaurence RideauLaurent 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