Sites Inria

English version

Equipe de recherche MARELLE

Publications de l'équipe MARELLE

2019

Article dans une revue

titre
Mechanisms of formation of slurry aluminide coatings from Al and Cr microparticles
auteur
Benjamin Grégoire, Gilles Bonnet, Fernando Pedraza
article
Surface and Coatings Technology, Elsevier, 2019, 359, pp.323-333. ⟨10.1016/j.surfcoat.2018.11.077⟩
Accès au bibtex
BibTex

Communication dans un congrès

titre
Symbolic methods in computational cryptography proofs
auteur
Gilles Barthe, Benjamin Grégoire, Charlie Jacomme, Steve Kremer, Pierre-Yves Strub
article
CSF 2019 - 32nd IEEE Computer Security Foundations Symposium, Jun 2019, Hoboken, United States
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-02117794/file/paper.pdf BibTex
titre
Formal Proofs of Tarjan's Strongly Connected Components Algorithm in Why3, Coq and Isabelle
auteur
Ran Chen, Cyril Cohen, Jean-Jacques Levy, Stephan Merz, Laurent Théry
article
ITP 2019 - 10th International Conference on Interactive Theorem Proving, Sep 2019, Portland, United States. pp.13:1 - 13:19, ⟨10.4230/LIPIcs.ITP.2019.13⟩
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-02303987/file/LIPIcs-ITP-2019-13.pdf BibTex

Thèse

titre
Formalisation Tools for Classical Analysis − A Case Study in Control Theory
auteur
Damien Rouhling
article
Computer Science [cs]. Université Côte d'Azur, 2019. English
Accès au texte intégral et bibtex
https://hal.inria.fr/tel-02333396/file/thesis.pdf BibTex

Pré-publication, Document de travail

titre
Completeness of an Axiomatization of Graph Isomorphism via Graph Rewriting in Coq
auteur
Christian Doczkal, Damien Pous
article
2019
Accès au texte intégral et bibtex
https://hal.archives-ouvertes.fr/hal-02333553/file/coq-2pdom.pdf BibTex
titre
The MetaCoq Project
auteur
Matthieu Sozeau, Abhishek Anand, Simon Boulier, Cyril Cohen, Yannick Forster, Fabian Kunze, Gregory Malecha, Nicolas Tabareau, Théo Winterhalter
article
2019
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-02167423/file/The_MetaCoq_Project.pdf BibTex
titre
Deriving proved equality tests in Coq-elpi: Stronger induction principles for containers in Coq
auteur
Enrico Tassi
article
2019
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01897468/file/induction.pdf BibTex
titre
Quantitative continuity and computable analysis in Coq
auteur
Florian Steinberg, Laurent Thery, Holger Thies
article
2019
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-02088293/file/paper.pdf BibTex
titre
Type-two polynomial-time and restricted lookahead
auteur
Bruce M. Kapron, Florian Steinberg
article
2019
Accès au bibtex
https://arxiv.org/pdf/1801.07485 BibTex

2018

Article dans une revue

titre
Formalization Techniques for Asymptotic Reasoning in Classical Analysis
auteur
Reynald Affeldt, Cyril Cohen, Damien Rouhling
article
Journal of Formalized Reasoning, ASDD-AlmaDL, 2018
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01719918/file/8124-27375-1-PB.pdf BibTex
titre
Proving expected sensitivity of probabilistic programs
auteur
Gilles Barthe, Thomas Espitau, Benjamin Grégoire, Justin Hsu, Pierre-Yves Strub
article
Proceedings of the ACM on Programming Languages, ACM, 2018, 2 (POPL), pp.1-29. ⟨10.1145/3158145⟩
Accès au texte intégral et bibtex
https://hal.archives-ouvertes.fr/hal-01959322/file/bounded.pdf BibTex

Communication dans un congrès

