EN FR
EN FR


previous Previous | up Home


Bibliography

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

    Computer-Aided Security Proofs for the Working Cryptographer, in: Advances in Cryptology - CRYPTO 2011 - 31st Annual Cryptology Conference, Santa Barbara, CA, USA, August 14-18, 2011. Proceedings, Lecture Notes in Computer Science, Springer, 2011, vol. 6841, pp. 71-90, Best Paper Award.
  • 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, pp. 12–16.

    http://hal.inria.fr/inria-00331193/
  • 4G. Gonthier, A. Asperti, J. Avigad, Y. Bertot, C. Cohen, F. Garillot, S. Le Roux, A. Mahboubi, R. O'Connor, S. Ould Biha, I. Pasca, L. Rideau, A. Solovyev, E. Tassi, L. Théry.

    A Machine-Checked Proof of the Odd Order Theorem, in: ITP 2013, 4th Conference on Interactive Theorem Proving, Rennes, France, S. Blazy, C. Paulin, D. Pichardie (editors), LNCS, Springer, 2013, vol. 7998, pp. 163-179. [ DOI : 10.1007/978-3-642-39634-2_14 ]

    http://hal.inria.fr/hal-00816699
  • 5G. 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, pp. 86-101.

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

Doctoral Dissertations and Habilitation Theses

Articles in International Peer-Reviewed Journals

  • 7Y. Bertot, G. Allais.

    Views of Pi: definition and computation, in: Journal of Formalized Reasoning, October 2014, vol. 7, no 1, pp. 105-129. [ DOI : 10.6092/issn.1972-5787/4343 ]

    https://hal.inria.fr/hal-01074926
  • 8L. Fuchs, L. Théry.

    Implementing Geometric Algebra Products with Binary Trees, in: Advances in Applied Clifford Algebras, February 2014, vol. 24, no 1, 22 p.

    https://hal.inria.fr/hal-01095495
  • 9É. Martin-Dorel, G. Hanrot, M. Mayero, L. Théry.

    Formally verified certificate checkers for hardest-to-round computation, in: Journal of Automated Reasoning, 2015, vol. 54, no 1, pp. 1-29. [ DOI : 10.1007/s10817-014-9312-2 ]

    https://hal.inria.fr/hal-00919498
  • 10L. Théry, F. Wiedijk.

    Foreword to the Special Focus on Formal Proofs for Mathematics and Computer Science, in: International Journal of Mathematics and Computer Science, October 2014, pp. 1-3. [ DOI : 10.1007/s11786-014-0214-9 ]

    https://hal.archives-ouvertes.fr/hal-01095761

Invited Conferences

  • 11Y. Bertot.

    Links between homotopy theory and type theory, in: CICM - Conference on Intelligent Computer Mathematics, Coimbra, Portugal, S. Watt, J. Davenport, A. Sexton, P. Sojka, J. Urban (editors), Springer, July 2014.

    https://hal.inria.fr/hal-00987248

International Conferences with Proceedings

  • 12J. A. Akinyele, G. Barthe, B. Grégoire, B. Schmidt, P.-Y. Strub.

    Certified Synthesis of Efficient Batch Verifiers, in: IEEE 27th Computer Security Foundations Symposium, CSF, Vienna, Austria, 2014. [ DOI : 10.1109/CSF.2014.19 ]

    https://hal.inria.fr/hal-01094565
  • 13G. Barthe, F. Dupressoir, P.-A. Fouque, B. Grégoire, J.-C. Zapalowicz.

    Synthesis of Fault Attacks on Cryptographic Implementations, in: Conference on Computer and Communications Security, Scottsdale, United States, Proceedings of the 2014 ACM SIGSAC Conference on Computer and Communications Security, ACM, 2014. [ DOI : 10.1145/2660267.2660304 ]

    https://hal.inria.fr/hal-01094549
  • 14G. Barthe, F. Dupressoir, P.-A. Fouque, M. Tibouchi, J.-C. Zapalowicz, B. Grégoire.

    Making RSA–PSS Provably Secure against Non-random Faults, in: Cryptographic Hardware and Embedded Systems - CHES 2014, Busan, South Korea, CHES 2014, Springer, September 2014, vol. LNCS 8731, pp. 206 - 222. [ DOI : 10.1007/978-3-662-44709-3_12 ]

    https://hal.inria.fr/hal-01094057
  • 15G. Barthe, C. Fournet, B. Grégoire, P.-Y. Strub, N. Swamy, S. Zanella Beguelin.

    Probabilistic relational verification for cryptographic implementations, in: The 41st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, San Diego, United States, January 2014.

    https://hal.inria.fr/hal-00935743
  • 16Y. Bertot.

    Fixed Precision Patterns for the Formal Verification of Mathematical Constant Approximations, in: Certified Programs and Proofs (CPP'15), Mumbai, India, ACM, January 2015. [ DOI : 10.1145/2676724.2693172 ]

    https://hal.inria.fr/hal-01074927

Internal Reports

  • 17J. Grimm.

    Fibonacci numbers and the Stern-Brocot tree in Coq, Inria Sophia Antipolis, December 2014, no RR-8654, 76 p.

    https://hal.inria.fr/hal-01093589
  • 18J. Grimm.

    Implementation of Bourbaki's Elements of Mathematics in Coq: Part Two; Ordered Sets, Cardinals, Integers, Inria Sophia Antipolis, 2015, no RR-7150, 685 p.

    https://hal.inria.fr/inria-00440786

Other Publications



previous Previous | up Home