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. 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

  • 6G. Barthe, B. Grégoire, S. Heraud, F. Olmedo, S. Zanella Beguelin.

    Verified indifferentiable hashing into elliptic curves, in: Journal of Computer Security, November 2013.

    http://hal.inria.fr/hal-00935747
  • 7É. Martin-Dorel, G. Melquiond, J.-M. Muller.

    Some issues related to double roundings, in: BIT Numerical Mathematics, December 2013, vol. 53, no 4, pp. 897-924. [ DOI : 10.1007/s10543-013-0436-2 ]

    http://hal.inria.fr/ensl-00644408
  • 8J. Zsidó.

    Theorem of three circles in Coq, in: Journal of Automated Reasoning, December 2013, 25 p. [ DOI : 10.1007/s10817-013-9299-0 ]

    http://hal.inria.fr/hal-00864827

International Conferences with Proceedings

  • 9G. Barthe, J. M. Crespo, B. Gregoire, C. Kunz, Y. Lakhnech, B. Schmidt, S. Zanella Beguelin.

    Fully automated analysis of padding-based encryption in the computational model, in: 2013 ACM SIGSAC Conference on Computer and Communications Security, Berlin, Germany, ACM, November 2013, pp. 1247-1260. [ DOI : 10.1145/2508859.2516663 ]

    http://hal.inria.fr/hal-00935737
  • 10G. Barthe, G. Danezis, B. Grégoire, C. Kunz, S. Zanella Beguelin.

    Verified Computational Differential Privacy with Applications to Smart Metering, in: 2013 IEEE 26th Computer Security Foundations Symposium, New Orleans, United States, IEEE Computer Society, June 2013, pp. 287-301. [ DOI : 10.1109/CSF.2013.26 ]

    http://hal.inria.fr/hal-00935736
  • 11G. Barthe, C. Fournet, B. Gregoire, 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.

    http://hal.inria.fr/hal-00935743
  • 12G. Cano, M. Dénès.

    Matrices à blocs et en forme canonique, in: JFLA - Journées francophones des langages applicatifs, Aussois, France, D. Pous, C. Tasson (editors), Damien Pous and Christine Tasson, February 2013.

    http://hal.inria.fr/hal-00779376
  • 13G. 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
  • 14É. Martin-Dorel, M. Mayero, I. Pasca, L. Rideau, L. Théry.

    Certified, Efficient and Sharp Univariate Taylor Models in COQ, in: SYNASC 2013 - 15th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, Timisoara, Romania, 2013.

    http://hal.inria.fr/hal-00845791
  • 15Q. Wang, B. Barras.

    Semantics of Intensional Type Theory extended with Decidable Equational Theories, in: Computer Science Logic 2013, Dagstuhl, Germany, S. R. D. Rocca (editor), Leibniz International Proceedings in Informatics (LIPIcs), Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik, August 2013, vol. 23, pp. 653–667. [ DOI : 10.4230/LIPIcs.CSL.2013.653 ]

    http://hal.inria.fr/hal-00937197

Scientific Books (or Scientific Book chapters)

  • 16P. Aczel, B. Ahrens, T. Altenkirch, S. Awodey, B. Barras, A. Bauer, Y. Bertot, M. Bezem, T. Coquand, E. Finster, D. Grayson, H. Herbelin, A. Joyal, D. Licata, P. Lumsdaine, A. Mahboubi, P. Martin-Löf, S. Melikhov, A. Pelayo, A. Polonsky, M. Shulman, M. Sozeau, B. Spitters, B. Van Den Berg, V. Voevodsky, M. Warren, C. Angiuli, A. Bordg, G. Brunerie, C. Kapulkin, E. Rijke, K. Sojakova, J. Avigad, C. Cohen, R. Constable, P.-L. Curien, P. Dybjer, M. Escardó, K.-B. Hou, N. Gambino, R. Garner, G. Gonthier, T. Hales, R. Harper, M. Hofmann, P. Hofstra, J. Koch, N. Kraus, N. Li, Z. Luo, M. Nahas, E. Palmgren, E. Riehl, D. Scott, P. Scott, S. Soloviev.

    Homotopy Type Theory: Univalent Foundations of Mathematics, Aucun, 2013, 448 p.

    http://hal.inria.fr/hal-00935057

Internal Reports

Other Publications

  • 20É. Martin-Dorel, G. Hanrot, M. Mayero, L. Théry.

    Formally verified certificate checkers for hardest-to-round computation, December 2013.

    http://hal.inria.fr/hal-00919498


previous Previous | up Home