Laurence Rideau

Université Côte d'Azur — France

Computer Science · Physical Sciences

10h-index666citations38works0.02yr avg
OpenAlex↗ORCID↗Google Scholar↗Lab page↗

Accepting Students?

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

Research Topics

Logic, programming, and type systems(14), Numerical Methods and Algorithms(8), Mathematics, Computing, and Information Processing(6), Parallel Computing and Optimization Techniques(5), Formal Methods in Verification(4)

Publications38 total

Accurate Calculation of Euclidean Norms Using Double-word Arithmetic
ACM Transactions on Mathematical Software·2022Open Access
Formalization of Double-Word Arithmetic, and Comments on “Tight and Rigorous Error Bounds for Basic Building Blocks of Double-Word Arithmetic”
ACM Transactions on Mathematical Software·2022Open 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
Formalization and Concretization of Ordered Networks
2016Open 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
Certified, Efficient and Sharp Univariate Taylor Models in COQ
2013· 11 cited
A Machine-Checked Proof of the Odd Order Theorem
Lecture notes in computer science·2013· 274 citedOpen Access
Rigorous Polynomial Approximation Using Taylor Models in Coq
Lecture notes in computer science·2012· 16 cited
Incidence Simplicial Matrices Formalized in Coq/SSReflect
Lecture notes in computer science·2011· 15 citedOpen Access
New Results - Type theory and formalization ofmathematics
2011
Intelligent Computer Mathematics, 10th International Conference, AISC 2010, 17th Symposium, Calculemus 2010, and 9th International Conference, MKM 2010, Paris, France, July 5-10, 2010. Proceedings
HAL (Le Centre pour la Communication Scientifique Directe)·2010· 5 cited
Proceedings of the 10th ASIC and 9th MKM international conference, and 17th Calculemus conference on Intelligent computer mathematics
2010
Packaging Mathematical Structures
Lecture notes in computer science·2009· 129 cited
Tilting at Windmills with Coq: Formal Verification of a Compilation Algorithm for Parallel Moves
Journal of Automated Reasoning·2008· 21 citedOpen Access
page 1 of 2Next →

Frequent Co-authors

Yves Bertot(15), Laurent Théry(11), Loïc Pottier(6), Georges Gonthier(5), Bernard Serpette(4), Pierre-Yves Strub(4), Philippe Audebaud(4), Hanane Naciri(4), Assia Mahboubi(3), E. ̃Tassi(3), Assia Mahboubi(3), Jean‐Michel Muller(3), Sophie Bernard(3), Frédérique Guilhot(3), François Garillot(2), Sidi Ould Biha(2), Ioana Paşca(2), Marc Daumas(2), Ahmed Amerkad(2), Xavier Leroy(2)