Skip to Main content Skip to Navigation


...
inria-00584918v1  Conference papers
Tuan Minh PhamYves BertotJulien 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. pp.368-383, ⟨10.1007/978-3-642-21898-9_32⟩
...
inria-00585400v1  Conference papers
Tuan Minh PhamYves 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
...
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
...
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-00083975v1  Lectures
Yves Bertot. lambda-calcul et types
Ecole Jeunes Chercheurs en Programmation (CNRS-INRIA) Toulouse, 2006
...
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-01074926v1  Journal articles
Yves BertotGuillaume 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⟩
hal-01240025v1  Conference papers
Sophie BernardYves BertotLaurence RideauPierre-Yves Strub. Formal Proofs of Transcendence for e and π as an Application of Multivariate and Symmetric Polynomials
Certified Programs and Proofs, Jan 2016, St Petersburg, Florida, United States. pp.12
...
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-00160309v2  Reports
Yves Bertot. Theorem proving support in programming language semantics
[Research Report] RR-6242, INRIA. 2007, pp.23
...
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