Publications

Publications HAL du labo/EPI marelle

2017

Journal articles

titre
Coqoon
auteur
Alexander Faithfull, Jesper Bengtson, Enrico Tassi, Carst Tankink
article
International Journal on Software Tools for Technology Transfer, Springer Verlag, 2017
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01410450/file/main-sttt.pdf BibTex
titre
Distant decimals of π
auteur
Yves Bertot, Laurence Rideau, Laurent Théry
article
Journal of Automated Reasoning, Springer Verlag, 2017
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01582524/file/main.pdf BibTex

Conference papers

titre
A Formal Proof in Coq of LaSalle’s Invariance Principle
auteur
Cyril Cohen, Damien Rouhling
article
Interactive Theorem Proving, Sep 2017, Brasilia, Brazil. 〈10.1007/978-3-319-66107-0_10〉
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01612293/file/main.pdf BibTex
titre
Proving uniformity and independence by self-composition and coupling
auteur
Gilles Barthe, Thomas Espitau, Benjamin Grégoire, Justin Hsu, Pierre-Yves Strub
article
LPAR 2017 – International Conferences on Logic for Programming, Artificial Intelligence and Reasoning, May 2017, Maun, Botswana. pp.19
Accès au texte intégral et bibtex
http://hal.upmc.fr/hal-01541198/file/1701.06477.pdf BibTex
titre
Formal Foundations of 3D Geometry to Model Robot Manipulators
auteur
Reynald Affeldt, Cyril Cohen
article
Conference on Certified Programs and Proofs 2017, Jan 2017, Paris, France
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01414753/file/robot_cpp_final.pdf BibTex
titre
A refinement-based approach to large scale reflection for algebra
auteur
Cyril Cohen, Damien Rouhling
article
JFLA 2017 – Vingt-huitième Journées Francophones des Langages Applicatifs, Jan 2017, Gourette, France
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01414881/file/cyrilcohen.pdf BibTex

Preprints, Working Papers, …

titre
A Formal Proof in Coq of a Control Function for the Inverted Pendulum
auteur
Damien Rouhling
article
2017
Accès au bibtex
BibTex
titre
Elpi: an extension language for Coq Metaprogramming Coq in the Elpi λProlog dialect
auteur
Enrico Tassi
article
2017
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01637063/file/coqpl2018.pdf BibTex
titre
Implementing Type Theory in Higher Order Constraint Logic Programming
auteur
Ferruccio Guidi, Claudio Sacerdoti Coen, Enrico Tassi
article
2017
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01410567/file/dalefest.pdf BibTex
titre
Formal correctness of comparison algorithms between binary64 and decimal64 floating-point numbers
auteur
Arthur Blot, Jean-Michel Muller, Laurent Théry
article
2017
Accès au texte intégral et bibtex
https://hal.archives-ouvertes.fr/hal-01512294/file/paper.pdf BibTex
titre
A Formalisation of the Generalised Towers of Hanoi
auteur
Laurent Théry
article
2017
Accès au texte intégral et bibtex
https://hal.archives-ouvertes.fr/hal-01446070/file/Note.pdf BibTex

2016

Journal articles

titre
Formalized Linear Algebra over Elementary Divisor Rings in Coq
auteur
Guillaume Cano, Cyril Cohen, Maxime Dénès, Anders Mörtberg, Vincent Siles
article
Logical Methods in Computer Science, Logical Methods in Computer Science Association, 2016, 〈10.2168/LMCS-12(2:7)2016〉
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01081908/file/main.author.pdf BibTex
titre
Implementation of Bourbaki’s Elements of Mathematics in Coq: Part Two, From Natural Numbers to Real Numbers
auteur
José Grimm
article
Journal of Formalized Reasoning, ASDD-AlmaDL, 2016, 9 (2), pp.52. 〈https://jfr.unibo.it/article/view/4771〉. 〈10.6092/issn.1972-5787/4771〉
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01415375/file/jfra2-v2.pdf BibTex

Conference papers

titre
Strong Non-Interference and Type-Directed Higher-Order Masking
auteur
Gilles Barthe, Sonia Belaïd, François Dupressoir, Pierre-Alain Fouque, Benjamin Grégoire, Pierre-Yves Strub, Rébecca Zucchini
article
23rd ACM Conference on Computer and Communications Security , Oct 2016, Vienne, Austria. pp.116 – 129, 2016, 〈10.1145/2976749.2978427〉
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01410216/file/main.pdf BibTex
titre
Advanced Probabilistic Couplings for Differential Privacy
auteur
Gilles Barthe, Noémie Fong, Marco Gaboardi, Benjamin Grégoire, Justin Hsu, Pierre-Yves Strub
article
23rd ACM Conference on Computer and Communications Security , Oct 2016, Vienne, Austria. pp.55 – 67, 2016, 〈10.1145/2976749.2978391〉
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01410196/file/main.pdf BibTex
titre
Boolean reflection via type classes
auteur
Benjamin Grégoire, Enrico Tassi
article
Coq Workshop, Aug 2016, Nancy, France. 2016
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01410530/file/autoview.pdf BibTex
titre
A program logic for union bounds
auteur
Gilles Barthe, Marco Gaboardi, Benjamin Grégoire, Justin Hsu, Pierre-Yves Strub
article
The 43rd International Colloquium on Automata, Languages and Programming , Jul 2016, Rome, Italy. 〈10.4230/LIPIcs.ICALP.2016.107〉
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01411095/file/icalp16-212.pdf BibTex
titre
Proving Differential Privacy via Probabilistic Couplings
auteur
Gilles Barthe, Marco Gaboardi, Benjamin Grégoire, Justin Hsu, Pierre-Yves Strub
article
Thirty-First Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), Jul 2016, New York, United States. pp.749 – 758, 2016, 〈10.1145/2933575.2934554〉
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01411097/file/main.pdf BibTex
titre
Implementing HOL in an Higher Order Logic Programming Language
auteur
Cvetan Dunchev, Claudio Sacerdoti Coen, Enrico Tassi
article
Logical Frameworks and Meta Languages: Theory and Practice, Jun 2016, Porto, Portugal. ACM, pp.10, 2016, LFMTP ’16. 〈10.1145/2966268.2966272〉
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01394686/file/holsuperlight.pdf BibTex
titre
Coqoon An IDE for interactive proof development in Coq
auteur
Alexander Faithfull, Jesper Bengtson, Enrico Tassi, Carst Tankink
article
TACAS, Apr 2016, Eindhoven, Netherlands. LNCS
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01242295/file/main.pdf BibTex
titre
Formal Proofs of Transcendence for e and π as an Application of Multivariate and Symmetric Polynomials
auteur
Sophie Bernard, Yves Bertot, Laurence Rideau, Pierre-Yves Strub
article
Jeremy Avigad and Adam Chlipala. Certified Programs and Proofs, Jan 2016, St Petersburg, Florida, United States. ACM Press, pp.12, 2016
Accès au bibtex
https://arxiv.org/pdf/1512.02791 BibTex
titre
Formalization of a Newton Series Representation of Polynomials
auteur
Cyril Cohen, Boris Djalal
article
Jeremy Avigad and Adam Chlipala. Certified Programs and Proofs, Jan 2016, St Petersburg, Florida, United States. Certified Programs and Proofs, 2016
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01240469/file/main.pdf BibTex

