Laurence Rideau

19 papers B 2Misc 1Journal 8Unranked 7
YearRankTypeTitle / Venue / Authors
2023 J jnl
Accurate Calculation of Euclidean Norms Using Double-word Arithmetic.
ACM Trans. Math. Softw.
Vincent Lefèvre, Nicolas Louvet, Jean-Michel Muller, Joris Picot, Laurence Rideau
2022 J jnl
Formalization of Double-Word Arithmetic, and Comments on "Tight and Rigorous Error Bounds for Basic Building Blocks of Double-Word Arithmetic".
ACM Trans. Math. Softw.
Jean-Michel Muller, Laurence Rideau
2018 J jnl
Distant Decimals of π : Formal Proofs of Some Algorithms Computing Them and Guarantees of Exact Computation.
J. Autom. Reason.
Yves Bertot, Laurence Rideau, Laurent Théry
2017 J jnl
Distant decimals of $π$.
CoRR
Yves Bertot, Laurence Rideau, Laurent Théry
2016 B conf
Formal proofs of transcendence for e and pi as an application of multivariate and symmetric polynomials.
CPP
Sophie Bernard, Yves Bertot, Laurence Rideau, Pierre-Yves Strub
2015 J jnl
Formal Proofs of Transcendence for e and $π$ as an Application of Multivariate and Symmetric Polynomials.
CoRR
Sophie Bernard, Yves Bertot, Laurence Rideau, Pierre-Yves Strub
2013 B conf
A Machine-Checked Proof of the Odd Order Theorem.
ITP
Georges Gonthier, Andrea Asperti, Jeremy Avigad, Yves Bertot, Cyril Cohen, François Garillot, Stéphane Le Roux, Assia Mahboubi, Russell O'Connor, Sidi Ould Biha, Ioana Pasca, Laurence Rideau, Alexey Solovyev, Enrico Tassi, Laurent Théry
2013 Misc conf
Certified, Efficient and Sharp Univariate Taylor Models in COQ.
SYNASC
Érik Martin-Dorel, Laurence Rideau, Laurent Théry, Micaela Mayero, Ioana Pasca
2012 — conf
Rigorous Polynomial Approximation Using Taylor Models in Coq.
NASA Formal Methods
Nicolas Brisebarre, Mioara Joldes, Érik Martin-Dorel, Micaela Mayero, Jean-Michel Muller, Ioana Pasca, Laurence Rideau, Laurent Théry
2011 — conf
Incidence Simplicial Matrices Formalized in Coq/SSReflect.
Calculemus/MKM
Jónathan Heras, María Poza, Maxime Dénès, Laurence Rideau
2010 — ed.
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
AISC/MKM/Calculemus
Serge Autexier, Jacques Calmet, David Delahaye, Patrick D. F. Ion, Laurence Rideau, Renaud Rioboo, Alan P. Sexton
2009 — conf
Packaging Mathematical Structures.
TPHOLs
François Garillot, Georges Gonthier, Assia Mahboubi, Laurence Rideau
2008 J jnl
Tilting at Windmills with Coq: Formal Verification of a Compilation Algorithm for Parallel Moves.
J. Autom. Reason.
Laurence Rideau, Bernard P. Serpette, Xavier Leroy
2007 — conf
A Modular Formalisation of Finite Group Theory.
TPHOLs
Georges Gonthier, Assia Mahboubi, Laurence Rideau, Enrico Tassi, Laurent Théry
2003 — conf
TEXmacs as Authoring Tool for Formal Developments.
UITP@TPHOLs
Philippe Audebaud, Laurence Rideau
2002 J jnl
Affichage et manipulation interactive de formules mathématiques dans les documents structurés.
ARIMA J.
Hanane Naciri, Laurence Rideau
2001 — conf
A Generic Library for Floating-Point Numbers and Its Application to Exact Computing.
TPHOLs
Marc Daumas, Laurence Rideau, Laurent Théry
1999 J jnl
CtCoq: an environment for mathematical reasoning.
SIGSAM Bull.
Yves Bertot, Laurence Rideau, Loïc Pottier, Laurent Thiry
1994 — conf
Towards a multi-formalism framework for architectural synthesis: the ASAR project.
CODES
Michel Auguin, Mohamed Belhadj, Judith Benzakki, C. Carrière, Guy Durrieu, Thierry Gautier, Michel Israël, Paul Le Guernic, Michel Lemaître, E. Martin, Patrice Quinton, Laurence Rideau, Frédéric Rousseau, Olivier Sentieys