titre
Symbolic Proofs for Lattice-Based Cryptography
auteur
Gilles Barthe, Xiong Fan, Joshua Gancher, Benjamin Grégoire, Charlie Jacomme, Elaine Shi
article
CCS 2018 - Proceedings of the 2018 ACM SIGSAC Conference on Computer and Communications Security Canada, October 15-19, 2018, Oct 2018, Toronto, Canada. pp.538-555, ⟨10.1145/3243734.3243825⟩
Accès au texte intégral et bibtex
https://hal.archives-ouvertes.fr/hal-01959391/file/paper.pdf BibTex
titre
Formal Verification of a Geometry Algorithm: A Quest for Abstract Views and Symmetry in Coq Proofs
auteur
Yves Bertot
article
ICTAC 2018 - International Colloquium on Theoretical of Computing, Oct 2018, Stellenbosch, South Africa
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01866271/file/main.pdf BibTex
titre
Formal Security Proof of CMAC and Its Variants
auteur
Cécile Baritel-Ruet, François Dupressoir, Pierre-Alain Fouque, Benjamin Grégoire
article
CSF 2018 - 31st EEE Computer Security Foundations Symposium, Jul 2018, Oxford, United Kingdom
Accès au texte intégral et bibtex
https://hal.archives-ouvertes.fr/hal-01959554/file/main.pdf BibTex
titre
Secure Compilation of Side-Channel Countermeasures: The Case of Cryptographic “Constant-Time”
auteur
Gilles Barthe, Benjamin Grégoire, Vincent Laporte
article
CSF 2018 - 31st IEEE Computer Security Foundations Symposium, Jul 2018, Oxford, United Kingdom
Accès au texte intégral et bibtex
https://hal.archives-ouvertes.fr/hal-01959560/file/main.pdf BibTex
titre
Vectorizing Higher-Order Masking
auteur
Benjamin Grégoire, Kostas Papagiannopoulos, Peter Schwabe, Ko Stoffelen
article
COSADE 2018 - Constructive Side-Channel Analysis and Secure Design - 9th International Workshop., Apr 2018, Singapore, Singapore. pp.23-43
Accès au texte intégral et bibtex
https://hal.archives-ouvertes.fr/hal-01959418/file/neonshares-20180406.pdf BibTex
titre
An Assertion-Based Program Logic for Probabilistic Programs
auteur
Gilles Barthe, Thomas Espitau, Marco Gaboardi, Benjamin Grégoire, Justin Hsu, Pierre-Yves Strub
article
Programming Languages and Systems - 27th European Symposium on Programming, 2018, Held as Part of the European Joint Conferences on Theory and Practice of Software, 2018, Thessaloniki, Greece, April 14-20, 2018, Proceedings, Apr 2018, Thessaloniki, Greece. pp.117-144
Accès au texte intégral et bibtex
https://hal.archives-ouvertes.fr/hal-01959567/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
21st International Conference on Types for Proofs and Programs, May 2015, Tallinn, Estonia. pp.262, ⟨10.4230/LIPIcs.TYPES.2015.5⟩
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01378906/file/LIPIcs-TYPES-2015-5.pdf BibTex
titre
A Formal Proof in Coq of a Control Function for the Inverted Pendulum
auteur
Damien Rouhling
article
CPP 2018 - 7th ACM SIGPLAN International Conference on Certified Programs and Proofs, Jan 2018, Los Angeles, United States. pp.1-14, ⟨10.1145/3167101⟩
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01639819/file/poplws18cppmain-id41-p-ef0777f-34741-final.pdf BibTex
titre
A Constructive Formalisation of Semi-algebraic Sets and Functions
auteur
Boris Djalal
article
CPP 2018 - Proceedings of the 7th ACM SIGPLAN International Conference on Certified Programs and Proofs, Jan 2018, Los Angeles, California, United States. pp.240-251
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01643919/file/CPP_2018_paper_Boris_Djalal.pdf BibTex
titre
Towards Certified Meta-Programming with Typed Template-Coq
auteur
Abhishek Anand, Simon Boulier, Cyril Cohen, Matthieu Sozeau, Nicolas Tabareau
article
ITP 2018 - 9th Conference on Interactive Theorem Proving, Jul 2018, Oxford, United Kingdom. pp.20-39, ⟨10.1007/978-3-319-94821-8_2⟩
Accès au texte intégral et bibtex
https://hal.archives-ouvertes.fr/hal-01809681/file/paper_39.pdf BibTex
titre
Masking the GLP Lattice-Based Signature Scheme at Any Order
auteur
Gilles Barthe, Sonia Belaïd, Thomas Espitau, Pierre-Alain Fouque, Benjamin Grégoire, Mélissa Rossi, Mehdi Tibouchi
article
Eurocrypt 2018 - 37th Annual International Conference on the Theory and Applications of Cryptographic Techniques, Apr 2018, Tel Aviv, Israel. pp.354-384, ⟨10.1007/978-3-319-78375-8_12⟩
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01900708/file/2018-381.pdf BibTex

Document associé à des manifestations scientifiques