Lectures

titre
Coq in a Hurry
auteur
Yves Bertot
article
3rd cycle. Types Summer School, also used at the University of Goteborg, Nice,
Ecole Jeunes Chercheurs en Programmation,
Universite de Nice, France. 2016, pp.49
Accès au texte intégral et bibtex
https://cel.archives-ouvertes.fr/inria-00001173/file/coq-hurry.pdf BibTex

Reports

titre
Implementation of Bourbaki’s Elements of Mathematics in Coq: Part Three Structures
auteur
José Grimm
article
[Research Report] RR-8997, Inria Sophia Antipolis. 2016, pp.115
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01412037/file/RR-8997.pdf BibTex
titre
Implementation of Bourbaki’s Elements of Mathematics in Coq: Part Two; Ordered Sets, Cardinals, Integers
auteur
José Grimm
article
[Research Report] RR-7150, Inria Sophia Antipolis; INRIA. 2016, pp.730
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00440786/file/RR-7150-v8.pdf BibTex
titre
A Small Scale Reflection Extension for the Coq system
auteur
Georges Gonthier, Assia Mahboubi, Enrico Tassi
article
[Research Report] RR-6455, Inria Saclay Ile de France. 2016
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00258384/file/main.pdf BibTex

Preprints, Working Papers, …

titre
Parallel Implementations of Masking Schemes and the Bounded Moment Leakage Model
auteur
Gilles Barthe, François Dupressoir, Sebastian Faust, Benjamin Grégoire, François-Xavier Standaert, Pierre-Yves Strub
article
2016
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01414009/file/parallel_masking_4.pdf BibTex
titre
From signatures to monads in UniMath
auteur
Benedikt Ahrens, Ralph Matthes, Anders Mörtberg
article
2016
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01410487/file/main.pdf BibTex
titre
Cubical Type Theory: a constructive interpretation of the univalence axiom
auteur
Cyril Cohen, Thierry Coquand, Simon Huber, Anders Mörtberg
article
Accepted for publication in LIPIcs. 2016
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01378906/file/cubicaltt.pdf BibTex

2015

Journal articles

titre
Formally verified certificate checkers for hardest-to-round computation
auteur
Érik Martin-Dorel, Guillaume Hanrot, Micaela Mayero, Laurent Théry
article
Journal of Automated Reasoning, Springer Verlag, 2015, 54 (1), pp.1-29. 〈10.1007/s10817-014-9312-2〉
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00919498/file/Hensel-JAR.pdf BibTex

Conference papers

titre
ELPI: fast, Embeddable, λProlog Interpreter
auteur
Cvetan Dunchev, Ferruccio Guidi, Claudio Sacerdoti Coen, Enrico Tassi
article
Proceedings of LPAR, Nov 2015, Suva, Fiji. LNCS
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01176856/file/lpar2015.pdf BibTex
titre
Automated Proofs of Pairing-Based Cryptography
auteur
Gilles Barthe, Benjamin Grégoire, Benedikt Schmidt
article
Proceedings of the 22nd Conference on Computer and Communications Security, Oct 2015, Denver, United States. 2015, 〈10.1145/2810103.2813697〉
Accès au bibtex
BibTex
titre
Asynchronous processing of Coq documents: from the kernel up to the user interface
auteur
Bruno Barras, Carst Tankink, Enrico Tassi
article
Proceedings of ITP, Aug 2015, Nanjing, China
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01135919/file/full.pdf BibTex
titre
Verified Proofs of Higher-Order Masking
auteur
Gilles Barthe, Sonia Belaïd, François Dupressoir, Pierre-Alain Fouque, Benjamin Grégoire, Pierre-Yves Strub
article
Eurocrypt 2015, Apr 2015, Sofia, Bulgaria. Advances in Cryptology — EUROCRYPT 2015, series Lecture Notes in Computer Science (9056), 2015, Advances in Cryptology — EUROCRYPT 2015. 〈10.1007/978-3-662-46800-5_18〉
Accès au bibtex
BibTex
titre
Fixed Precision Patterns for the Formal Verification of Mathematical Constant Approximations
auteur
Yves Bertot
article
Certified Programs and Proofs (CPP’15), Jan 2015, Mumbai, India. ACM, 2015, 〈10.1145/2676724.2693172〉
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01074927/file/main%20%281%29.pdf BibTex
titre
Relational Reasoning via Probabilistic Coupling
auteur
Gilles Barthe, Thomas Espitau, Benjamin Grégoire, Justin Hsu, Léo Stefanesco, Pierre-Yves Strub
article
LPAR, 2015, Suva, France. pp.387 – 401, 2015, 〈10.1007/978-3-662-48899-7_27〉
Accès au texte intégral et bibtex
https://hal.archives-ouvertes.fr/hal-01246719/file/Couplings.pdf BibTex

Lectures

titre
Semantics for programming languages with Coq encodings
auteur
Yves Bertot
article
Master. France. 2015
Accès au texte intégral et bibtex
https://hal.inria.fr/cel-01130272/file/semantics1.pdf BibTex

Preprints, Working Papers, …

titre
Formally-Proven Kosaraju’s algorithm
auteur
Laurent Théry
article
2015
Accès au texte intégral et bibtex
https://hal.archives-ouvertes.fr/hal-01095533/file/Note.pdf BibTex

2014

Journal articles

titre
Views of Pi: definition and computation
auteur
Yves Bertot, Guillaume Allais
article
Journal of Formalized Reasoning, ASDD-AlmaDL, 2014, 7 (1), pp.105-129. 〈10.6092/issn.1972-5787/4343〉
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01074926/file/main.pdf BibTex
titre
Foreword to the Special Focus on Formal Proofs for Mathematics and Computer Science
auteur
Laurent Théry, Freek Wiedijk
article
International Journal of Mathematics and Computer Science, 2014, pp.1-3. 〈10.1007/s11786-014-0214-9〉
Accès au bibtex
BibTex
titre
Implementing Geometric Algebra Products with Binary Trees
auteur
Laurent Fuchs, Laurent Théry
article
Advances in Applied Clifford Algebras, Springer Verlag, 2014, 24 (1), pp.22. 〈http://link.springer.com/article/10.1007%2Fs00006-014-0447-3〉
Accès au bibtex
BibTex

