EN FR
EN FR




Bibliography

Major publications by the team in recent years
  • 1G. Barthe, B. Grégoire, S. Zanella Béguelin.

    Formal Certification of Code-Based Cryptographic Proofs, in: 36th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2009, ACM, 2009, p. 90–101.

    http://dx.doi.org/10.1145/1480881.1480894
  • 2Y. Bertot, P. Castéran.

    Interactive Theorem Proving and Program Development, Coq'Art:the Calculus of Inductive Constructions, Springer-Verlag, 2004.
  • 3Y. Bertot, G. Gonthier, S. O. Biha, I. Paşca.

    Canonical Big Operators, in: Proceedings of the 21st International Conference on Theorem Proving in Higher Order Logics (TPHOLs 2008), Lecture Notes in Computer Science, Springer, August 2008, vol. 5170, p. 12–16.

    http://hal.inria.fr/inria-00331193/
  • 4G. Gonthier, A. Mahboubi, L. Rideau, E. Tassi, L. Théry.

    A Modular Formalisation of Finite Group Theory, in: Proceedings of the 20th International Conference on Theorem Proving in Higher Order Logics (TPHOLs 2007), K. Schneider, J. Brandt (editors), LNCS, Springer-Verlag, September 2007, vol. 4732, p. 86-101.

    http://hal.inria.fr/inria-00139131
Publications of the year

Doctoral Dissertations and Habilitation Theses

  • 5T. M. Pham.

    Description formelle de propriétés géométriques, Université de Nice Sophia Antipolis, September 2011.
  • 6J. Sacchini.

    Terminaison basée sur les types et filtrage dépendant pour le calcul des constructions inductives, École Nationale Supérieure des Mines de Paris, June 2011.

    http://hal.inria.fr/pastel-00622429/en

Articles in International Peer-Reviewed Journal

  • 7Y. Bertot, F. Guilhot, A. Mahboubi.

    A formal study of Bernstein coefficients and polynomials, in: Mathematical Structures in Computer Science, 2011, vol. 21, no 04, p. 731-761.

    http://hal.inria.fr/inria-00503017/en
  • 8J. O. Blech, B. Grégoire.

    Certifying compilers using higher-order theorem provers as certificate checkers, in: Formal Methods in System Design, 2011, vol. 38, no 1, p. 33-61.

International Conferences with Proceedings

  • 9M. Armand, G. Faure, B. Grégoire, C. Keller, L. Théry, B. Werner.

    A Modular Integration of SAT/SMT Solvers to Coq through Proof Witnesses, in: First International Conference on Certified Programs and Proofs, Tawain, Lecture Notes in Computer Science, Springer, December 7-9 2011, To Appear.
  • 10M. Armand, G. Faure, B. Grégoire, C. Keller, L. Théry, B. Werner.

    Verifying SAT and SMT in Coq for a fully automated decision procedure, in: PSATTT'11: International Workshop on Proof-Search in Axiomatic Theories and Type Theories, Wroclaw, Poland, Germain Faure, Stéphane Lengrand, Assia Mahboubi, 2011.

    http://hal.inria.fr/inria-00614041/en
  • 12G. Barthe, B. Grégoire, Y. Lakhnech, S. Zanella Béguelin.

    Beyond Provable Security Verifiable IND-CCA Security of OAEP, in: Topics in Cryptology - CT-RSA 2011 - The Cryptographers' Track at the RSA Conference 2011, San Francisco, CA, USA, Springer, February 14-18 2011, vol. 6558, p. 180-196.
  • 13F. Besson, P. Fontaine, L. Théry.

    A Flexible Proof Format for SMT: a Proposal, in: PxTP 2011: First InternationalWorkshop on Proof eXchange for Theorem Proving, Wroclaw, Poland, 2011.

    http://pxtp2011.loria.fr/PxTP2011.pdf
  • 14M. Boespflug, M. Dénès, B. Grégoire.

    Full reduction at full throttle, in: First International Conference on Certified Programs and Proofs, Tawain, Lecture Notes in Computer Science, Springer, December 7-9 2011, To Appear.
  • 15L. Fuchs, L. Théry.

    A Formalization of Grassmann-Cayley Algebra in COQ and Its Application to Theorem Proving in Projective Geometry, in: Automated Deduction in Geometry, Lecture Notes in Computer Science, 2011, vol. 6877, p. 51-67.
  • 16B. Grégoire, L. Pottier, L. Théry.

    Proof Certificates for Algebra and Their Application to Automatic Geometry Theorem Proving, in: Automated Deduction in Geometry - 7th International Workshop, ADG 2008, Shanghai, China, Lecture Notes in Computer Science, Springer, September 22-24 2011, vol. 6301, p. 42-59, Revised Papers.
  • 17J. Heras, M. Poza, M. Dénès, L. Rideau.

    Incidence simplicial matrices formalized in Coq/SSReflect, in: Conference on Intelligent Computer Mathematics'11, Lecture Notes in Artificial Intelligence, Springer-Verlag, August 2011, vol. 6824.

    http://hal.inria.fr/inria-00603208/en
  • 18S. Heraud, D. Nowak.

    A Formalization of Polytime Functions, in: Interactive Theorem Proving - Second International Conference, ITP 2011, Berg en Dal, The Netherlands, M. C. J. D. van Eekelen, H. Geuvers, J. Schmaltz, F. Wiedijk (editors), Lecture Notes in Computer Science, August 22-25 2011, vol. 6898, p. 119-134.
  • 19T. M. Pham, Y. Bertot, J. Narboux.

    A Coq-based Library for Interactive and Automated Theorem Proving in Plane Geometry, in: The 11th International Conference on Computational Science and Its Applications (ICCSA 2011), Santander, Spain, Lecture Notes in Computer Science, Springer-Verlag, 2011, vol. 6785, p. 368-383. [ DOI : 10.1007/978-3-642-21898-9_32 ]

    http://hal.inria.fr/inria-00584918/en

Internal Reports