Yves Bertot

Computer Science · Physical Sciences

21h-index2.6kcitations124works0.02yr avg
OpenAlex↗ORCID↗Google Scholar↗

Accepting Students?

No reports yet. Know if this professor is taking students?

Research Topics

Logic, programming, and type systems(74), Logic, Reasoning, and Knowledge(32), Formal Methods in Verification(29), Mathematics, Computing, and Information Processing(18), Numerical Methods and Algorithms(13)

Publications124 total

Mathematical Components Analysis
SPIRE - Sciences Po Institutional REpository·2025
The challenges of using Type Theory to teach Mathematics
Electronic Proceedings in Theoretical Computer Science·2024Open Access
Safe Smooth Paths Between Straight Line Obstacles
Lecture notes in computer science·2024Open Access
Porting Coq Scripts to the Mathematical Components Library Version 2
SPIRE - Sciences Po Institutional REpository·2023Open Access
Porting the Mathematical Components library to Hierarchy Builder
HAL (Le Centre pour la Communication Scientifique Directe)·2021Open Access
Corrigendum: C floating-point proofs layered with VST and Flocq
SHILAP Revista de lepidopterología·2021Open Access
Requirements on the Use of Coq in the Context of Common Criteria Evaluations
SPIRE - Sciences Po Institutional REpository·2020· 2 citedOpen Access
C floating-point proofs layered with VST and Flocq
2020· 3 citedOpen Access
Formal Verification of a Geometry Algorithm: A Quest for Abstract Views and Symmetry in Coq Proofs
HAL (Le Centre pour la Communication Scientifique Directe)·2018Open Access
Formal study in Coq of pi computations using arithmetic-geometric means
HAL (Le Centre pour la Communication Scientifique Directe)·2018
Formal Verification of a Geometry Algorithm: A Quest for Abstract Views and Symmetry in Coq Proofs
Lecture notes in computer science·2018· 5 citedOpen Access
Distant Decimals of $$\pi $$ π : Formal Proofs of Some Algorithms Computing Them and Guarantees of Exact Computation
Journal of Automated Reasoning·2017
Distant decimals of $π$
arXiv (Cornell University)·2017Open Access
Distant decimals of $\pi$
arXiv (Cornell University)·2017Open Access
Formal proofs of transcendence for e and pi as an application of multivariate and symmetric polynomials
2016· 13 cited
New Results - A book on mathematical components
2016· 4 cited
Formal Proofs of Transcendence for e and $\\pi$ as an Application of\n Multivariate and Symmetric Polynomials
arXiv (Cornell University)·2015Open Access
Formal Proofs of Transcendence for e and $\pi$ as an Application of Multivariate and Symmetric Polynomials
arXiv (Cornell University)·2015Open Access
Formal Proofs of Transcendence for e and $π$ as an Application of Multivariate and Symmetric Polynomials
arXiv (Cornell University)·2015Open Access
Semantics for programming languages with Coq encodings
HAL (Le Centre pour la Communication Scientifique Directe)·2015Open Access
page 1 of 7Next →

Frequent Co-authors

Laurent Théry(6), Laurence Rideau(4), Georges Gonthier(3), Gilles Kahn(3), Ekaterina Komendantskaya(3), Pierre Castéran(2), Assia Mahboubi(2), Sidi Ould Biha(2), Ioana Paşca(2), E. ̃Tassi(2), Nicolas Magaud(2), Xavier Leroy(2), Loïc Pottier(2), Frédérique Guilhot(2), Janet Bertot(2), Andrea Asperti(1), Jeremy Avigad(1), Cyril Cohen(1), François Garillot(1), Stéphane Le Roux(1)