Conference papers

titre
Synthesis of Fault Attacks on Cryptographic Implementations
auteur
Gilles Barthe, François Dupressoir, Pierre-Alain Fouque, Benjamin Grégoire, Jean-Christophe Zapalowicz
article
ACM CCS 2014, Nov 2014, Scottsdale, United States. ACM, pp.16, 2014, ACM SIGSAC Conference on Computer and Communications Security. 〈http://www.sigsac.org/ccs/CCS2014/〉. 〈10.1145/2660267.2660304〉
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01094034/file/paper.pdf BibTex
titre
Making RSA–PSS Provably Secure against Non-random Faults
auteur
Gilles Barthe, François Dupressoir, Pierre-Alain Fouque, Mehdi Tibouchi, Jean-Christophe Zapalowicz, Benjamin Grégoire
article
Cryptographic Hardware and Embedded Systems – 2014, Sep 2014, Busan, South Korea. Springer, LNCS 8731, pp.206 – 222, 2014, CHES 2014. 〈http://www.chesworkshop.org/ches2014/start.php〉. 〈10.1007/978-3-662-44709-3_12〉
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01094057/file/FaultRSA.pdf BibTex
titre
Certified Synthesis of Efficient Batch Verifiers
auteur
Joseph A. Akinyele, Gilles Barthe, Benjamin Grégoire, Benedikt Schmidt, Pierre-Yves Strub
article
CSF 2014 – IEEE 27th Computer Security Foundations Symposium, Jul 2014, Vienna, Austria. pp.153 – 165, 2014, 27th Computer Security Foundations Symposium, 2014. 〈10.1109/CSF.2014.19〉
Accès au bibtex
BibTex
titre
Links between homotopy theory and type theory
auteur
Yves Bertot
article
Stephen Watt; James Davenport; Alan Sexton; Petr Sojka; Josef Urban. CICM – Conference on Intelligent Computer Mathematics, Jul 2014, Coimbra, Portugal. Springer, 2014
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00987248/file/paper.pdf BibTex
titre
Probabilistic relational verification for cryptographic implementations
auteur
Gilles Barthe, Cédric Fournet, Benjamin Grégoire, Pierre-Yves Strub, Nikhil Swamy, Santiago Zanella-Béguelin
article
The 41st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Jan 2014, San Diego, United States. 2014
Accès au bibtex
BibTex

Reports

titre
Fibonacci numbers and the Stern-Brocot tree in Coq
auteur
José Grimm
article
[Research Report] RR-8654, Inria Sophia Antipolis; INRIA. 2014, pp.76
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01093589/file/RR8654-v2.pdf BibTex
titre
Coq 8.4 Reference Manual
auteur
Pierre Boutillier, Stephane Glondu, Benjamin Grégoire, Hugo Herbelin, Pierre Letouzey, Pierre-Marie Pédrot, Yann Régis-Gianas, Matthieu Sozeau, Arnaud Spiwack, Enrico Tassi
article
[Research Report] Inria. 2014
Accès au bibtex
BibTex

Theses

titre
Interaction entre algèbre linéaire et analyse en formalisation des mathématiques
auteur
Guillaume Cano
article
Autre [cs.OH]. Université Nice Sophia Antipolis, 2014. Français. 〈NNT : 2014NICE4016〉
Accès au texte intégral et bibtex
https://tel.archives-ouvertes.fr/tel-00986283/file/2014NICE4016.pdf BibTex

Preprints, Working Papers, …

titre
A Formally-Proven Algorithm for 2-Sat Problems
auteur
Laurent Théry
article
2014
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01095538/file/TwoSat.pdf BibTex

2013

Journal articles

titre
Theorem of three circles in Coq
auteur
Julianna Zsidó
article
Journal of Automated Reasoning, Springer Verlag, 2013, 〈10.1007/s10817-013-9299-0〉
Accès au bibtex
https://arxiv.org/pdf/1306.0783 BibTex
titre
Some issues related to double roundings
auteur
Érik Martin-Dorel, Guillaume Melquiond, Jean-Michel Muller
article
BIT Numerical Mathematics, Springer Verlag, 2013, 53 (4), pp.897-924. 〈10.1007/s10543-013-0436-2〉
Accès au texte intégral et bibtex
https://hal-ens-lyon.archives-ouvertes.fr/ensl-00644408/file/Version_Finale_DoubleRoundings.pdf BibTex
titre
Verified indifferentiable hashing into elliptic curves
auteur
Gilles Barthe, Benjamin Grégoire, Sylvain Heraud, Federico Olmedo, Santiago Zanella-Béguelin
article
Journal of Computer Security, IOS Press, 2013
Accès au bibtex
BibTex

Conference papers