titre
A simple universal machine of type two and a formal proof of its correctness
auteur
Florian Steinberg
article
CCA 2018 - 15th International Conference on Computability and Complexity in Analysis, Aug 2018, Kochel, Germany
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-02019706/file/CCA2018Abstracts-7-8.pdf BibTex

Rapport

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. 2018, pp.826
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00440786/file/RR-7150-v10.pdf BibTex

Logiciel

titre
The Coq Proof Assistant, version 8.8.0
auteur
The Coq Development Team
article
2018
Accès au bibtex
BibTex
titre
Formal study in Coq of pi computations using arithmetic-geometric means
auteur
Yves Bertot
article
2018, ⟨swh:1:rev:b1e197c030e66d588987087a193fc3a88d8bd5ed⟩
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01767263/file/pi-agm-1.0.0.zip BibTex

Pré-publication, Document de travail

titre
Implementing Type Theory in Higher Order Constraint Logic Programming
auteur
Ferruccio Guidi, Claudio Sacerdoti Coen, Enrico Tassi
article
2018
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01410567/file/dalefest.pdf BibTex
titre
Formal Proofs of Tarjan's Algorithm in Why3, Coq, and Isabelle
auteur
Ran Chen, Cyril Cohen, Jean-Jacques Levy, Stephan Merz, Laurent Thery
article
2018
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01906155/file/paper.pdf BibTex
titre
Elpi: an extension language for Coq (Metaprogramming Coq in the Elpi λProlog dialect)
auteur
Enrico Tassi
article
2018
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01637063/file/coqpl2018.pdf BibTex

2017

Article dans une revue

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, In press, pp.1-45
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01582524/file/main.pdf BibTex

Communication dans un congrès

titre
A Fast and Verified Software Stack for Secure Function Evaluation
auteur
José Almeida, Manuel Barbosa, Gilles Barthe, Francois Dupressoir, Benjamin Grégoire, Vincent Laporte, Vitor Pereira
article
CCS 2017 - ACM SIGSAC Conference on Computer and Communications Security, Oct 2017, Dallas, United States. pp.1-18
Accès au texte intégral et bibtex
https://hal.archives-ouvertes.fr/hal-01649104/file/jasmin.pdf BibTex
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
Formal correctness of comparison algorithms between binary64 and decimal64 floating-point numbers
auteur
Arthur Blot, Jean-Michel Muller, Laurent Théry
article
Numerical Software Verification, Jul 2017, Heidelberg, Germany
Accès au texte intégral et bibtex
https://hal.archives-ouvertes.fr/hal-01512294/file/paper.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
https://hal.sorbonne-universite.fr/hal-01541198/file/1701.06477.pdf BibTex
titre
Coupling proofs are probabilistic product programs
auteur
Gilles Barthe, Benjamin Grégoire, Justin Hsu, Pierre-Yves Strub
article
POPL 2017 - Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, Jan 2017, Paris, France. pp.161-174, ⟨10.1145/3009837.3009896⟩
Accès au texte intégral et bibtex
https://hal.archives-ouvertes.fr/hal-01649028/file/main.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
titre
Formalization of the Lindemann-Weierstrass Theorem
auteur
Sophie Bernard
article
Interactive Theorem Proving, Sep 2017, Brasilia, Brazil
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01647563/file/main.pdf BibTex
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
Advances in Cryptology - 2017 - 36th Annual International Conference on the Theory and Applications of Cryptographic Techniques, Apr 2017, Paris, France. pp.535--566
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01414009/file/parallel_masking_4.pdf BibTex
titre
Jasmin: High-Assurance and High-Speed Cryptography
auteur
José Almeida, Manuel Barbosa, Gilles Barthe, Arthur Blot, Benjamin Grégoire, Vincent Laporte, Tiago Oliveira, Hugo Pacheco, Benedikt Schmidt, Pierre-Yves Strub
article
CCS 2017 - Proceedings of the 2017 ACM SIGSAC Conference on Computer and Communications Security, Oct 2017, Dallas, United States. pp.1-17
Accès au texte intégral et bibtex
https://hal.archives-ouvertes.fr/hal-01649140/file/main.pdf BibTex

Autre publication

titre
The Coq Proof Assistant, version 8.7.1
auteur
The Coq Development Team
article
2017, pp.1-571. ⟨10.5281/zenodo.1133970⟩
Accès au bibtex
BibTex

Pré-publication, Document de travail

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

Article dans une revue

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

Communication dans un congrès

