2020
Communication dans un congrès
- titre
- Completeness of an Axiomatization of Graph Isomorphism via Graph Rewriting in Coq
- auteur
- Christian Doczkal, Damien Pous
- article
- CPP 2020 – 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, Jan 2020, New Orleans, LA, United States. ⟨10.1145/3372885.3373831⟩
- Accès au texte intégral et bibtex
-
2019
Article dans une revue
- titre
- Implementing Type Theory in Higher Order Constraint Logic Programming
- auteur
- Ferruccio Guidi, Claudio Sacerdoti Coen, Enrico Tassi
- article
- Mathematical Structures in Computer Science, 2019, 29 (8), pp.1125-1150
- Accès au texte intégral et bibtex
-
Communication dans un congrès
- titre
- A Machine-Checked Proof of Security for AWS Key Management Service
- auteur
- José Bacelar Almeida, Manuel Barbosa, Gilles Barthe, Matthew Campagna, Ernie Cohen, Benjamin Grégoire, Vitor Pereira, Bernardo Portela, Pierre-Yves Strub, Serdar Tasiran
- article
- ACM CCS 2019 – 26th ACM Conference on Computer and Communications Security, Nov 2019, London, United Kingdom. pp.63-78, ⟨10.1145/3319535.3354228⟩
- Accès au texte intégral et bibtex
-
- titre
- Machine-Checked Proofs for Cryptographic Standards: Indifferentiability of Sponge and Secure High-Assurance Implementations of SHA-3
- auteur
- José Bacelar Almeida, Cécile Baritel-Ruet, Manuel Barbosa, Gilles Barthe, François Dupressoir, Benjamin Grégoire, Vincent Laporte, Tiago Oliveira, Alley Stoughton, Pierre-Yves Strub
- article
- CCS 2019 – 26th ACM Conference on Computer and Communications Security, Nov 2019, London, United Kingdom. pp.1607-1622, ⟨10.1145/3319535.3363211⟩
- Accès au texte intégral et bibtex
-
- titre
- Automated Verification of Higher-Order Masking in Presence of Physical Defaults
- auteur
- Gilles Barthe, Sonia Belaïd, Gaëtan Cassiers, Pierre-Alain Fouque, Benjamin Grégoire, François-Xavier Standaert
- article
- ESORICS 2019 – 24th European Symposium on Research in Computer Security, Sep 2019, Luxembourg, Luxembourg. pp.300-318, ⟨10.1007/978-3-030-29959-0_15⟩
- Accès au texte intégral et bibtex
-
- titre
- Deriving proved equality tests in Coq-elpi: Stronger induction principles for containers in Coq
- auteur
- Enrico Tassi
- article
- ITP 2019 – 10th International Conference on Interactive Theorem Proving, Sep 2019, Portland, United States. ⟨10.4230/LIPIcs.CVIT.2016.23⟩
- Accès au texte intégral et bibtex
-
- titre
- Quantitative continuity and Computable Analysis in Coq
- auteur
- Florian Steinberg, Holger Thies, Laurent Théry
- article
- ITP 2019 – Tenth International Conference on Interactive Theorem Proving, Sep 2019, Portland, United States. ⟨10.4230/LIPIcs.ITP.2019.28⟩
- Accès au 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
-
- titre
- Symbolic Methods in Computational Cryptography Proofs
- auteur
- Gilles Barthe, Benjamin Grégoire, Charlie Jacomme, Steve Kremer, Pierre-Yves Strub
- article
- CSF2019 – 32nd IEEE Computer Security Foundations Symposium, Jun 2019, Hoboken, United States. pp.136-13615, ⟨10.1109/CSF.2019.00017⟩
- Accès au texte intégral et bibtex
-
- titre
- FaCT: A DSL for Timing-Sensitive Computation
- auteur
- Sunjay Cauligi, Gary Soeller, Brian Johannesmeyer, Fraser Brown, Riad S Wahby, John Renner, Benjamin Grégoire, Gilles Barthe, Ranjit Jhala, Deian Stefan
- article
- PLDI 2019 – 40th ACM SIGPLAN Conference on Programming Language Design and Implementation, Jun 2019, Phoenix, United States. ⟨10.1145/3314221.3314605⟩
- Accès au texte intégral et bibtex
-
Thèse
- titre
- Formalisation tools for classical analysis : a case study in control theory
- auteur
- Damien Rouhling
- article
- Logic in Computer Science [cs.LO]. Université Côte d’Azur, 2019. English. ⟨NNT : 2019AZUR4058⟩
- Accès au texte intégral et bibtex
-
Pré-publication, Document de travail
- titre
- Quantitative continuity and computable analysis in Coq
- auteur
- Florian Steinberg, Laurent Théry, Holger Thies
- article
- 2019
- Accès au texte intégral et bibtex
-
- titre
- Type-two polynomial-time and restricted lookahead
- auteur
- Bruce M. Kapron, Florian Steinberg
- article
- 2019
- Accès au 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, 2018
- Accès au texte intégral et bibtex
-
- titre
- Distant decimals of $π$
- auteur
- Yves Bertot, Laurence Rideau, Laurent Théry
- article
- Journal of Automated Reasoning, 2018, 61, pp.33-71. ⟨10.1007/s10817-017-9444-2⟩
- Accès au texte intégral et bibtex
-
Communication dans un congrès
- 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
-
- 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
-
- 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
-
- 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
-
- 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
-
- 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
-
- 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
-
- 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
- Lecture Notes in Computer Science, Apr 2018, Thessaloniki, Greece. pp.117-144, ⟨10.1007/978-3-319-89884-1_5⟩
- Accès au texte intégral et bibtex
-
- titre
- Elpi: an extension language for Coq (Metaprogramming Coq in the Elpi λProlog dialect)
- auteur
- Enrico Tassi
- article
- The Fourth International Workshop on Coq for Programming Languages, Jan 2018, Los Angeles (CA), United States
- Accès au texte intégral et 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
-
- 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
-
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
-
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
-
Logiciel
- titre
- The Coq Proof Assistant, version 8.8.0
- auteur
- The Coq Development Team
- article
- 2018
- Accès au bibtex
-
- titre
- Formal study in Coq of pi computations using arithmetic-geometric means
- auteur
- Yves Bertot
- article
- 2018, ⟨swh:1:dir:47d41cb06472ccf913aba4be5b08aeb725a8888d;origin=https://hal.archives-ouvertes.fr/hal-01767263;visit=swh:1:snp:cd55c2657ac70c9b15ae4384b6af1ae6ce8df512;anchor=swh:1:rev:b1e197c030e66d588987087a193fc3a88d8bd5ed;path=/⟩
- Accès au texte intégral et bibtex
-
Pré-publication, Document de travail
- 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
-
2017
Article dans une revue
- 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, 2017, 2 (POPL), pp.1-29. ⟨10.1145/3158145⟩
- Accès au texte intégral et bibtex
-
- titre
- Coqoon
- auteur
- Alexander Faithfull, Jesper Bengtson, Enrico Tassi, Carst Tankink
- article
- International Journal on Software Tools for Technology Transfer, 2017
- Accès au texte intégral et bibtex
-
Communication dans un congrès
- titre
- A Fast and Verified Software Stack for Secure Function Evaluation
- auteur
- José Bacelar 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
-
- titre
- Jasmin: High-Assurance and High-Speed Cryptography
- auteur
- José Bacelar 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
-
- 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
-
- 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
-
- 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
-
- 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
-
- 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 – {EUROCRYPT} 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
-
- 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
-
- 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
-
- 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
-
Autre publication scientifique
- 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
-
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
-
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, 2016, ⟨10.2168/LMCS-12(2:7)2016⟩
- Accès au texte intégral et 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, 2016, 9 (2), pp.52. ⟨10.6092/issn.1972-5787/4771⟩
- Accès au texte intégral et bibtex
-
Communication dans un congrès
- 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
-
- 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
-
- 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
-
- 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
-
- 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
-
- 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
-
- 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
-
- 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
-
- 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
-
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
-
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
-
- 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
-
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, 2015, 54 (1), pp.1-29. ⟨10.1007/s10817-014-9312-2⟩
- Accès au texte intégral et 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
-
- titre
- Automated Proofs of Pairing-Based Cryptography
- auteur
- Gilles Barthe, Benjamin Grégoire, Benedikt Schmidt
- article
- Proceedings of the 22nd {ACM} {SIGSAC} Conference on Computer and Communications Security, Oct 2015, Denver, United States. ⟨10.1145/2810103.2813697⟩
- Accès au 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
-
- 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
-
- 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
-
- 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
-
- 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
-
Cours
- titre
- Semantics for programming languages with Coq encodings
- auteur
- Yves Bertot
- article
- Master. France. 2015
- Accès au texte intégral et 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
-
2014
Article dans une revue
- titre
- Views of Pi: definition and computation
- auteur
- Yves Bertot, Guillaume Allais
- article
- Journal of Formalized Reasoning, 2014, 7 (1), pp.105-129. ⟨10.6092/issn.1972-5787/4343⟩
- Accès au texte intégral et 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
-
- titre
- Implementing Geometric Algebra Products with Binary Trees
- auteur
- Laurent Fuchs, Laurent Théry
- article
- Advances in Applied Clifford Algebras, 2014, 24 (1), pp.22. ⟨10.1007/s00006-014-0447-3⟩
- Accès au 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
-
- 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 – {CHES} 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
-
- 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
-
- 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
-
- 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
-
- 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
-
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
-
- 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
-
- titre
- Proving Tight Bounds on Univariate Expressions in Coq
- auteur
- Érik Martin-Dorel, Guillaume Melquiond
- article
- [Research Report] IRIT-RR-2014-09-FR, IRIT : Institut de Recherche Informatique de Toulouse. 2014, pp.1-32
- Accès au 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
-
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
-
2013
Article dans une revue
- titre
- Theorem of three circles in Coq
- auteur
- Julianna Zsidó
- article
- Journal of Automated Reasoning, 2013, ⟨10.1007/s10817-013-9299-0⟩
- Accès au bibtex
-
- titre
- Some issues related to double roundings
- auteur
- Érik Martin-Dorel, Guillaume Melquiond, Jean-Michel Muller
- article
- BIT Numerical Mathematics, 2013, 53 (4), pp.897-924. ⟨10.1007/s10543-013-0436-2⟩
- Accès au texte intégral et 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, 2013
- Accès au 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
-
- 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
-
- 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
-
- 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
-
- 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
-
- 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
-
- 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
-
- 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
-
- 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
-
Ouvrages
- 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
- The Univalent Foundations Program Institute for Advanced Study, pp.1–587, 2013
- Accès au 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
-
- 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
-
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
-
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, 2012, 2012 (91)
- Accès au 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
-
- titre
- Computer-Aided Cryptographic Proofs
- auteur
- Gilles Barthe, Juan Manuel Crespo, Benjamin Grégoire, Cesar Kunz, Santiago Zanella-Béguelin
- article
- ITP 2012 – Third International Conference on Interactive Theorem Proving, Aug 2012, Princeton N.J., United States. ⟨10.1007/978-3-642-32347-8_2⟩
- Accès au texte intégral et 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
-
- 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
-
- 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
-
- 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
-
- 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
-
- 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
-
Rapport
- titre
- Formalization and Concretization of Ordered Networks
- auteur
- Laurence Rideau, Bernard P. Serpette, Cédric Tedeschi
- article
- [Research Report] RR-8172, INRIA. 2012, pp.22
- Accès au texte intégral et 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. ⟨NNT : ⟩
- Accès au texte intégral et 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, 2011, 21 (04), pp.731-761. ⟨10.1017/S0960129511000090⟩
- Accès au texte intégral et 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
-
- 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
-
- 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
-
- 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
-
- 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
-
- 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
-
- 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
-
- 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 – {CRYPTO} 2011 – 31st Annual Cryptology Conference, 2011, Santa Barbara, United States. ⟨10.1007/978-3-642-22792-9_5⟩
- Accès au bibtex
-
- titre
- Preuves formelles automatiques et calcul formel
- auteur
- Loïc Pottier
- article
- Journées nationales de calcul formel, 2011, Luminy, France. pp.1-25, ⟨10.5802/ccirm.15⟩
- Accès au 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 – {CT-RSA} 2011 – The Cryptographers’ Track at the {RSA} 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
-
Chapitre d’ouvrage
- 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
-
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. ⟨NNT : ⟩
- Accès au texte intégral et bibtex
-
- titre
- On type-based termination and dependent pattern matching in the calculus of inductive constructions
- auteur
- Jorge Luis 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
-
2010
Communication dans un congrès
- titre
- On Strong Normalization of the Calculus of Constructions with Type-Based Termination
- auteur
- Benjamin Grégoire, Jorge Luis 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
-
- 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
-
- 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
-
- 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
-
- 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
-
- 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
-
- 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
-
- titre
- Similar Triangles and Orientation in Plane Elementary Geometry for Coq-based Proofs
- auteur
- Tuan Minh Pham
- article
- SAC 2010 – 25th ACM International Symposium on Applied Computing, Mar 2010, Sierre, Switzerland. ⟨10.1145/1774088.1774358⟩
- Accès au texte intégral et 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
-
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
-
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
-
- titre
- Formal Verifcation for Numerical Methods
- auteur
- Ioana Pasca
- article
- Other [cs.OH]. Université Nice Sophia Antipolis, 2010. English. ⟨NNT : ⟩
- Accès au texte intégral et 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. ⟨NNT : ⟩
- Accès au texte intégral et bibtex
-
2009
Article dans une revue
- titre
- Résoudre le Mini-Rubik’s Cube
- auteur
- Laurent Théry
- article
- Interstices, 2009
- Accès au 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
-
- 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
-
- 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
-
- 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
-
2008
Article dans une revue
- titre
- Tilting at windmills with Coq: formal verification of a compilation algorithm for parallel moves
- auteur
- Laurence Rideau, Bernard P. Serpette, Xavier Leroy
- article
- Journal of Automated Reasoning, 2008, 40 (4), pp.307-326. ⟨10.1007/s10817-007-9096-8⟩
- Accès au texte intégral et 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
-
- 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
-
- 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
-
- 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
-
- 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
-
- 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
-
- 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
-
- titre
- A New Elimination Rule for the Calculus of Inductive Constructions
- auteur
- Bruno Barras, Pierre Corbineau, Benjamin Grégoire, Hugo Herbelin, Jorge Luis 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
-
- 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
-
- 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
-
- 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
-
- 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
-
2007
Article dans une revue
- titre
- Implementing the cylindrical algebraic decomposition within the Coq system
- auteur
- Assia Mahboubi
- article
- Mathematical Structures in Computer Science, 2007, 17 (1), pp.99-127. ⟨10.1017/S096012950600586X⟩
- Accès au bibtex
-
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
-
- 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
-
Rapport
- 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
-
- 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
-
- 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
-
Pré-publication, Document de travail
- titre
- Battling windmills with Coq: formal verification of a compilation algorithm for parallel moves
- auteur
- Laurence Rideau, Bernard P. Serpette, Xavier Leroy
- article
- 2007
- Accès au texte intégral et 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, 2006, 17 (1), pp.37-63. ⟨10.1017/S0960129506005809⟩
- Accès au texte intégral et 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
-
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
-
Rapport
- titre
- Sudoku in Coq
- auteur
- Laurent Théry
- article
- [Research Report] INRIA Sophia Antipolis – Méditerranée. 2006
- Accès au texte intégral et 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
-
- titre
- Ambiguous Typing
- auteur
- Loïc Pottier
- article
- [Research Report] RR-6041, INRIA. 2006, pp.11
- Accès au texte intégral et bibtex
-
- 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
-
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. ⟨NNT : ⟩
- Accès au texte intégral et 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, 2005, Langages Applicatifs, Spécifications, Programmation, Vérification, 24 (9), pp.1161-1195
- Accès au texte intégral et bibtex
-
Communication dans un congrès
- titre
- Coq à la conquête des moulins
- auteur
- Laurence Rideau, Bernard P. Serpette
- article
- JFLA ‘2005, INRIA, Mar 2005, Obernai, pp.169-180
- Accès au texte intégral et 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
-
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
-
Ouvrages
- 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
-
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
-