titre
Refinements for Free!
auteur
Cyril Cohen, Maxime Dénès, Anders Mörtberg
article
Certified Programs and Proofs, Dec 2013, Melbourne, Australia. pp.147 – 162, 2013, 〈10.1007/978-3-319-03545-1_10〉
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01113453/file/refinements.pdf BibTex
titre
Fully automated analysis of padding-based encryption in the computational model
auteur
Gilles Barthe, Juan Manuel Crespo, Benjamin Grégoire, César Kunz, Yassine Lakhnech, Benedikt Schmidt, Santiago Zanella-Béguelin
article
2013 ACM SIGSAC Conference on Computer and Communications Security, Nov 2013, Berlin, Germany. ACM, pp.1247-1260, 2013, Proceedings of the 2013 ACM SIGSAC conference on Computer & communications security. 〈10.1145/2508859.2516663〉
Accès au bibtex
BibTex
titre
Certified, Efficient and Sharp Univariate Taylor Models in COQ
auteur
Érik Martin-Dorel, Micaela Mayero, Ioana Pasca, Laurence Rideau, Laurent Théry
article
SYNASC 2013 – 15th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, Sep 2013, Timisoara, Romania. 2013
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00845791/file/CoqApprox2013_HAL_v2.pdf BibTex
titre
Semantics of Intensional Type Theory extended with Decidable Equational Theories
auteur
Qian Wang, Bruno Barras
article
Simona Ronchi Della Rocca. Computer Science Logic 2013, Aug 2013, Dagstuhl, Germany. Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik, 23, pp.653–667, 2013, Leibniz International Proceedings in Informatics (LIPIcs). 〈10.4230/LIPIcs.CSL.2013.653〉
Accès au bibtex
BibTex
titre
A Machine-Checked Proof of the Odd Order Theorem
auteur
Georges Gonthier, Andrea Asperti, Jeremy Avigad, Yves Bertot, Cyril Cohen, François Garillot, Stéphane Le Roux, Assia Mahboubi, Russell O’Connor, Sidi Ould Biha, Ioana Pasca, Laurence Rideau, Alexey Solovyev, Enrico Tassi, Laurent Théry
article
Sandrine Blazy and Christine Paulin and David Pichardie. ITP 2013, 4th Conference on Interactive Theorem Proving, Jul 2013, Rennes, France. Springer, 7998, pp.163-179, 2013, LNCS. 〈10.1007/978-3-642-39634-2_14〉
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00816699/file/main.pdf BibTex
titre
Verified Computational Differential Privacy with Applications to Smart Metering
auteur
Gilles Barthe, George Danezis, Benjamin Grégoire, César Kunz, Santiago Zanella-Béguelin
article
2013 IEEE 26th Computer Security Foundations Symposium, Jun 2013, New Orleans, United States. IEEE Computer Society, pp.287-301, 2013, Proceedings of the 26th IEEE Computer Security Foundations Symposium. 〈10.1109/CSF.2013.26〉
Accès au bibtex
BibTex
titre
Matrices à blocs et en forme canonique
auteur
Guillaume Cano, Maxime Dénès
article
Damien Pous and Christine Tasson. JFLA – Journées francophones des langages applicatifs, Feb 2013, Aussois, France. 2013
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00779376/file/jfla2013-04.pdf BibTex
titre
EasyCrypt: A Tutorial
auteur
Gilles Barthe, Francois Dupressoir, Benjamin Grégoire, Cesar Kunz, Benedikt Schmidt, Pierre-Yves Strub
article
FOSAD 2013, 2013, Bertinoro, Italy. LNCS, 2013, Foundations of Security Analysis and Design – 2012/2013 Tutorial Lectures. 〈10.1007/978-3-319-10082-1_6〉
Accès au bibtex
BibTex

Books

titre
Homotopy Type Theory: Univalent Foundations of Mathematics
auteur
Peter Aczel, Benedikt Ahrens, Thorsten Altenkirch, Steve Awodey, Bruno Barras, Andrej Bauer, Yves Bertot, Marc Bezem, Thierry Coquand, Eric Finster, Daniel Grayson, Hugo Herbelin, André Joyal, Dan Licata, Peter Lumsdaine, Assia Mahboubi, Per Martin-Löf, Sergey Melikhov, Alvaro Pelayo, Andrew Polonsky, Michael Shulman, Matthieu Sozeau, Bas Spitters, Benno Van den Berg, Vladimir Voevodsky, Michael Warren, Carlo Angiuli, Anthony Bordg, Guillaume Brunerie, Chris Kapulkin, Egbert Rijke, Kristina Sojakova, Jeremy Avigad, Cyril Cohen, Robert Constable, Pierre-Louis Curien, Peter Dybjer, Martín Escardó, Kuen-Bang Hou, Nicola Gambino, Richard Garner, Georges Gonthier, Thomas Hales, Robert Harper, Martin Hofmann, Pieter Hofstra, Joachim Koch, Nicolai Kraus, Nuo Li, Zhaohui Luo, Michael Nahas, Erik Palmgren, Emily Riehl, Dana Scott, Philip Scott, Sergei Soloviev
article
Aucun, pp.448, 2013
Accès au bibtex
BibTex

Reports

titre
Implementation of Bourbaki’s Elements of Mathematics in Coq: Part One, Theory of Sets
auteur
José Grimm
article
[Research Report] RR-6999, INRIA. 2013, pp.205
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00408143/file/RR-6999-v6.pdf BibTex
titre
Implementation of three types of ordinals in Coq
auteur
José Grimm
article
[Research Report] RR-8407, INRIA. 2013, pp.74
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00911710/file/RR8407.pdf BibTex

Theses

titre
Étude formelle d’algorithmes efficaces en algèbre linéaire
auteur
Maxime Dénès
article
Autre [cs.OH]. Université Nice Sophia Antipolis, 2013. Français. 〈NNT : 2013NICE4103〉
Accès au texte intégral et bibtex
https://tel.archives-ouvertes.fr/tel-00945775/file/2013NICE4103.pdf BibTex

2012

Journal articles

titre
Recent Advances in the Formal Verification of Cryptographic Systems: Turing’s Legacy
auteur
Benjamin Grégoire
article
ERCIM News, ERCIM, 2012, 2012 (91)
Accès au bibtex
BibTex

Conference papers