titre
Boolean reflection via type classes
auteur
Benjamin Grégoire, Enrico Tassi
article
Coq Workshop, Aug 2016, Nancy, France
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
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. pp.10, ⟨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
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
Certified Programs and Proofs, Jan 2016, St Petersburg, Florida, United States. pp.12
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
Certified Programs and Proofs, Jan 2016, St. Petersburg, Florida, United States
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01240469/file/main.pdf BibTex
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
CCS 2016 - 23rd ACM Conference on Computer and Communications Security, Oct 2016, Vienne, Austria. pp.116 - 129, ⟨10.1145/2976749.2978427⟩
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01410216/file/main.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, ⟨10.1145/2933575.2934554⟩
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01411097/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, ⟨10.1145/2976749.2978391⟩
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01410196/file/main.pdf BibTex

Cours

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

Rapport

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

2015

Article dans une revue

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

Communication dans un congrès

titre
ELPI: fast, Embeddable, λProlog Interpreter
auteur
Cvetan Dunchev, Ferruccio Guidi, Claudio Sacerdoti Coen, Enrico Tassi
article
Proceedings of LPAR, Nov 2015, Suva, Fiji
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. ⟨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. ⟨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. ⟨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, ⟨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

Cours

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

Pré-publication, Document de travail

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

Article dans une revue

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
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
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
Accès au bibtex
BibTex

Communication dans un congrès

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. pp.16, ⟨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. pp.206 - 222, ⟨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
A Logical Framework for Systems Biology
auteur
Elisabetta de Maria, Joëlle Despeyroux, Amy Felty
article
FMMB 2014 - First International Conference on Formal Methods in Macro-Biology, Sep 2014, Noumea, France. ⟨10.1007/978-3-319-10398-3_10⟩
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01285058/file/fmmb14-final.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, ⟨10.1109/CSF.2014.19⟩
Accès au bibtex
BibTex
titre
Links between homotopy theory and type theory
auteur
Yves Bertot
article
CICM - Conference on Intelligent Computer Mathematics, Jul 2014, Coimbra, Portugal
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
Accès au bibtex
BibTex

Rapport

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

Thèse

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

Pré-publication, Document de travail

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

Article dans une revue

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

Communication dans un congrès

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, ⟨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. pp.1247-1260, ⟨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
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
Computer Science Logic 2013, Aug 2013, Dagstuhl, Germany. pp.653--667, ⟨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
ITP 2013, 4th Conference on Interactive Theorem Proving, Jul 2013, Rennes, France. pp.163-179, ⟨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. pp.287-301, ⟨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
JFLA - Journées francophones des langages applicatifs, Damien Pous and Christine Tasson, Feb 2013, Aussois, France
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00779376/file/jfla2013-04.pdf BibTex
titre
Pragmatic Quotient Types in Coq
auteur
Cyril Cohen
article
International Conference on Interactive Theorem Proving, Jul 2013, Rennes, France. pp.16
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01966714/file/main.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. ⟨10.1007/978-3-319-10082-1_6⟩
Accès au bibtex
BibTex

Ouvrage (y compris édition critique et traduction)

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

Rapport

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
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.213
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00408143/file/RR-6999-v7.pdf BibTex

Thèse

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

Article dans une revue

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

Communication dans un congrès

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. ⟨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. ⟨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
ITP - 3rd International Conference on Interactive Theorem Proving - 2012, Aug 2012, Princeton, United States. pp.83-98, ⟨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
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. pp.354-368, ⟨10.1109/CSF.2012.14⟩
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00765883/file/main.pdf BibTex
titre
Probabilistic relational Hoare logics for computer-aided security proofs
auteur
Gilles Barthe, Benjamin Grégoire, Santiago Zanella-Béguelin
article
Mathematics of Program Construction - 11th International Conference, MPC 2012, Jun 2012, Madrid, Spain. pp.1-6, ⟨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
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. pp.49-57, ⟨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
Fourth NASA Formal Methods Symposium, NASA, Apr 2012, Norfolk, Virginia, United States. pp.15
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
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. pp.209-228, ⟨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

Rapport

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

Thèse

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

Article dans une revue

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

