Towards a multi-formalism framework for architectural synthesis: the ASAR project. - 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; et al. (CODES, 1994)

CtCoq: an environment for mathematical reasoning. - Yves Bertot; Laurence Rideau; Loïc Pottier; Laurent Thiry (SIGSAM Bull., 1999)

A Generic Library for Floating-Point Numbers and Its Application to Exact Computing. - Marc Daumas; Laurence Rideau; Laurent Théry (TPHOLs, 2001)

Affichage et manipulation interactive de formules mathématiques dans les documents structurés. - Hanane Naciri; Laurence Rideau (ARIMA J., 2002)

TEXmacs as Authoring Tool for Formal Developments. - Philippe Audebaud; Laurence Rideau (UITP@TPHOLs, 2003)

A Modular Formalisation of Finite Group Theory. - Georges Gonthier; Assia Mahboubi; Laurence Rideau; Enrico Tassi; Laurent Théry (TPHOLs, 2007)

Tilting at Windmills with Coq: Formal Verification of a Compilation Algorithm for Parallel Moves. - Laurence Rideau; Bernard P. Serpette; Xavier Leroy (J. Autom. Reason., 2008)

Packaging Mathematical Structures. - François Garillot; Georges Gonthier; Assia Mahboubi; Laurence Rideau (TPHOLs, 2009)

Incidence Simplicial Matrices Formalized in Coq/SSReflect. - Jónathan Heras; María Poza; Maxime Dénès; Laurence Rideau (Calculemus/MKM, 2011)

Rigorous Polynomial Approximation Using Taylor Models in Coq. - Nicolas Brisebarre; Mioara Joldes; Érik Martin-Dorel; Micaela Mayero; Jean-Michel Muller; Ioana Pasca; Laurence Rideau; Laurent Théry (NASA Formal Methods, 2012)

A Machine-Checked Proof of the Odd Order Theorem. - Georges Gonthier; Andrea Asperti; Jeremy Avigad; Yves Bertot; Cyril Cohen; François Garillot; Stéphane Le Roux 001; Assia Mahboubi; Russell O'Connor; Sidi Ould Biha; Ioana Pasca; Laurence Rideau; et al. (ITP, 2013)

Certified, Efficient and Sharp Univariate Taylor Models in COQ. - Érik Martin-Dorel; Laurence Rideau; Laurent Théry; Micaela Mayero; Ioana Pasca (SYNASC, 2013)

Formal Proofs of Transcendence for e and $π$ as an Application of Multivariate and Symmetric Polynomials. - Sophie Bernard; Yves Bertot; Laurence Rideau; Pierre-Yves Strub (CoRR, 2015)

Formal proofs of transcendence for e and pi as an application of multivariate and symmetric polynomials. - Sophie Bernard; Yves Bertot; Laurence Rideau; Pierre-Yves Strub (CPP, 2016)

Distant decimals of $π$. - Yves Bertot; Laurence Rideau; Laurent Théry (CoRR, 2017)

Distant Decimals of π : Formal Proofs of Some Algorithms Computing Them and Guarantees of Exact Computation. - Yves Bertot; Laurence Rideau; Laurent Théry (J. Autom. Reason., 2018)

Formalization of Double-Word Arithmetic, and Comments on "Tight and Rigorous Error Bounds for Basic Building Blocks of Double-Word Arithmetic". - Jean-Michel Muller; Laurence Rideau (ACM Trans. Math. Softw., 2022)

Accurate Calculation of Euclidean Norms Using Double-word Arithmetic. - Vincent Lefèvre; Nicolas Louvet; Jean-Michel Muller; Joris Picot; Laurence Rideau (ACM Trans. Math. Softw., 2023)