Laurence RIDEAU

[French]
  • Organisation: INRIA
  • Research Unit: Sophia Antipolis
  • Project: MARELLE
  • Phone : +33 04 92 38 78 04
  • Fax : +33 04 92 38 76 33
  • E-mail:(my first name).(my name)@inria.fr

    •  

     

    Research Interests

    Administrative Experience

    Development and Industrial Relationship Manager (CDRI.) for the INRIA Sophia-Antipolis Research Center from 1995 to 2000 (february).

    References

    Main Publications

    V. Lefèvre, N. Louvet, J.-M. Muller, J. Picot and L. Rideau Accurate calculation of Euclidean Norms using Double-word arithmetic ACM Transactions on Mathematical Software, Vol. 49, issue 1, March 2023, https://doi.org/10.1145/3568672.

    J.-M. Muller and Laurence Rideau 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, Vol. 48 No 1, DOI 10.1145/3484514, March 2022.

    Yves Bertot, Laurence Rideau, Laurent Théry Distant decimals of π : Formal proofs of some algorithms computing them and guarantees of exact computation. Journal of Automated Reasoning, December 2017 (open archive version)

    Georges Gonthier & al.
    A Machine-Checked Proof of the Odd Order Theorem In Sandrine Blazy and Christine Paulin and David Pichardie. ITP 2013, 4th Conference on Interactive Theorem Proving,2013, Rennes, France. Springer, 7998, pp. 163-179, LNCS

    Laurence Rideau, Bernard P. Serpette, and Xavier Leroy.
    Tilting at windmills with Coq: formal verification of a compilation algorithm for parallel moves. Journal of Automated Reasoning, 2008.Volume 40, number 4, p.307--326. (open archive version)

    All publications

    Yves Bertot, Laurence Rideau, Laurent Théry Distant decimals of π : Formal proofs of some algorithms computing them and guarantees of exact computation. Journal of Automated Reasoning, December 2017 (open archive version)

    Sophie Bernard, Yves Bertot, Laurence Rideau, Pierre-Yves Strub Formal Proofs of Transcendence for e and pi as an Application of Multivariate and Symmetric Polynomials Certified Programs and Proofs (CPP'16) (2016), ACM. (open archive version)

    Georges Gonthier & al.
    A Machine-Checked Proof of the Odd Order Theorem In Sandrine Blazy and Christine Paulin and David Pichardie. ITP 2013, 4th Conference on Interactive Theorem Proving,2013, Rennes, France. Springer, 7998, pp. 163-179, LNCS

    Erik Martin-Dorel, Micaela Mayero, Ioana Pasca, Laurence Rideau, and Laurent Théry.
    Certified, Efficient and Sharp Univariate Taylor Models in Coq. In Proceedings of SYNASC 2012 (International Symposium on Symbolic and Numeric Algorithms for Scientific Computing), 2013. To appear.

    Nicolas Brisebarre, Mioara Joldes, Erik Martin-Dorel, Micaela Mayero, Jean-Michel Muller, Ioana Pasca, Laurence Rideau, and Laurent Théry.
    Rigorous Polynomial Approximations using Taylor Models in Coq. In Proceedings of NFM 2012 (Nasa Formal Methods). Springer-Verlag LNCS, 2012. To appear.

    J. Heras, M. Poza, M. Dénès and L. Rideau
    in CICM'11. Lecture Notes in Computer Science, 6824, pages 30--44, 2011

    François Garillot, Georges Gonthier, Assia Mahboubi, Laurence Rideau
    `Packaging mathematical structures' Proceedings of TPHOLs'2009, LNCS, 2009. Rapport de Recherche .

    Laurence Rideau, Bernard P. Serpette, and Xavier Leroy.
    Tilting at windmills with Coq: formal verification of a compilation algorithm for parallel moves. Journal of Automated Reasoning, 2008. .Volume 40, number 4, p.307--326.

    Georges Gonthier, Assia Mahboubi, Laurence Rideau, Enrico Tassi, Laurent Théry
    `A Modular Formalisation of Finite Group Theory' Rapport de Recherche 6156.

    Laurence Rideau et Laurent Théry,
    `Formalising Sylow's theorems in Coq', Rapport Technique 327 .

    L.Rideau, B.P. Serpette
    Coq à la conquête des moulins, JFLA'2005, Obernai, France, 9-10 Mars 2005

    Ph. Audebaud, L.Rideau
    TeXmacs as Authoring Tool for Publication and Dissemination of Formal Developments, UITP'2003, Roma, Italy, 8 Sep 2003,also ENTCS volume 103, 2004

    H.Naciri, L.Rideau.
    Affichage et diffusion sur Internet d'explications en langue arabe de preuves mathématiques,
    CARI'2002 6ème Colloque Africain sur la Recherche en Informatique, Yaoundé, Cameroun,14-17 Oct, 2002

    H.Naciri, L.Rideau.
    Formal Mathematical Proof Explanations in Natural Language Using MathML: An Application to Proofs in Arabic,
    MathML International Conference 2002, Chicago,USA, June 28-30, 2002

    H.Naciri, L.Rideau.
    FIGUE: Mathematical Formula Layout with Interaction and MathML Support.,
    The Fifth Asian Symposium on Computer Mathematics ASCM'2001, Matsuyama, Japan, September 26-28, 2001.
    ASCM'2001 Page Web

    Marc Daumas, Laurence Rideau, and Laurent Théry,
    `` A Generic Library for Floating-Point Numbers and Its Application to exact Computing.'', Proceedings of TPHOLs'2001, LNCS 2152, 2001.

    H.Naciri, L.Rideau.
    The Mariage of MathML and Theorem Proving.
    IAMC'2001 Workshop,London Ontario, Canada, Juillet 2001.
    IAMC'2001 Proceedings

    Ahmed Amerkad, Yves Bertot, Laurence Rideau, and Loïc Pottier.
    Mathematics and proof presentation in Pcoq.
    PTP'01 Workshop, Siena, Italy, June 2001.

    H.Naciri, L.Rideau.
    Affichage et manipulation interactive de formules mathématiques dans les documents structurés.
    Rapport de recherche INRIA RR-4140, Janvier 2001 (accepté pour publication dans la revue ARIMA, Decembre 2002).

    Hanane Naciri and Laurence Rideau,
    ``Affichage interactif, bidimensionnel et incrémental de formules mathématiques.'',
    Proceedings of the 5th African Conference on Research in Computer Science, p. 473-480, CARI'2000, ANTANANARIVO (Madagascar), 16-19 october 2000.

    Olivier Pons, Yves bertot and Laurence Rideau,
    "Notions of dependency in proof assistants",
    In User Interfaces for Theorem Provers 1998, Eindhoven University of Technology.

    Laurence Rideau and Laurent Théry,
    ``Interactive Programming Environment for ML'',
    Research Report INRIA 3139, March 1997.

    P. Asar, (generic name for the Project ASAR, including L. Rideau),
    ``Framework and Multi-Formalism: The ASAR Project'',
    The Fourth International IFIP 10.5 Working Conference on Electronic Design Automation Frameworks, Gramado (Brazil), November 1994.

    A.-M. Déry and L. Rideau,
    ``Distributed programming environments: an example of a message protocol'',
    Inria Technical Report no. 165, August 1994.

    I. Jacobs and L. Rideau,
    ``A Centaur Tutorial'',
    Inria Technical Report no. 140, July 1992.

    T. Bouguerba, J. Benzakki, M. Israel and L. Rideau,
    "A front-end VHDL editor for synthesis tools",
    proceedings VUIF'95 San-Diego - April 1995.

    T. Bouguerba, J. Benzakki,M. Israel and L. Rideau,
    "VHDL subsets in the SDEV environment. A Case Study : The Synopsys Subset.",
    proceedings VUIF'95 Boston - pages 2.11-2.16 - October 1995

    P. Asar, (generic name for the Project ASAR, including L. Rideau),
    "Vers un Atelier d'accueil générique pour la Synthèse ARchitecturale bâti autour de CENTAUR : ASA"
    Symposium Architectures Nouvelles de Machines - Rennes - Décember 2-3, 1995.

    Some proofs

    Using the Plouffe formula to the decimals of Π in Coq

    A simple proof that Π is irrational using Coquelicot

    A proof that Π and e are transcendental using Coquelicot

    The puzzles of Le Monde in Coq.

    A Formal Proof of the theorem of Feit-Thompson (ended September 20, 2012).