titre
Computer-Aided Cryptographic Proofs
auteur
Gilles Barthe, Benjamin Grégoire, Santiago Zanella-Béguelin
article
Static Analysis – 19th International Symposium, SAS 2012, Sep 2012, Deauville, France. 2012, 〈10.1007/978-3-642-33125-1_1〉
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00765869/file/main.pdf BibTex
titre
Computer-Aided Cryptographic Proofs
auteur
Gilles Barthe, Juan Manuel Crespo, Benjamin Grégoire, Cesar Kunz, Santiago Zanella-Béguelin
article
ITP 2012, Aug 2012, Princeton N.J., United States. Springer, 7406, 2012, Lecture Notes in Computer Science. 〈10.1007/978-3-642-32347-8_2〉
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00765842/file/main.pdf BibTex
titre
A refinement-based approach to computational algebra in COQ
auteur
Maxime Dénès, Anders Mörtberg, Vincent Siles
article
Lennart Beringer and Amy Felty. ITP – 3rd International Conference on Interactive Theorem Proving – 2012, Aug 2012, Princeton, United States. Springer, 7406, pp.83-98, 2012, Lecture Notes In Computer Science. 〈10.1007/978-3-642-32347-8_7〉
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00734505/file/coqeal.pdf BibTex
titre
Probabilistic relational Hoare logics for computer-aided security proofs
auteur
Gilles Barthe, Benjamin Grégoire, Santiago Zanella-Béguelin
article
Jeremy Gibbons and Pablo Nogueira. Mathematics of Program Construction – 11th International Conference, MPC 2012, Jun 2012, Madrid, Spain. Springer, 7342, pp.1-6, 2012, Lecture Notes in Computer Science. 〈10.1007/978-3-642-31113-0_1〉
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00765864/file/main.pdf BibTex
titre
Verified Security of Merkle-Damgaard
auteur
Michael Backes, Gilles Barthe, Matthias Berg, Benjamin Grégoire, Cesar Kunz, Malte Skoruppa, Santiago Zanella-Béguelin
article
25th IEEE Computer Security Foundations Symposium, CSF 2012, Jun 2012, Cambridge, MA, United States. IEEE, pp.354-368, 2012, Computer Security Foundations Symposium (CSF), 2012 IEEE 25th. 〈10.1109/CSF.2012.14〉
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00765883/file/main.pdf BibTex
titre
Towards a certified computation of homology groups for digital images
auteur
Jónathan Heras, Maxime Dénès, Gadea Mata, Anders Mörtberg, María Poza, Vincent Siles
article
CTIC – Computational Topology in Image Context – 2012, May 2012, Bertinoro, Italy. Springer, 7309, pp.49-57, 2012, Lecture Notes In Computer Science. 〈10.1007/978-3-642-30238-1_6〉
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00711385/file/taccohgfdi.pdf BibTex
titre
Rigorous Polynomial Approximation using Taylor Models in Coq
auteur
Nicolas Brisebarre, Mioara Maria Joldes, Érik Martin-Dorel, Micaela Mayero, Jean-Michel Muller, Ioana Pasca, Laurence Rideau, Laurent Théry
article
Alwyn Goodloe and Suzette Person. Fourth NASA Formal Methods Symposium, Apr 2012, Norfolk, Virginia, United States. Springer, pp.15, 2012, Lecture Notes in Computer Science
Accès au texte intégral et bibtex
https://hal-ens-lyon.archives-ouvertes.fr/ensl-00653460/file/NFM2012_Brisebarre_et_al.pdf BibTex
titre
Verified Indifferentiable Hashing into Elliptic Curves
auteur
Gilles Barthe, Benjamin Grégoire, Sylvain Heraud, Federico Olmedo, Santiago Zanella-Béguelin
article
Pierpaolo Degano and Joshua D. Guttman. Principles of Security and Trust – First International Conference, POST 2012, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2012, Mar 2012, Tallinn, Estonia. Springer, 7215, pp.209-228, 2012, Lecture Notes in Computer Science. 〈10.1007/978-3-642-28641-4_12〉
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00765874/file/main.pdf BibTex

Reports

titre
Formalization and Concretization of Ordered Networks
auteur
Laurence Rideau, Bernard Serpette, Cédric Tedeschi
article
[Research Report] RR-8172, INRIA. 2012, pp.22
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00762627/file/RR-8172.pdf BibTex

Theses

titre
Vérification semi-automatique de primitives cryptographiques
auteur
Sylvain Heraud
article
Cryptographie et sécurité [cs.CR]. Université Nice Sophia Antipolis, 2012. Français
Accès au texte intégral et bibtex
https://tel.archives-ouvertes.fr/tel-00766757/file/these_heraud.pdf BibTex

2011

Journal articles

titre
A formal study of Bernstein coefficients and polynomials
auteur
Yves Bertot, Frédérique Guilhot, Assia Mahboubi
article
Mathematical Structures in Computer Science, Cambridge University Press (CUP), 2011, 21 (04), pp.731-761. 〈10.1017/S0960129511000090〉
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00503017/file/check_version_Jan_2011.pdf BibTex

Conference papers

titre
A Modular Integration of SAT/SMT Solvers to Coq through Proof Witnesses
auteur
Michaël Armand, Germain Faure, Benjamin Grégoire, Chantal Keller, Laurent Thery, Benjamin Werner
article
Jouannaud, Jean-Pierre and Shao, Zhong. CPP – Certified Programs and Proofs – First International Conference – 2011, Dec 2011, Kenting, Taiwan. Springer, 7086, pp.135-150, 2011, Lecture notes in computer science – LNCS. 〈10.1007/978-3-642-25379-9_12〉
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00639130/file/cpp11.pdf BibTex
titre
Full reduction at full throttle
auteur
Mathieu Boespflug, Maxime Dénès, Benjamin Grégoire
article
Certified Programs and Proofs, Dec 2011, Kenting, Taiwan. 2011, Certified Programs and Proofs. 〈10.1007/978-3-642-25379-9_26〉
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00650940/file/full_throttle.pdf BibTex
titre
A Formalization of Polytime Functions
auteur
Sylvain Heraud, David Nowak
article
ITP 2011, Aug 2011, Nijmegen, Netherlands. 2011
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00654217/file/itp2011-arxiv.pdf BibTex
titre
Verifying SAT and SMT in Coq for a fully automated decision procedure
auteur
Mickaël Armand, Germain Faure, Benjamin Grégoire, Chantal Keller, Laurent Théry, Benjamin Wener
article
PSATTT’11: International Workshop on Proof-Search in Axiomatic Theories and Type Theories, Aug 2011, Wroclaw, Poland. 2011
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00614041/file/ArmandAl.pdf BibTex
titre
A Flexible Proof Format for SMT: a Proposal
auteur
Frédéric Besson, Pascal Fontaine, Laurent Théry
article
Pascal Fontaine and Aaron Stump. First International Workshop on Proof eXchange for Theorem Proving – PxTP 2011, Aug 2011, Wrocław, Poland. 2011, 〈http://pxtp2011.loria.fr〉
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00642544/file/paper3.pdf BibTex
titre
Incidence simplicial matrices formalized in Coq/SSReflect
auteur
Jónathan Heras, María Poza, Maxime Denes, Laurence Rideau
article
Conference on Intelligent Computer Mathematics, Jul 2011, Bertinoro, Italy. 2011, 〈10.1007/978-3-642-22673-1_3〉
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00603208/file/ismfis.pdf BibTex
titre
A Coq-based Library for Interactive and Automated Theorem Proving in Plane Geometry
auteur
Tuan Minh Pham, Yves Bertot, Julien Narboux
article
The 11th International Conference on Computational Science and Its Applications (ICCSA 2011), Jun 2011, Santander, Spain. Springer-Verlag, 6785, pp.368-383, 2011, Lecture Notes in Computer Science. 〈10.1007/978-3-642-21898-9_32〉
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00584918/file/iccsaConf.pdf BibTex
titre
Computer-Aided Security Proofs for the Working Cryptographer
auteur
Gilles Barthe, Benjamin Grégoire, Santiago Zanella-Béguelin, Sylvain Heraud
article
Advances in Cryptology – 2011 – 31st Annual Cryptology Conference, 2011, Santa Barbara, United States. Advances in Cryptology – 2011 – 31st Annual Cryptology Conference, Santa Barbara, CA, USA, August 14-18, 2011. Proceedings, 2011, 〈10.1007/978-3-642-22792-9_5〉
Accès au bibtex
BibTex
titre
Beyond Provable Security Verifiable IND-CCA Security of OAEP
auteur
Gilles Barthe, Benjamin Grégoire, Yassine Lakhnech, Santiago Zanella-Béguelin
article
Topics in Cryptology – 2011 – The Cryptographers’ Track at the Conference 2011, San Francisco, CA, USA, February 14-18, 2011. Proceedings, 2011, San Francisco, United States. 2011, 〈10.1007/978-3-642-19074-2_13〉
Accès au bibtex
BibTex

