Laurence RIDEAU

Cherchons comme cherchent ceux qui doivent trouver et trouvons comme trouvent ceux qui doivent chercher encore. (Augustin d'Hippone(354 - 430))

[English]

  • Organisation: INRIA
  • Unité de Recherche: Sophia Antipolis
  • Projet: MARELLE
  • Tel : +33 04 92 38 78 04
  • Fax : +33 04 92 38 76 33
  • E-mail: (mon Prénom).(mon Nom)@inria.fr

    •  

     
     
     

    Thèmes de recherche

    Toutes mes activités de recherche sont axées autour du système Coq et sont effectuées en collaboration avec les membres du projet Marelle et de l'équipe Mathematical Components du centre de recherche commun Microsoft Research/Inria.

    Activités d'intérêt général

    Chargée du Développement et des Relations Industrielles (CDRI) à l'Unité de Recherche de Sophia-Antipolis de 1995 à février 2000.

    Publications

    Publications caractéristiques

    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)

    Toutes les publications

    V. Lefèvre, N. Louvet, J.-M. Muller, J. Picot and L. Rideau Accurate calculation of Euclidean Norms using Double-word arithmetic to appear in ACM Transactions on Mathematical Software.

    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)

    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.(open archive version)

    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.(open archive version)

    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. (open archive version)

    Georges Gonthier, Assia Mahboubi, Laurence Rideau, Enrico Tassi, Laurent Théry
    `A Modular Formalisation of Finite Group Theory' Proceedings of TPHOLs'2007, LNCS 4732, 2007. 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, aussi 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, Décembre 2002)

    Hanane Naciri et Laurence Rideau,
    ``Affichage interactif, bidimensionnel et incrémental de formules mathématiques.'',
    Actes du 5ème Colloque Africain sur la Recherche en Informatique, p. 473-481, CARI'2000, ANTANANARIVO (Madagascar), 16-19 octobre 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'',
    Rapport de Recherche INRIA 3139, Mars 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 VIUF'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 VIUF'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 : ASAR"
    Symposium Architectures Nouvelles de Machines - Rennes - Décember 2-3, 1995.

    Quelques preuves

    Les décimales de Π en Coq en utilisant la formule de Plouffe

    Une preuve simple que Π est irrationnel en utilisant Coquelicot

    Une preuve que Π et e sont transcendants avec Coquelicot

    Les énigmes du Monde en Coq.

    Une Preuve Formelle du théorème de Feit-Thompson (terminé le 20 Septembre 2012).

    JFLA: Les Journées Francophones des Langages Applicatifs.