Communication dans un congrès

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. ⟨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 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
CPP - Certified Programs and Proofs - First International Conference - 2011, Dec 2011, Kenting, Taiwan. pp.135-150, ⟨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
A Formalization of Polytime Functions
auteur
Sylvain Heraud, David Nowak
article
ITP 2011, Aug 2011, Nijmegen, Netherlands
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00654217/file/itp2011-arxiv.pdf BibTex
titre
A Flexible Proof Format for SMT: a Proposal
auteur
Frédéric Besson, Pascal Fontaine, Laurent Théry
article
First International Workshop on Proof eXchange for Theorem Proving - PxTP 2011, Aug 2011, Wrocław, Poland
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00642544/file/paper3.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, Germain Faure, Stéphane Lengrand, Assia Mahboubi, Aug 2011, Wroclaw, Poland
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00614041/file/ArmandAl.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. ⟨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. pp.368-383, ⟨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
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. ⟨10.1007/978-3-642-19074-2_13⟩
Accès au bibtex
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. ⟨10.1007/978-3-642-22792-9_5⟩
Accès au bibtex
BibTex

Chapitre d'ouvrage

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

Thèse

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

Article dans une revue

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

Communication dans un congrès

titre
On Strong Normalization of the Calculus of Constructions with Type-Based Termination
auteur
Benjamin Grégoire, Jorge Sacchini
article
17th International Conference on Logic for Programming, Artificial Intelligence and Reasoning, Oct 2010, Yogyakarta, Indonesia. pp.333-347, ⟨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
Automated Deduction in Geometry, ADG 2010, Jul 2010, Munich, Germany. pp.51--62, ⟨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. pp.246-260, ⟨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
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
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
Interactive Theorem Proving, Jul 2010, Edinburgh, United Kingdom. pp.211-226
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. pp.219-233
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
ITP'10, 2010, Edinburgh, United Kingdom. pp.115-130, ⟨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

Rapport

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

Thèse

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

Article dans une revue

titre
Résoudre le Mini-Rubik’s Cube
auteur
Laurent Théry
article
Interstices, INRIA, 2009
Accès au bibtex
BibTex

Communication dans un congrès

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
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. pp.408-423, ⟨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
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
Theorem Proving in Higher Order Logics, 2009, Munich, Germany
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00368403/file/main.pdf BibTex

2008

Article dans une revue

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

Communication dans un congrès

titre
Connecting Gröbner Bases Programs with Coq to do Proofs in Algebra, Geometry and Arithmetics
auteur
Loïc Pottier
article
Knowledge Exchange: Automated Provers and Proof Assistants, Nov 2008, Doha, Qatar. pp.418
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
7th International Workshop, ADG 2008, Sep 2008, Shangai, China. pp.42-59, ⟨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
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. ⟨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
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
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
Coalgebraic Methods in Computer Science, Apr 2008, Budapest, Hungary
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
Types for Proofs and Programs, Mar 2008, Torino, Italy. pp.32-48, ⟨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
LERNET Summer School, Ana Bove and Jorge Sousa Pinto, Feb 2008, Piriapolis, Uruguay
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), INRIA, Jan 2008, Etretat, France. pp.15-30
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), INRIA, Jan 2008, Etretat, France. pp.1-14
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
Types 2008, 2008, Torino, Italy. pp.220-236
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00322331/file/fibonacci.pdf BibTex

2007

Communication dans un congrès

titre
Primality Proving with Elliptic Curves
auteur
Laurent Théry, Guillaume Hanrot
article
TPHOL 2007, Sep 2007, Kaiserslautern, Germany. pp.319-333
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
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00116820/file/exactreals.pdf BibTex

Rapport

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
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
titre
Proving the group law for elliptic curves formally
auteur
Laurent Théry
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

Pré-publication, Document de travail

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

Article dans une revue

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

Communication dans un congrès

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

Cours

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

Rapport

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 Théry, 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

Thèse

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

Article dans une revue

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

Communication dans un congrès

titre
Coq à la conquête des moulins
auteur
Laurence Rideau, Bernard Serpette
article
JFLA '2005, INRIA, Mar 2005, Obernai, pp.169-180
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00001128/file/RideauSerpetteJFLA05.pdf BibTex

Cours

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

Communication dans un congrès

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. pp.66-81, ⟨10.1007/11617990⟩
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00289549/file/proofs_dataflow_optimizations.pdf BibTex

Ouvrage (y compris édition critique et traduction)

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

2001

Communication dans un congrès

titre
Formalizing Convex Hulls Algorithms
auteur
David Pichardie, Yves Bertot
article
TPHOLs 2001 - 14th International Conference Theorem Proving in Higher Order Logics, Sep 2001, Edinburgh, United Kingdom. pp.346-361, ⟨10.1007/3-540-44755-5_24⟩
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01702679/file/hulls.pdf BibTex

Suivez Inria