Book sections

titre
A Formalization of Grassmann-Cayley Algebra in COQ and Its Application to Theorem Proving in Projective Geometry
auteur
Laurent Fuchs, Laurent Thery
article
Pascal Schreck; Julien Narboux; Jürgen Richter-Gebert. Automated Deduction in Geometry 8th International Workshop, ADG 2010, Munich, Germany, July 22-24, 2010, Revised Selected Papers, 6877, Springer, pp.51–62, 2011, Lecture Notes in Computer Science, 978-3-642-25069-9. 〈10.1007/978-3-642-25070-5_3〉
Accès au bibtex
BibTex
titre
Proof Certificates for Algebra and their Application to Automatic Geometry Theorem Proving
auteur
Benjamin Grégoire, Loïc Pottier, Laurent Théry
article
Thomas Sturm; Christoph Zengler. Automated Deduction in Geometry, 6301, Springer, pp.42-59, 2011, Lecture Notes in Computer Science, 978-3-642-21045-7. 〈10.1007/978-3-642-21046-4_3〉
Accès au bibtex
BibTex

Theses

titre
Formal Description of Geometrical Properties
auteur
Tuan Minh Pham
article
Logic in Computer Science [cs.LO]. Univeristé Nice Sophia Antipolis, 2011. English
Accès au texte intégral et bibtex
https://tel.archives-ouvertes.fr/tel-01112334/file/PhamThesis.pdf BibTex
titre
On type-based termination and dependent pattern matching in the calculus of inductive constructions
auteur
Jorge Sacchini
article
Performance [cs.PF]. École Nationale Supérieure des Mines de Paris, 2011. English. 〈NNT : 2011ENMP0022〉
Accès au texte intégral et bibtex
https://pastel.archives-ouvertes.fr/pastel-00622429/file/21076_SACCHINI_2011_archivage.pdf BibTex

2010

Journal articles

titre
Similar Triangles and Orientation in Plane Elementary Geometry for Coq-based Proofs
auteur
Tuan Minh Pham
article
SAC ’10 Proceedings of the 2010 ACM Symposium on Applied Computing, ACM Proceeding, 2010
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00585203/file/Sac-pham.pdf BibTex

Conference papers

titre
On Strong Normalization of the Calculus of Constructions with Type-Based Termination
auteur
Benjamin Grégoire, Jorge Sacchini
article
Christian G. Fermüller and Andrei Voronkov. 17th International Conference on Logic for Programming, Artificial Intelligence and Reasoning, Oct 2010, Yogyakarta, Indonesia. Springer, 6397, pp.333-347, 2010, Lecture notes in computer science. 〈10.1007/978-3-642-16242-8_24〉
Accès au texte intégral et bibtex
https://hal.archives-ouvertes.fr/hal-00537104/file/lpar10.pdf BibTex
titre
A Formalization of Grassmann-Cayley Algebra in COQ and Its Application to Theorem Proving in Projective Geometry
auteur
Laurent Fuchs, Laurent Thery
article
Pascal Schreck, Julien Narboux and Jürgen Richter-Gebert. Automated Deduction in Geometry, ADG 2010, Jul 2010, Munich, Germany. Springer, 6877, pp.51–62, 2011, Lecture Notes in Computer Science. 〈10.1007/978-3-642-25070-5_3〉
Accès au texte intégral et bibtex
https://hal.archives-ouvertes.fr/hal-00657901/file/fuchs_thery_adg10_postproc_final.pdf BibTex
titre
A Machine-Checked Formalization of Sigma-Protocols
auteur
Gilles Barthe, Daniel Hedin, Santiago Zanella-Béguelin, Benjamin Grégoire, Sylvain Heraud
article
CSF’10, Jul 2010, Edinburgh, Sweden. IEEE, pp.246-260, 2010, 23rd IEEE Computer Security Foundations Symposium CSF 2010. 〈10.1109/CSF.2010.24〉
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00552886/file/main.pdf BibTex
titre
Extending Coq with Imperative Features and its Application to SAT Verification
auteur
Michaël Armand, Benjamin Grégoire, Arnaud Spiwack, Laurent Théry
article
Interactive Theorem Proving, Jul 2010, Edinburgh, United Kingdom. 2010
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00502496/file/fastcoq.pdf BibTex
titre
A combination of a dynamic geometry software with a proof assistant for interactive formal proofs
auteur
Tuan Minh Pham, Yves Bertot
article
9th International Workshop On User Interfaces for Theorem Provers FLOC’10 Satellite Workshop, Jul 2010, Edinburgh, Scotland, United Kingdom. Elsevier, 2010, Electronic Notes in Theoretical Computer Science (ENTCS)
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00585400/file/paper8.pdf BibTex
titre
Formal study of plane Delaunay triangulation
auteur
Jean-François Dufourd, Yves Bertot
article
Paulson, Lawrence and Kaufmann, Matt. Interactive Theorem Proving, Jul 2010, Edinburgh, United Kingdom. Springer, 6172, pp.211-226, 2010, Lecture Notes in Computer Science. 〈http://www.springerlink.com/content/yk74674271411315/fulltext.pdf〉
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00504027/file/Del-ITP10.pdf BibTex
titre
Formally Verified Conditions for Regularity of Interval Matrices
auteur
Ioana Pasca
article
Symposium on the Integration of Symbolic Computation and Mechanised Reasoning, Calculemus, Jul 2010, Paris, France. Springer, 6167, pp.219-233, 2010, LNAI
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00464937/file/main.pdf BibTex
titre
Programming Language Techniques for Cryptographic Proofs
auteur
Gilles Barthe, Benjamin Grégoire, Santiago Zanella-Béguelin
article
Matt Kaufmann and Lawrence C. Paulson. ITP’10, 2010, Edinburgh, United Kingdom. Springer, 6172, pp.115-130, 2010, Lecture Notes in Computer Science. 〈10.1007/978-3-642-14052-5_10〉
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00552894/file/itp10.pdf BibTex

