Skip to Main content Skip to Navigation


...
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-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
...
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