Reports

titre
Formal Proofs for Theoretical Properties of Newton’s Method
auteur
Ioana Pasca
article
[Research Report] RR-7228, INRIA. 2010
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00463150/file/RR-7228.pdf BibTex

Theses

titre
Formal certification of game-based cryptographic proofs
auteur
Santiago Zanella-Béguelin
article
Computer Science and Game Theory [cs.GT]. École Nationale Supérieure des Mines de Paris, 2010. English. 〈NNT : 2010ENMP0050〉
Accès au texte intégral et bibtex
https://pastel.archives-ouvertes.fr/pastel-00584350/file/ZANELLA.pdf BibTex
titre
Formal Verifcation for Numerical Methods
auteur
Ioana Pasca
article
Other [cs.OH]. Université Nice Sophia Antipolis, 2010. English
Accès au texte intégral et bibtex
https://tel.archives-ouvertes.fr/tel-00555158/file/pasca_phd_thesis.pdf BibTex
titre
Composants mathématiques pour la théorie des groupes
auteur
Sidi Ould Biha
article
Génie logiciel [cs.SE]. Université Nice Sophia Antipolis, 2010. Français
Accès au texte intégral et bibtex
https://tel.archives-ouvertes.fr/tel-00493524/file/sidi-thesis.pdf BibTex

2009

Journal articles

titre
Résoudre le Mini-Rubik’s Cube
auteur
Laurent Théry
article
Interstices, INRIA, 2009, 〈https://interstices.info/jcms/c_42150/resoudre-le-mini-rubik-s-cube〉
Accès au bibtex
BibTex

Conference papers

titre
Formal proof of theorems on genetic regulatory networks
auteur
Maxime Dénès, Benjamin Lesage, Yves Bertot, Adrien Richard
article
SYNASC’09, Sep 2009, Timisoara, Romania. IEEE, 2009, Synasc 2009, 11th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing
Accès au bibtex
BibTex
titre
Formal verification of exact computations using Newton’s method
auteur
Nicolas Julien, Ioana Pasca
article
Theorem Proving in Higher Order Logics, Aug 2009, Munich, Germany. Springer, 5674, pp.408-423, 2009, LNCS. 〈10.1007/978-3-642-03359-9_28〉
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00369511/file/main.pdf BibTex
titre
Finite groups representation theory with Coq
auteur
Sidi Ould Biha
article
8th International Conference on Mathematical Knowledge Management, Jul 2009, Grand Bend, Ontario, Canada. 2009
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00377431/file/main.pdf BibTex
titre
Packaging Mathematical Structures
auteur
François Garillot, Georges Gonthier, Assia Mahboubi, Laurence Rideau
article
Tobias Nipkow and Christian Urban. Theorem Proving in Higher Order Logics, 2009, Munich, Germany. Springer, 5674, 2009, Lecture Notes in Computer Science
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00368403/file/main.pdf BibTex

2008

Journal articles

titre
Tilting at windmills with Coq: formal verification of a compilation algorithm for parallel moves
auteur
Laurence Rideau, Bernard Serpette, Xavier Leroy
article
Journal of Automated Reasoning, Springer Verlag, 2008, 40 (4), pp.307-326. 〈10.1007/s10817-007-9096-8〉
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00289709/file/parallel-move.pdf BibTex

Conference papers

titre
Connecting Gröbner Bases Programs with Coq to do Proofs in Algebra, Geometry and Arithmetics
auteur
Loïc Pottier
article
Sutcliffe, G. and Rudnicki, P. and Schmidt, R. and Konev, B. and Schulz, S. Knowledge Exchange: Automated Provers and Proof Assistants, Nov 2008, Doha, Qatar. pp.418, 2008, CEUR Workshop Proceedings
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00504727/file/easychair-a4.pdf BibTex
titre
Proof Certificates for Algebra and their Application to Automatic Geometry Theorem Proving
auteur
Loïc Pottier, Laurent Théry
article
Thomas Sturm; Christoph Zengler. 7th International Workshop, ADG 2008, Sep 2008, Shangai, China. Springer, 7th International Workshop, ADG 2008, Shanghai, China, September 22-24, 2008. Revised Papers, 6301, pp.42-59, 2011, Lecture Notes in Computer Science. 〈10.1007/978-3-642-21046-4_3〉
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00504719/file/pottier.pdf BibTex
titre
Fibrational semantics for many-valued logic programs: grounds for non-groundness.
auteur
Ekaterina Komendantskaya, John Power
article
JELIA, Aug 2008, Dresden, Germany. 2008
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00295027/file/JELIAKomendaPower.pdf BibTex
titre
Canonical Big Operators
auteur
Yves Bertot, Georges Gonthier, Sidi Ould Biha, Ioana Pasca
article
Theorem Proving in Higher Order Logics, Aug 2008, Montreal, Canada. 5170/2008, 2008, LNCS. 〈10.1007/978-3-540-71067-7〉
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00331193/file/main.pdf BibTex
titre
Fixed point semantics and partial recursion in Coq
auteur
Yves Bertot, Vladimir Komendantsky
article
PPDP 2008, Jul 2008, Valencia, Spain. 2008
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00190975/file/ppdp19-bertot.pdf BibTex
titre
Certified exact real arithmetic using co-induction in arbitrary integer base
auteur
Nicolas Julien
article
FLOPS 2008, Apr 2008, ISE, Japan. 2008
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00202744/file/exactreals.pdf BibTex
titre
Inductive and Coinductive Components of Corecursive Functions in Coq
auteur
Yves Bertot, Ekaterina Komendantskaya
article
Jiri Adamek. Coalgebraic Methods in Computer Science, Apr 2008, Budapest, Hungary. 2008
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00277075/file/CMCS08BertotKomenda.pdf BibTex
titre
A New Elimination Rule for the Calculus of Inductive Constructions
auteur
Bruno Barras, Pierre Corbineau, Benjamin Grégoire, Hugo Herbelin, Jorge Sacchini
article
Stefano Berardi and Ferruccio Damiani and Ugo de’Liguoro. Types for Proofs and Programs, Mar 2008, Torino, Italy. Springer, 5497, pp.32-48, 2009, Lecture Notes in Computer Science. 〈10.1007/978-3-642-02444-3_3〉
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00524938/file/types-BarCorGreHerSac08-dep-matching.pdf BibTex
titre
Structural abstract interpretation, A formal study using Coq
auteur
Yves Bertot
article
Ana Bove and Jorge Sousa Pinto. LERNET Summer School, Feb 2008, Piriapolis, Uruguay. Springer, 2008, Lecture Notes in Computer Science
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00329572/file/absint.pdf BibTex
titre
A Formal Verification for Kantorovitch’s Theorem
auteur
Ioana Pasca
article
JFLA (Journées Francophones des Langages Applicatifs), Jan 2008, Etretat, France. pp.15-30, 2008
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00202808/file/pasca.pdf BibTex
titre
Formalisation des mathématiques : une preuve du théorème de Cayley-Hamilton
auteur
Sidi Ould Biha
article
JFLA (Journées Francophones des Langages Applicatifs), Jan 2008, Etretat, France. pp.1-14, 2008
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00202795/file/ouldbiha.pdf BibTex
titre
Using Structural Recursion for Corecursion
auteur
Yves Bertot, Ekaterina Komendantskaya
article
Stefano Berardi and Feruccio Damiani and Ugo de Liguoro. Types 2008, 2008, Torino, Italy. Springer, 5497, pp.220-236, 2008, Lecture Notes in Computer Science
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00322331/file/fibonacci.pdf BibTex

2007

Conference papers

titre
Primality Proving with Elliptic Curves
auteur
Laurent Théry, Guillaume Hanrot
article
Klaus Schneider and Jens Brandt. TPHOL 2007, Sep 2007, Kaiserslautern, Germany. Springer-Verlag, 4732, pp.319-333, 2007, LNCS
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00138382/file/paper.pdf BibTex
titre
Arithmétique réelle exacte certifiée, co-induction et base arbitraire
auteur
Nicolas Julien
article
Journées Francophones des Langages Applicatifs, Jan 2007, Aix-les-Bains, 2007
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00116820/file/exactreals.pdf BibTex

Reports

titre
A Modular Formalisation of Finite Group Theory
auteur
Georges Gonthier, Assia Mahboubi, Laurence Rideau, Enrico Tassi, Laurent Théry
article
[Research Report] RR-6156, INRIA. 2007, pp.17
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00139131/file/RR-6156.pdf BibTex
titre
Proving the group law for elliptic curves formally
auteur
Laurent Thery
article
[Technical Report] RT-0330, INRIA. 2007, pp.16
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00129237/file/RT-0330.pdf BibTex
titre
Theorem proving support in programming language semantics
auteur
Yves Bertot
article
[Research Report] RR-6242, INRIA. 2007, pp.23
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00160309/file/RR-6242.pdf BibTex

Preprints, Working Papers, …

titre
Battling windmills with Coq: formal verification of a compilation algorithm for parallel moves
auteur
Laurence Rideau, Bernard Serpette, Xavier Leroy
article
2007
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00176007/file/pmov.pdf BibTex

2006

Journal articles

titre
Affine functions and series with co-inductive real numbers
auteur
Yves Bertot
article
Mathematical Structures in Computer Science, Cambridge University Press (CUP), 2006, 17 (1), pp.37-63. 〈10.1017/S0960129506005809〉
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00001171/file/a.pdf BibTex

Conference papers

titre
Proving formally the implementation of an efficient gcd algorithm for polynomials
auteur
Assia Mahboubi
article
Ulrich Furbach and Natarajan Shankar. Automated Reasoning, Third International Joint Conference, IJCAR 2006, Aug 2006, Seattle, WA, United States. Springer, 4130, pp.438-452, 2006, Lecture Notes in Computer Science
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00001270/file/SousRes.pdf BibTex

Lectures

titre
lambda-calcul et types
auteur
Yves Bertot
article
Ecole Jeunes Chercheurs en Programmation (CNRS-INRIA) Toulouse, 2006
Accès au texte intégral et bibtex
https://cel.archives-ouvertes.fr/inria-00083975/file/types.pdf BibTex

Reports

titre
Extending the Calculus of Constructions with Tarski’s fix-point theorem
auteur
Yves Bertot
article
[Research Report] 2006, pp.15
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00105529/file/a.pdf BibTex
titre
Formalising Sylow’s theorems in Coq
auteur
Laurent Thery, Laurence Rideau
article
[Technical Report] RT-0327, INRIA. 2006, pp.23
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00113750/file/RT-0327.pdf BibTex
titre
Ambiguous Typing
auteur
Loïc Pottier
article
[Research Report] RR-6041, INRIA. 2006, pp.11
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00117458/file/RR-6041.pdf BibTex

Theses

titre
Contributions à la certification des calculs dans R : théorie, preuves, programmation
auteur
Assia Mahboubi
article
Génie logiciel [cs.SE]. Université Nice Sophia Antipolis, 2006. Français
Accès au texte intégral et bibtex
https://tel.archives-ouvertes.fr/tel-00117409/file/these_assia_mahboubi.pdf BibTex

2005

Journal articles

titre
Vérification formelle d’extractions de racines entières
auteur
Yves Bertot
article
Revue des Sciences et Technologies de l’Information – Série TSI : Technique et Science Informatiques, Lavoisier, 2005, Langages Applicatifs, Spécifications, Programmation, Vérification, 24 (9), pp.1161-1195
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00001172/file/racines.pdf BibTex

Conference papers

titre
Coq à la conquête des moulins
auteur
Laurence Rideau, Bernard Serpette
article
Olivier Michel. JFLA ‘2005, Mar 2005, Obernai, INRIA, pp.169-180, 2005, JFLA 2005 : actes de la conférence journées francophones des langages applicatifs
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00001128/file/RideauSerpetteJFLA05.pdf BibTex

Lectures

titre
CoInduction in Coq
auteur
Yves Bertot
article
DEA. EU’s coordination action Types Goteborg, 2005
Accès au texte intégral et bibtex
https://cel.archives-ouvertes.fr/inria-00001174/file/co.pdf BibTex

2004

Conference papers

titre
A structured approach to proving compiler optimizations based on dataflow analysis
auteur
Yves Bertot, Benjamin Grégoire, Xavier Leroy
article
Types for Proofs and Programs, Workshop TYPES 2004, Dec 2004, Jouy-en-Josas, France. Springer, 3839, pp.66-81, 2006, Lecture Notes in Computer Science. 〈10.1007/11617990〉
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00289549/file/proofs_dataflow_optimizations.pdf BibTex

Books

titre
Interactive theorem proving and program development. Coq’Art: The Calculus of inductive constructions.
auteur
Pierre Castéran, Yves Bertot
article
Springer Verlag, pp.470, 2004, Texts in Theoretical Computer Science
Accès au bibtex
BibTex