Publications

Publications HAL de Laurent,Théry; Yves Bertot; Benjamin Grégoire; Laurence Rideau; Cyril Cohen; Enrico Tassi du labo/EPI INRIA

2024

Conference papers

titre
Trocq: Proof Transfer for Free, With or Without Univalence
auteur
Cyril Cohen, Enzo Crance, Assia Mahboubi
article
ESOP 2024 – 33rd European Symposium on Programming, Apr 2024, Luxembourg, Luxembourg. pp.239-268
Accès au texte intégral et bibtex
https://hal.science/hal-04177913/file/main.pdf BibTex

Preprints, Working Papers, …

titre
Towards a correctly-rounded and fast power function in binary64 arithmetic
auteur
Tom Hubrecht, Claude-Pierre Jeannerod, Paul Zimmermann, Laurence Rideau, Laurent Théry
article
2024
Accès au texte intégral et bibtex
https://inria.hal.science/hal-04159652/file/pow.pdf BibTex

2023

Journal articles

titre
Measure Construction by Extension in Dependent Type Theory with Application to Integration
auteur
Reynald Affeldt, Cyril Cohen
article
Journal of Automated Reasoning, 2023, 67 (3), pp.28. ⟨10.1007/s10817-023-09671-5⟩
Accès au texte intégral et bibtex
https://inria.hal.science/hal-04183173/file/2209.02345.pdf BibTex
titre
Mechanized Proofs of Adversarial Complexity and Application to Universal Composability
auteur
Manuel Barbosa, Gilles Barthe, Benjamin Grégoire, Adrien Koutsos, Pierre-Yves Strub
article
ACM Transactions on Privacy and Security, 2023, 26 (3), pp.1-34. ⟨10.1145/3589962⟩
Accès au texte intégral et bibtex
https://inria.hal.science/hal-04048217/file/hal-preprint.pdf BibTex
titre
Accurate calculation of Euclidean Norms using Double-word arithmetic
auteur
Vincent Lefèvre, Nicolas Louvet, Jean-Michel Muller, Joris Picot, Laurence Rideau
article
ACM Transactions on Mathematical Software, 2023, 49 (1), pp.1-34. ⟨10.1145/3568672⟩
Accès au texte intégral et bibtex
https://hal.science/hal-03482567/file/NormsandDW%20HaLV2.pdf BibTex
titre
Prouvez que vos programmes fonctionnels n’ont pas de bugs avec Coq Première partie
auteur
Yves Bertot
article
Programmez !, 2023, 256, pp.35
Accès au texte intégral et bibtex
https://inria.hal.science/hal-04219914/file/short_article.pdf BibTex

Conference papers

titre
Formally verifying Kyber
auteur
José Bacelar Almeida, Manuel Barbosa, Gilles Barthe, Benjamin Grégoire, Vincent Laporte, Jean-Christophe Léchenet, Tiago Oliveira, Hugo Pacheco, Miguel Quaresma, Peter Schwabe, Antoine Séré, Pierre-Yves Strub
article
CHES 2023 – Conference on Cryptographic Hardware and Embedded Systems, IACR, Sep 2023, Praha, Czech Republic. pp.164-193, ⟨10.46586/tches.v2023.i3.164-193⟩
Accès au texte intégral et bibtex
https://inria.hal.science/hal-04218417/file/a.pdf BibTex
titre
Fixing and Mechanizing the Security Proof of Fiat-Shamir with Aborts and Dilithium
auteur
Manuel Barbosa, Gilles Barthe, Christian Doczkal, Jelle Don, Serge Fehr, Benjamin Grégoire, Yu-Hsuan Huang, Andreas Hülsing, Yi Lee, Xiaodi Wu
article
CRYPTO 2023 – 43rd International Cryptology Conference, Aug 2023, Santa Barbara, United States. pp.358-389, ⟨10.1007/978-3-031-38554-4_12⟩
Accès au texte intégral et bibtex
https://hal.science/hal-04315311/file/dilithium.pdf BibTex
titre
A new Type-Class solver for Coq in Elpi
auteur
Davide Fissore, Enrico Tassi
article
The Coq Workshop 2023, Jul 2023, Białystok, Poland
Accès au texte intégral et bibtex
https://inria.hal.science/hal-04467855/file/coq2023_TC-elpi.pdf BibTex
titre
Typing High-Speed Cryptography against Spectre v1
auteur
Basavesh Ammanaghatta Shivakumar, Gilles Barthe, Benjamin Grégoire, Vincent Laporte, Tiago Oliveira, Swarn Priya, Peter Schwabe, Lucas Tabary-Maujean
article
SP 2023- IEEE Symposium on Security and Privacy, IEEE, May 2023, San Francisco, United States. pp.1592-1609, ⟨10.1109/SP46215.2023.10179418⟩
Accès au texte intégral et bibtex
https://hal.science/hal-04106448/file/camera_ready.pdf BibTex
titre
Practical and sound equality tests, automatically — Deriving eqType instances for Jasmin’s data types with Coq-Elpi
auteur
Benjamin Grégoire, Jean-Christophe Léchenet, Enrico Tassi
article
CPP ’23: 12th ACM SIGPLAN International Conference on Certified Programs and Proofs, Jan 2023, Boston MA USA, France. pp.167-181, ⟨10.1145/3573105.3575683⟩
Accès au texte intégral et bibtex
https://inria.hal.science/hal-03800154/file/feqb.pdf BibTex
titre
Semantics of Probabilistic Programs using s-Finite Kernels in Coq
auteur
Reynald Affeldt, Cyril Cohen, Ayumu Saito
article
CPP 2023 – Certified Programs and Proofs, Jan 2023, Boston, United States. ⟨10.1145/3573105.3575691⟩
Accès au texte intégral et bibtex
https://inria.hal.science/hal-03917948/file/poplws23cppmain-p61-p-b400dabdc2-62273-submitted.pdf BibTex

Book sections

titre
Inductive Predicates
auteur
Yves Bertot, Lawrence C. Paulson
article
Jasmin Blanchette; Assia Mahboubi. Proof Assistants and Their Applications to Mathematics and Computer Science, 04, pp.37, In press
Accès au bibtex
BibTex

Proceedings

titre
Machine-Checked Security for XMSS as in RFC 8391 and SPHINCS +
auteur
Manuel Barbosa, François Dupressoir, Benjamin Grégoire, Andreas Hülsing, Matthias Meijers, Pierre-Yves Strub
article
2023, ⟨10.1007/978-3-031-38554-4\_14⟩
Accès au texte intégral et bibtex
https://hal.science/hal-04315335/file/sphincs.pdf BibTex

Reports

titre
Porting Coq Scripts to the Mathematical Components Library Version 2
auteur
Reynald Affeldt, Yves Bertot, Cyril Cohen, Pierre Roux, Kazuhiko Sakaguchi, Enrico Tassi
article
Inria Sophia Antipolis – Méditerranée, Université Côte d’Azur; National Institute of Advanced Industrial Science and Technology (AIST), Japan; ONERA / DTIS, Université de Toulouse, France. 2023, pp.1-12
Accès au texte intégral et bibtex
https://hal.science/hal-04225130/file/porting.pdf BibTex

Preprints, Working Papers, …

titre
CV2EC: Getting the Best of Both Worlds
auteur
Bruno Blanchet, Pierre Boutry, Christian Doczkal, Benjamin Grégoire, Pierre-Yves Strub
article
2023
Accès au texte intégral et bibtex
https://inria.hal.science/hal-04321656/file/main.pdf BibTex
titre
Safe smooth paths between straight line obstacles
auteur
Yves Bertot
article
2023
Accès au texte intégral et bibtex
https://inria.hal.science/hal-04312815/file/FHG_paper.pdf BibTex
titre
Design patterns of hierarchies for order structures
auteur
Xavier Allamigeon, Quentin Canu, Cyril Cohen, Kazuhiko Sakaguchi, Pierre-Yves Strub
article
2023
Accès au texte intégral et bibtex
https://inria.hal.science/hal-04008820/file/relorder.pdf BibTex

2022

Journal articles

titre
Formalization of double-word arithmetic, and comments on “Tight and rigorous error bounds for basic building blocks of double-word arithmetic
auteur
Jean-Michel Muller, Laurence Rideau
article
ACM Transactions on Mathematical Software, 2022, 48 (1), pp.1-24. ⟨10.1145/3484514⟩
Accès au texte intégral et bibtex
https://hal.science/hal-02972245/file/muller-rideau-hal.pdf BibTex

Conference papers

titre
Enforcing Fine-grained Constant-time Policies
auteur
Basavesh Ammanaghatta Shivakumar, Gilles Barthe, Benjamin Grégoire, Vincent Laporte, Swarn Priya
article
CCS 2022 – 2022 ACM SIGSAC Conference on Computer and Communications Security, Nov 2022, Los Angeles CA, United States. pp.83-96, ⟨10.1145/3548606.3560689⟩
Accès au bibtex
BibTex
titre
Reliably Reproducing Machine-Checked Proofs with the Coq Platform
auteur
Karl Palmskog, Enrico Tassi, Théo Zimmermann
article
RRRR 2022 – Workshop on Reproducibility and Replication of Research Results, Apr 2022, Munich, Germany
Accès au texte intégral et bibtex
https://inria.hal.science/hal-03592675/file/main.pdf BibTex

Preprints, Working Papers, …

titre
A Formalisation of a Fast Fourier Transform
auteur
Laurent Théry
article
2022
Accès au texte intégral et bibtex
https://inria.hal.science/hal-03807965/file/Note.pdf BibTex
titre
Primality Tests and Prime Certificate
auteur
Laurent Théry
article
2022
Accès au texte intégral et bibtex
https://inria.hal.science/hal-03601611/file/Note.pdf BibTex
titre
A Formalisation of Algorithms for Sorting Network
auteur
Laurent Théry
article
2022
Accès au texte intégral et bibtex
https://inria.hal.science/hal-03585618/file/Note.pdf BibTex

2021

Journal articles

titre
Computable analysis and notions of continuity in Coq
auteur
Florian Steinberg, Laurent Théry, Holger Thies
article
Logical Methods in Computer Science, 2021, 17 (2), ⟨10.23638/LMCS-17(2:16)2021⟩
Accès au bibtex
BibTex
titre
Masking in Fine-Grained Leakage Models: Construction, Implementation and Verification
auteur
Gilles Barthe, Marc Gourjon, Benjamin Grégoire, Maximilian Orlt, Clara Paglialonga, Lars Porth
article
IACR Transactions on Cryptographic Hardware and Embedded Systems, 2021, pp.189-228. ⟨10.46586/tches.v2021.i2.189-228⟩
Accès au texte intégral et bibtex
https://inria.hal.science/hal-03528937/file/main.pdf BibTex

Conference papers

titre
Structured Leakage and Applications to Cryptographic Constant-Time and Cost
auteur
Gilles Barthe, Benjamin Grégoire, Vincent Laporte, Swarn Priya
article
CCS 2021 – ACM SIGSAC Conference on Computer and Communications Security, Nov 2021, Virtual Event, South Korea. pp.462-476, ⟨10.1145/3460120.3484761⟩
Accès au bibtex
BibTex
titre
EasyPQC: Verifying Post-Quantum Cryptography
auteur
Manuel Barbosa, Gilles Barthe, Xiong Fan, Benjamin Grégoire, Shih-Han Hung, Jonathan Katz, Pierre-Yves Strub, Xiaodi Wu, Li Zhou
article
ACM CCS 2021 – ACM SIGSAC Conference on Computer and Communications Security, Nov 2021, Virtual Event, South Korea. pp.2564-2586, ⟨10.1145/3460120.3484567⟩
Accès au texte intégral et bibtex
https://inria.hal.science/hal-03529301/file/2021-1253.pdf BibTex
titre
Mechanized Proofs of Adversarial Complexity and Application to Universal Composability
auteur
Manuel Barbosa, Gilles Barthe, Benjamin Grégoire, Adrien Koutsos, Pierre-Yves Strub
article
CCS 2021 – ACM SIGSAC Conference on Computer and Communications Security, Nov 2021, Virtual Event, South Korea. pp.2541-2563, ⟨10.1145/3460120.3484548⟩
Accès au texte intégral et bibtex
https://hal.science/hal-03469015/file/eprint-main.pdf BibTex
titre
Porting the Mathematical Components library to Hierarchy Builder
auteur
Reynald Affeldt, Xavier Allamigeon, Yves Bertot, Quentin Canu, Cyril Cohen, Pierre Roux, Kazuhiko Sakaguchi, Enrico Tassi, Laurent Théry, Anton Trunov
article
the COQ Workshop 2021, Jul 2021, virtuel- Rome, Italy
Accès au texte intégral et bibtex
https://hal.science/hal-03463762/file/DTIS21240.pdf BibTex
titre
Proof Pearl : Playing with the Tower of Hanoi Formally
auteur
Laurent Théry
article
ITP 2021 – 12th International Conference on Interactive Theorem Proving, Jun 2021, Rome / Virtual, Italy. ⟨10.4230/LIPIcs.ITP.2021.31⟩
Accès au bibtex
BibTex
titre
Unsolvability of the Quintic Formalized in Dependent Type Theory
auteur
Sophie Bernard, Cyril Cohen, Assia Mahboubi, Pierre-Yves Strub
article
ITP 2021 – 12th International Conference on Interactive Theorem Proving, Jun 2021, Rome / Virtual, France
Accès au texte intégral et bibtex
https://inria.hal.science/hal-03136002/file/main.pdf BibTex
titre
High-Assurance Cryptography in the Spectre Era
auteur
Gilles Barthe, Sunjay Cauligi, Benjamin Grégoire, Adrien Koutsos, Kevin Liao, Tiago Oliveira, Swarn Priya, Tamara Rezk, Peter Schwabe
article
S&P 2021 – IEEE Symposium of Security and Privacy, May 2021, Virtual, France. ⟨10.1109/SP40001.2021.00046⟩
Accès au texte intégral et bibtex
https://inria.hal.science/hal-03352062/file/highassurance.pdf BibTex

Documents associated with scientific events

titre
A Nix toolbox for reproducible Coq environments, Continuous Integration and artifact reuse
auteur
Cyril Cohen, Théo Zimmermann
article
The Coq Workshop, Jul 2021, Virtual, France
Accès au texte intégral et bibtex
https://inria.hal.science/hal-03366644/file/main.pdf BibTex

Preprints, Working Papers, …

titre
Formalization of a sign determination algorithm in real algebraic geometry
auteur
Cyril Cohen
article
2021
Accès au texte intégral et bibtex
https://inria.hal.science/hal-03274013/file/main.pdf BibTex

2020

Journal articles

titre
C-language floating-point proofs layered with VST and Flocq
auteur
Andrew W. Appel, Yves Bertot
article
Journal of Formalized Reasoning, 2020, 13 (1), pp.1-16. ⟨10.6092/issn.1972-5787/11442⟩
Accès au texte intégral et bibtex
https://inria.hal.science/hal-03130704/file/paper_v2.pdf BibTex
titre
Hardware Private Circuits: From Trivial Composition to Full Verification
auteur
Gaetan Cassiers, Benjamin Grégoire, Itamar Levi, Francois-Xavier Standaert
article
IEEE Transactions on Computers, 2020, ⟨10.1109/tc.2020.3022979⟩
Accès au texte intégral et bibtex
https://inria.hal.science/hal-03133227/file/185.pdf BibTex
titre
Improved parallel mask refreshing algorithms: generic solutions with parametrized non-interference and automated optimizations
auteur
Gilles Barthe, Sonia Belaïd, François Dupressoir, Pierre-Alain Fouque, Benjamin Grégoire, François-Xavier Standaert, Pierre-Yves Strub
article
Journal of Cryptographic Engineering, 2020, 10 (1), pp.17-26. ⟨10.1007/s13389-018-00202-2⟩
Accès au texte intégral et bibtex
https://inria.hal.science/hal-03133221/file/505.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
Journal of Automated Reasoning, 2020, ⟨10.1007/s10817-019-09540-0⟩
Accès au texte intégral et bibtex
https://inria.hal.science/hal-02167423/file/The_MetaCoq_Project.pdf BibTex
titre
Formal verification of a constant-time preserving C compiler
auteur
Gilles Barthe, Sandrine Blazy, Benjamin Grégoire, Rémi Hutin, Vincent Laporte, David Pichardie, Alix Trieu
article
Proceedings of the ACM on Programming Languages, 2020, 4 (POPL), pp.1-30. ⟨10.1145/3371075⟩
Accès au texte intégral et bibtex
https://hal.univ-lorraine.fr/hal-02975012/file/Barthe-2020-Formal%20verification%20of%20a%20constant-time%20preserving%20C%20compiler.pdf BibTex

Conference papers

titre
Security Analysis of ElGamal Implementations
auteur
Mohamad El Laz, Benjamin Grégoire, Tamara Rezk
article
SECRYPT 2020 – 17th International Conference on Security and Cryptography, Jul 2020, Lieusaint – Paris, France. pp.310-321, ⟨10.5220/0009817103100321⟩
Accès au texte intégral et bibtex
https://inria.hal.science/hal-03141511/file/SecryptElGamal.pdf BibTex
titre
Competing inheritance paths in dependent type theory: a case study in functional analysis
auteur
Reynald Affeldt, Cyril Cohen, Marie Kerjean, Assia Mahboubi, Damien Rouhling, Kazuhiko Sakaguchi
article
IJCAR 2020 – International Joint Conference on Automated Reasoning, Jun 2020, Paris, France. pp.1-19
Accès au texte intégral et bibtex
https://inria.hal.science/hal-02463336/file/ijcar%20%281%29.pdf BibTex
titre
Hierarchy Builder: algebraic hierarchies made easy in Coq with Elpi
auteur
Cyril Cohen, Kazuhiko Sakaguchi, Enrico Tassi
article
FSCD 2020 – 5th International Conference on Formal Structures for Computation and Deduction, Jun 2020, Paris, France. pp.34:1–34:21, ⟨10.4230/LIPIcs.FSCD.2020.34⟩
Accès au texte intégral et bibtex
https://inria.hal.science/hal-02478907/file/LIPIcs-FSCD-2020-34.pdf BibTex
titre
Private types in Higher Order Logic Programming
auteur
Marco Maggesi, Enrico Tassi
article
TEASE-LP 2020 – Workshop on Trends, Extensions, Applications and Semantics of Logic Programming, May 2020, Virtual Event, France
Accès au texte intégral et bibtex
https://inria.hal.science/hal-03117762/file/privtypes.pdf BibTex
titre
The Last Mile: High-Assurance and High-Speed Cryptographic Implementations
auteur
José Bacelar Almeida, Manuel Barbosa, Gilles Barthe, Benjamin Grégoire, Adrien Koutsos, Vincent Laporte, Tiago Oliveira, Pierre-Yves Strub
article
SP 2020 – 41st IEEE Symposium on Security and Privacy, May 2020, San Francisco / Virtual, United States. pp.965-982, ⟨10.1109/SP40000.2020.00028⟩
Accès au bibtex
https://arxiv.org/pdf/1904.04606 BibTex

Other publications

titre
Requirements on the Use of Coq in the Context of Common Criteria Evaluations
auteur
Yves Bertot, Maxime Dénès, Arnaud Fontaine, Vincent Laporte, Thomas Letan
article
2020, pp.20
Accès au texte intégral et bibtex
https://inria.hal.science/hal-04452421/file/coq.pdf BibTex

Preprints, Working Papers, …

titre
Playing with the Tower of Hanoi Formally
auteur
Laurent Théry
article
2020
Accès au texte intégral et bibtex
https://inria.hal.science/hal-02903548/file/Note.pdf BibTex

2019

Journal articles

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
https://inria.hal.science/hal-01410567/file/dalefest.pdf BibTex

Conference papers

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
https://hal.science/hal-02404540/file/main.pdf 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
https://hal.science/hal-02404581/file/sketch.pdf BibTex
titre
MaskVerif: 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 The European Symposium on Research in Computer Security, Sep 2019, Luxembourg, Luxembourg. pp.300-318
Accès au bibtex
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
https://hal.science/hal-02404662/file/main.pdf 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
https://inria.hal.science/hal-01897468/file/induction.pdf 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
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://inria.hal.science/hal-02303987/file/LIPIcs-ITP-2019-13.pdf 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
https://hal.science/hal-02404701/file/paper.pdf 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
https://hal.science/hal-02404755/file/main.pdf BibTex

Preprints, Working Papers, …

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
https://inria.hal.science/hal-02088293/file/paper.pdf BibTex

2018

Journal articles

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
https://inria.hal.science/hal-01719918/file/8124-27375-1-PB.pdf 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
https://inria.hal.science/hal-01582524/file/main.pdf BibTex

Conference papers

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://inria.hal.science/hal-01866271/file/main.pdf 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
https://hal.science/hal-01959391/file/paper.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.science/hal-01809681/file/paper_39.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.science/hal-01959560/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.science/hal-01959554/file/main.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://inria.hal.science/hal-01900708/file/2018-381.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.science/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
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
https://hal.science/hal-01959567/file/main.pdf 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
https://inria.hal.science/hal-01637063/file/coqpl2018.pdf BibTex

Software

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
https://inria.hal.science/hal-01767263/file/pi-agm-1.0.0.zip BibTex

Preprints, Working Papers, …

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://inria.hal.science/hal-01906155/file/paper.pdf BibTex

2017

Journal articles

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
https://hal.science/hal-01959322/file/bounded.pdf 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
https://inria.hal.science/hal-01410450/file/main-sttt.pdf BibTex

Conference papers

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
https://hal.science/hal-01649104/file/jasmin.pdf 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
https://hal.science/hal-01649140/file/main.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://inria.hal.science/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.science/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
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
https://inria.hal.science/hal-01414009/file/parallel_masking_4.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.science/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://inria.hal.science/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://inria.hal.science/hal-01414881/file/cyrilcohen.pdf BibTex

Preprints, Working Papers, …

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.science/hal-01446070/file/Note.pdf BibTex

2016

Journal articles

titre
Formalized Linear Algebra over Elementary Divisor Rings in Coq
auteur
Guillaume Cano, Cyril Cohen, Maxime Dénès, Anders Mörtberg, Vincent Siles
article
Logical Methods in Computer Science, 2016, ⟨10.2168/LMCS-12(2:7)2016⟩
Accès au texte intégral et bibtex
https://inria.hal.science/hal-01081908/file/main.author.pdf BibTex

Conference papers

titre
Strong Non-Interference and Type-Directed Higher-Order Masking
auteur
Gilles Barthe, Sonia Belaïd, François Dupressoir, Pierre-Alain Fouque, Benjamin Grégoire, Pierre-Yves Strub, Rébecca Zucchini
article
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://inria.hal.science/hal-01410216/file/main.pdf BibTex
titre
Advanced Probabilistic Couplings for Differential Privacy
auteur
Gilles Barthe, Noémie Fong, Marco Gaboardi, Benjamin Grégoire, Justin Hsu, Pierre-Yves Strub
article
23rd ACM Conference on Computer and Communications Security , Oct 2016, Vienne, Austria. pp.55 – 67, ⟨10.1145/2976749.2978391⟩
Accès au texte intégral et bibtex
https://inria.hal.science/hal-01410196/file/main.pdf BibTex
titre
The Littlun S-box and the Fly block cipher
auteur
Pierre Karpman, Benjamin Grégoire
article
Lightweight Cryptography Workshop, Oct 2016, Gaithersburg, United States
Accès au texte intégral et bibtex
https://hal.science/hal-03543497/file/littlun.pdf 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
https://inria.hal.science/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://inria.hal.science/hal-01411095/file/icalp16-212.pdf BibTex
titre
Proving Differential Privacy via Probabilistic Couplings
auteur
Gilles Barthe, Marco Gaboardi, Benjamin Grégoire, Justin Hsu, Pierre-Yves Strub
article
Thirty-First Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), Jul 2016, New York, United States. pp.749 – 758, ⟨10.1145/2933575.2934554⟩
Accès au texte intégral et bibtex
https://inria.hal.science/hal-01411097/file/main.pdf BibTex
titre
Implementing HOL in an Higher Order Logic Programming Language
auteur
Cvetan Dunchev, Claudio Sacerdoti Coen, Enrico Tassi
article
Logical Frameworks and Meta Languages: Theory and Practice, Jun 2016, Porto, Portugal. pp.10, ⟨10.1145/2966268.2966272⟩
Accès au texte intégral et bibtex
https://inria.hal.science/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://inria.hal.science/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://inria.hal.science/hal-01240469/file/main.pdf BibTex

Lectures

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

Reports

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://inria.hal.science/inria-00258384/file/main.pdf BibTex

2015

Journal articles

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

Conference papers

titre
ELPI: fast, Embeddable, λProlog Interpreter
auteur
Cvetan Dunchev, Ferruccio Guidi, Claudio Sacerdoti Coen, Enrico Tassi
article
Proceedings of LPAR, Nov 2015, Suva, Fiji
Accès au texte intégral et bibtex
https://inria.hal.science/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 {ACM} {SIGSAC} 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://inria.hal.science/hal-01135919/file/full.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://inria.hal.science/hal-01378906/file/LIPIcs-TYPES-2015-5.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://inria.hal.science/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.science/hal-01246719/file/Couplings.pdf BibTex

Lectures

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

Preprints, Working Papers, …

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

2014

Journal articles

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, 2014, 7 (1), pp.105-129. ⟨10.6092/issn.1972-5787/4343⟩
Accès au texte intégral et bibtex
https://inria.hal.science/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, 2014, 24 (1), pp.22. ⟨10.1007/s00006-014-0447-3⟩
Accès au bibtex
BibTex

Conference papers

titre
Synthesis of Fault Attacks on Cryptographic Implementations
auteur
Gilles Barthe, François Dupressoir, Pierre-Alain Fouque, Benjamin Grégoire, Jean-Christophe Zapalowicz
article
ACM CCS 2014, Nov 2014, Scottsdale, United States. pp.16, ⟨10.1145/2660267.2660304⟩
Accès au texte intégral et bibtex
https://inria.hal.science/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 – {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
https://inria.hal.science/hal-01094057/file/FaultRSA.pdf BibTex
titre
Certified Synthesis of Efficient Batch Verifiers
auteur
Joseph A. Akinyele, Gilles Barthe, Benjamin Grégoire, Benedikt Schmidt, Pierre-Yves Strub
article
CSF 2014 – IEEE 27th Computer Security Foundations Symposium, Jul 2014, Vienna, Austria. pp.153 – 165, ⟨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://inria.hal.science/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
titre
A Computer-Algebra-Based Formal Proof of the Irrationality of ζ(3)
auteur
Frédéric Chyzak, Assia Mahboubi, Thomas Sibut-Pinote, Enrico Tassi
article
ITP – 5th International Conference on Interactive Theorem Proving, 2014, Vienna, Austria
Accès au texte intégral et bibtex
https://inria.hal.science/hal-00984057/file/main.pdf BibTex

Reports

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

Preprints, Working Papers, …

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

2013

Journal articles

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
BibTex
titre
A constructive version of Laplace’s proof on the existence of complex roots
auteur
Cyril Cohen, Thierry Coquand
article
Journal of Algebra, 2013, 381, pp.110-115. ⟨10.1016/j.jalgebra.2013.01.016⟩
Accès au texte intégral et bibtex
https://inria.hal.science/inria-00592284/file/laplace1.pdf BibTex

Conference papers

titre
Refinements for Free!
auteur
Cyril Cohen, Maxime Dénès, Anders Mörtberg
article
Certified Programs and Proofs, Dec 2013, Melbourne, Australia. pp.147 – 162, ⟨10.1007/978-3-319-03545-1_10⟩
Accès au texte intégral et bibtex
https://inria.hal.science/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://inria.hal.science/hal-00845791/file/CoqApprox2013_HAL_v2.pdf BibTex
titre
Canonical Structures for the working Coq user
auteur
Assia Mahboubi, Enrico Tassi
article
ITP 2013, 4th Conference on Interactive Theorem Proving, Jul 2013, Rennes, France. pp.19-34, ⟨10.1007/978-3-642-39634-2_5⟩
Accès au texte intégral et bibtex
https://inria.hal.science/hal-00816703/file/main.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://inria.hal.science/hal-01966714/file/main.pdf 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://inria.hal.science/hal-00816699/file/main.pdf BibTex
titre
Pervasive Parallelism in Highly-Trustable Interactive Theorem Proving Systems
auteur
Bruno Barras, Lourdes del Carmen Gonzalez Huesca, Hugo Herbelin, Yann Régis-Gianas, Enrico Tassi, Makarius Wenzel, Burkhart Wolff
article
MKM/Calculemus/DML, Jul 2013, Bath, United Kingdom. pp.359-363
Accès au bibtex
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
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

Books

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

2012

Journal articles

titre
Formal proofs in real algebraic geometry: from ordered fields to quantifier elimination
auteur
Cyril Cohen, Assia Mahboubi
article
Logical Methods in Computer Science, 2012, 8 (1:02), pp.1-40. ⟨10.2168/LMCS-8(1:02)2012⟩
Accès au texte intégral et bibtex
https://inria.hal.science/inria-00593738/file/1201.3731.pdf BibTex
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
BibTex

Conference papers

titre
Computer-Aided Cryptographic Proofs
auteur
Gilles Barthe, Benjamin Grégoire, Santiago Zanella-Béguelin
article
Static Analysis – 19th International Symposium, SAS 2012, Sep 2012, Deauville, France. ⟨10.1007/978-3-642-33125-1_1⟩
Accès au texte intégral et bibtex
https://inria.hal.science/hal-00765869/file/main.pdf BibTex
titre
A language of patterns for subterm selection
auteur
Georges Gonthier, Enrico Tassi
article
ITP, Aug 2012, Princeton, United States. pp.361-376, ⟨10.1007/978-3-642-32347-8_25⟩
Accès au texte intégral et bibtex
https://inria.hal.science/hal-00652286/file/rew.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 – 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
https://inria.hal.science/hal-00765842/file/main.pdf BibTex
titre
Construction of real algebraic numbers in Coq
auteur
Cyril Cohen
article
ITP – 3rd International Conference on Interactive Theorem Proving – 2012, Aug 2012, Princeton, United States
Accès au texte intégral et bibtex
https://inria.hal.science/hal-00671809/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://inria.hal.science/hal-00765864/file/main.pdf BibTex
titre
Verified Security of Merkle-Damgaard
auteur
Michael Backes, Gilles Barthe, Matthias Berg, Benjamin Grégoire, Cesar Kunz, Malte Skoruppa, Santiago Zanella-Béguelin
article
25th IEEE Computer Security Foundations Symposium, CSF 2012, Jun 2012, Cambridge, MA, United States. pp.354-368, ⟨10.1109/CSF.2012.14⟩
Accès au texte intégral et bibtex
https://inria.hal.science/hal-00765883/file/main.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://ens-lyon.hal.science/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://inria.hal.science/hal-00765874/file/main.pdf BibTex
titre
Construction des nombres algébriques réels en Coq
auteur
Cyril Cohen
article
JFLA – Journées Francophones des Langages Applicatifs – 2012, Feb 2012, Carnac, France
Accès au texte intégral et bibtex
https://inria.hal.science/hal-00665965/file/paper_11.pdf BibTex

Reports

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
https://inria.hal.science/hal-00762627/file/RR-8172.pdf BibTex

Theses

titre
Formalized algebraic numbers: construction and first-order theory.
auteur
Cyril Cohen
article
Logic in Computer Science [cs.LO]. Ecole Polytechnique X, 2012. English. ⟨NNT : ⟩
Accès au texte intégral et bibtex
https://pastel.hal.science/pastel-00780446/file/main.pdf BibTex

2011

Journal articles

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

Conference papers

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://inria.hal.science/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://inria.hal.science/hal-00639130/file/cpp11.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://inria.hal.science/inria-00614041/file/ArmandAl.pdf BibTex
titre
A Flexible Proof Format for SMT: a Proposal
auteur
Frédéric Besson, Pascal Fontaine, Laurent Théry
article
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://inria.hal.science/hal-00642544/file/paper3.pdf BibTex
titre
Incidence simplicial matrices formalized in Coq/SSReflect
auteur
Jónathan Heras, María Poza, Maxime Denes, Laurence Rideau
article
Conference on Intelligent Computer Mathematics, Jul 2011, Bertinoro, Italy. ⟨10.1007/978-3-642-22673-1_3⟩
Accès au texte intégral et bibtex
https://inria.hal.science/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://inria.hal.science/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 – {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
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
BibTex

Book sections

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

2010

Conference papers

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
https://hal.science/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.science/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://inria.hal.science/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://inria.hal.science/inria-00502496/file/fastcoq.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://inria.hal.science/inria-00504027/file/Del-ITP10.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://inria.hal.science/inria-00585400/file/paper8.pdf BibTex
titre
A formal quantifier elimination for algebraically closed fields
auteur
Cyril Cohen, Assia Mahboubi
article
Symposium on the Integration of Symbolic Computation and Mechanised Reasoning, Calculemus, Jul 2010, Paris, France. pp.189-203, ⟨10.1007/978-3-642-14128-7_17⟩
Accès au texte intégral et bibtex
https://inria.hal.science/inria-00464237/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://inria.hal.science/inria-00552894/file/itp10.pdf BibTex

Preprints, Working Papers, …

titre
Formalizing real analysis for polynomials
auteur
Cyril Cohen
article
2010
Accès au texte intégral et bibtex
https://inria.hal.science/inria-00545778/file/main.pdf BibTex

2009

Journal articles

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

Conference papers

titre
Formal proof of theorems on genetic regulatory networks
auteur
Maxime Dénès, Benjamin Lesage, Yves Bertot, Adrien Richard
article
SYNASC’09, Sep 2009, Timisoara, Romania
Accès au bibtex
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://inria.hal.science/inria-00368403/file/main.pdf BibTex

2008

Journal articles

titre
Tilting at windmills with Coq: formal verification of a compilation algorithm for parallel moves
auteur
Laurence Rideau, Bernard 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
https://inria.hal.science/inria-00289709/file/parallel-move.pdf BibTex

Conference papers

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://inria.hal.science/inria-00504719/file/pottier.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://inria.hal.science/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://inria.hal.science/inria-00190975/file/ppdp19-bertot.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://inria.hal.science/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 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
https://inria.hal.science/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://inria.hal.science/inria-00329572/file/absint.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://inria.hal.science/inria-00322331/file/fibonacci.pdf BibTex

2007

Conference papers

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://inria.hal.science/inria-00138382/file/paper.pdf BibTex

Reports

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://inria.hal.science/inria-00129237/file/RT-0330.pdf 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
https://inria.hal.science/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://inria.hal.science/inria-00160309/file/RR-6242.pdf BibTex

Preprints, Working Papers, …

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

2006

Journal articles

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

Conference papers

titre
Calcul de formules affines et de séries entières en arithmétique exacte avec types co-inductifs
auteur
Yves Bertot
article
Journées Francophones des Langages Applicatifs, INRIA, Jan 2006, Pauillac, pp.41-55
Accès au texte intégral et bibtex
https://inria.hal.science/inria-00000480/file/exactreals.pdf BibTex

Lectures

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

Reports

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
https://inria.hal.science/hal-03277886/file/Note.pdf 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
https://inria.hal.science/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://inria.hal.science/inria-00113750/file/RT-0327.pdf BibTex

2005

Journal articles

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

Conference papers

titre
Proving Equalities in a Commutative Ring Done Right in Coq
auteur
Benjamin Gregoire, Assia Mahboubi
article
TPHOLs 2005, Aug 2005, Oxford, United Kingdom. pp.98-113, ⟨10.1007/11541868_7⟩
Accès au bibtex
BibTex
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
https://inria.hal.science/inria-00001128/file/RideauSerpetteJFLA05.pdf BibTex

Lectures

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

Reports

titre
Simplifying Polynomial Expressions in a Proof Assistant
auteur
Laurent Théry
article
[Research Report] RR-5614, INRIA. 2005, pp.16
Accès au texte intégral et bibtex
https://inria.hal.science/inria-00070394/file/RR-5614.pdf BibTex

2004

Conference papers

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

Books

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

Reports

titre
Vérification formelle d’extractions de racines
auteur
Yves Bertot
article
RR-5344, INRIA. 2004, pp.23
Accès au texte intégral et bibtex
https://inria.hal.science/inria-00070657/file/RR-5344.pdf BibTex
titre
Filters on Co-Inductive streams: an application to Eratosthenes’ sieve
auteur
Yves Bertot
article
RR-5343, INRIA. 2004, pp.21
Accès au texte intégral et bibtex
https://inria.hal.science/inria-00070658/file/RR-5343.pdf BibTex
titre
Proof by reflection in semantics
auteur
Kuntal das Barman, Yves Bertot
article
RR-5134, INRIA. 2004
Accès au texte intégral et bibtex
https://inria.hal.science/inria-00071449/file/RR-5134.pdf BibTex

2003

Reports

titre
QArith: Coq Formalisation of Lazy Rational Arithmetic
auteur
Milad Niqui, Yves Bertot
article
[Research Report] RR-5004, INRIA. 2003, pp.19
Accès au texte intégral et bibtex
https://inria.hal.science/inria-00077041/file/RR-5004.pdf BibTex
titre
A Table-Driven Compiler for Pretty Printing Specifications
auteur
Laurent Théry
article
[Technical Report] RT-0288, INRIA. 2003, pp.31
Accès au texte intégral et bibtex
https://inria.hal.science/inria-00069891/file/RT-0288.pdf BibTex

2002

Journal articles

titre
Interactive layout and handling of mathematical formulas in structured documents
auteur
Hanane Naciri, Laurence Rideau
article
Revue Africaine de Recherche en Informatique et Mathématiques Appliquées, 2002, Volume 1, 2002, pp.95-125. ⟨10.46298/arima.1832⟩
Accès au texte intégral et bibtex
https://inria.hal.science/hal-01261698/file/arima00105.pdf BibTex
titre
A Proof of GMP Square Root
auteur
Yves Bertot, Nicolas Magaud, Paul Zimmermann
article
Journal of Automated Reasoning, 2002, 29 (3-4), pp.225–252. ⟨10.1023/A:1021987403425⟩
Accès au bibtex
BibTex

Conference papers

titre
A Compiled Implementation of Strong Reduction
auteur
Benjamin Grégoire, Xavier Leroy
article
ICFP ’02: seventh ACM SIGPLAN international conference on Functional programming , ACM, Oct 2002, Pittsburgh, United States. pp.235-246, ⟨10.1145/581478.581501⟩
Accès au texte intégral et bibtex
https://inria.hal.science/hal-01499941/file/strong-reduction.pdf BibTex

Reports

titre
A Tour of Formal Verification with Coq:Knuth’s Algorithm for Prime Numbers
auteur
Laurent Théry
article
RR-4600, INRIA. 2002
Accès au texte intégral et bibtex
https://inria.hal.science/inria-00071985/file/RR-4600.pdf BibTex
titre
Stålmarck’s Algorithm in Coq: A Three-Level Approach
auteur
Laurent Théry
article
RR-4353, INRIA. 2002
Accès au texte intégral et bibtex
https://inria.hal.science/inria-00072235/file/RR-4353.pdf BibTex
titre
A proof of GMP square root using the Coq assistant
auteur
Yves Bertot, Nicolas Magaud, Paul Zimmermann
article
[Research Report] RR-4475, INRIA. 2002
Accès au texte intégral et bibtex
https://inria.hal.science/inria-00072113/file/RR-4475.pdf BibTex

2001

Conference papers

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://inria.hal.science/hal-01702679/file/hulls.pdf BibTex
titre
A Generic Library for Floating-Point Numbers and Its Application to Exact Computing
auteur
Marc Daumas, Laurence Rideau, Laurent Thery
article
Theorem Proving in Higher Order Logics, 2001, Edinburgh, United Kingdom. pp.169-184
Accès au texte intégral et bibtex
https://hal.science/hal-00157285/file/DauRidThe01.pdf BibTex

Reports

titre
Mathematics and Proof Presentation in Pcoq
auteur
Ahmed Amerkad, Yves Bertot, Loïc Pottier, Laurence Rideau
article
RR-4313, INRIA. 2001
Accès au texte intégral et bibtex
https://inria.hal.science/inria-00072274/file/RR-4313.pdf BibTex
titre
Affichage et manipulation interactive de formules mathématiques dans les documents structurés
auteur
Hanane Naciri, Laurence Rideau
article
RR-4140, INRIA. 2001
Accès au texte intégral et bibtex
https://inria.hal.science/inria-00072486/file/RR-4140.pdf BibTex
titre
Computer Validated Proofs of a Toolset for Adaptable Arithmetic
auteur
Marc Daumas, Claire Moreau-Finot, Laurent Théry
article
[Research Report] RR-4095, LIP RR2001-01, INRIA, LIP. 2001
Accès au texte intégral et bibtex
https://inria.hal.science/inria-00072536/file/RR-4095.pdf BibTex

Preprints, Working Papers, …

titre
Computer validated proofs of a toolset for adaptable arithmetic
auteur
Sylvie Boldo, Marc Daumas, Claire Moreau-Finot, Laurent Thery
article
2001
Accès au bibtex
https://arxiv.org/pdf/cs.MS/0107025 BibTex

2000

Conference papers

titre
A distributed editing environment for XML documents
auteur
Claude Pasquier, Laurent Théry
article
1st ECOOP Workshop on XML and Object Technology, Jun 2000, Sophia Antipolis, France
Accès au texte intégral et bibtex
https://hal.science/hal-00362451/file/paper.pdf BibTex
titre
Formalizing Stalmarck’s algorithm in Coq
auteur
Pierre Letouzey, Laurent Théry
article
Theorem Proving in Higher Order Logics, 13th International Conference, TPHOLs 2000, 2000, Portland, United States. pp.388
Accès au texte intégral et bibtex
https://hal.science/hal-00150915/file/stalmark.pdf BibTex

Reports

titre
Graphes de dépendance pour les démonstrateurs de théorèmes intéractifs
auteur
Yves Bertot, Olivier Pons, Loïc Pottier
article
RR-4052, INRIA. 2000
Accès au texte intégral et bibtex
https://inria.hal.science/inria-00072585/file/RR-4052.pdf BibTex
titre
Changements de représentation des données dans le calcul des constructions inductives
auteur
Nicolas Magaud, Yves Bertot
article
[Rapport de recherche] RR-4039, INRIA. 2000, pp.29
Accès au texte intégral et bibtex
https://inria.hal.science/inria-00072599/file/RR-4039.pdf BibTex
titre
A Coq Formalization of a Type Checker for Object Initialization in the Java Virtual Machine
auteur
Yves Bertot
article
[Research Report] RR-4047, INRIA. 2000, pp.53
Accès au texte intégral et bibtex
https://inria.hal.science/inria-00072591/file/RR-4047.pdf BibTex

1998

Reports

titre
The CtCoq System: Design and Architecture
auteur
Yves Bertot
article
RR-3540, INRIA. 1998
Accès au texte intégral et bibtex
https://inria.hal.science/inria-00073145/file/RR-3540.pdf BibTex
titre
A certified Compiler for an Imperative Language
auteur
Yves Bertot
article
RR-3488, INRIA. 1998
Accès au texte intégral et bibtex
https://inria.hal.science/inria-00073199/file/RR-3488.pdf BibTex

1997

Reports

titre
Proving and Computing: a Certified Version of the Buchberger’s Algorithm
auteur
Laurent Théry
article
RR-3275, INRIA. 1997
Accès au texte intégral et bibtex
https://inria.hal.science/inria-00073414/file/RR-3275.pdf BibTex
titre
Implementing Proof by Pointing without a Structure Editor
auteur
Yves Bertot, Thomas Kleymann-Schreiber, Dilip Sequeira
article
RR-3286, INRIA. 1997
Accès au texte intégral et bibtex
https://inria.hal.science/inria-00073402/file/RR-3286.pdf BibTex
titre
Interactive Programming Environment for ML
auteur
Laurence Rideau, Laurent Théry
article
RR-3139, INRIA. 1997
Accès au texte intégral et bibtex
https://inria.hal.science/inria-00073550/file/RR-3139.pdf BibTex
titre
Programming Language Specifications and Environments
auteur
Yves Bertot
article
[Technical Report] RT-0212, INRIA. 1997, pp.47
Accès au texte intégral et bibtex
https://inria.hal.science/inria-00069959/file/RT-0212.pdf BibTex
titre
User Guide to the CTCOQ Proof Environment
auteur
Janet Bertot, Yves Bertot, Yann Coscoy, Healfdene Goguen, Francis Montagnac
article
[Technical Report] RT-0210, INRIA. 1997, pp.63
Accès au texte intégral et bibtex
https://inria.hal.science/inria-00069961/file/RT-0210.pdf BibTex

1996

Reports

titre
Distributed Architecture for Programming Environments
auteur
Anne-Marie Dery, Laurence Rideau
article
RR-2918, INRIA. 1996
Accès au texte intégral et bibtex
https://inria.hal.science/inria-00073779/file/RR-2918.pdf BibTex
titre
Interactive Theorem Proving with Temporal Logic
auteur
Amy Felty, Laurent Théry
article
RR-2804, INRIA. 1996
Accès au texte intégral et bibtex
https://inria.hal.science/inria-00073886/file/RR-2804.pdf BibTex
titre
Reasoning with Executable Specifications
auteur
Yves Bertot, Ranan Fraer
article
RR-2780, INRIA. 1996
Accès au texte intégral et bibtex
https://inria.hal.science/inria-00073912/file/RR-2780.pdf BibTex

1995

Reports

titre
Extracting Text from Proofs
auteur
Yann Coscoy, Gilles Kahn, Laurent Thery
article
RR-2459, INRIA. 1995
Accès au texte intégral et bibtex
https://inria.hal.science/inria-00074217/file/RR-2459.pdf BibTex

1994

Reports

titre
Distributed programming environments: an example of a message protocol
auteur
Anne-Marie Dery, Laurence Rideau
article
[Research Report] RT-0165, INRIA. 1994, pp.24
Accès au texte intégral et bibtex
https://inria.hal.science/inria-00070004/file/RT-0165.pdf BibTex

1993

Reports

titre
Proof by pointing
auteur
Yves Bertot, Gilles Kahn, Laurent Théry
article
University of Cambridge. 1993
Accès au texte intégral et bibtex
https://inria.hal.science/hal-03957702/file/UCAM-CL-TR-313.pdf BibTex

1992

Reports

titre
Real theorem provers deserve real user-interfaces
auteur
Laurent Théry, Yves Bertot, Gilles Kahn
article
[Research Report] RR-1684, INRIA. 1992
Accès au texte intégral et bibtex
https://inria.hal.science/inria-00076907/file/RR-1684.pdf BibTex

1991

Reports

titre
The Origins of lambda-calculus and term rewriting systems
auteur
Yves Bertot
article
[Research Report] RR-1543, INRIA. 1991, pp.19
Accès au texte intégral et bibtex
https://inria.hal.science/inria-00075019/file/RR-1543.pdf BibTex
titre
A Canonical calculus of residuals
auteur
Yves Bertot
article
[Research Report] RR-1542, INRIA. 1991, pp.12
Accès au texte intégral et bibtex
https://inria.hal.science/inria-00075020/file/RR-1542.pdf BibTex

1990

Reports

titre
Occurences in debugger specifications
auteur
Yves Bertot
article
[Research Report] RR-1350, INRIA. 1990, pp.13
Accès au texte intégral et bibtex
https://inria.hal.science/inria-00075209/file/RR-1350.pdf BibTex

1989

Reports

titre
Implementation of an interpreter for a parallel language in CENTAUR
auteur
Yves Bertot
article
[Research Report] RR-1076, INRIA. 1989, pp.27
Accès au texte intégral et bibtex
https://inria.hal.science/inria-00075483/file/RR-1076.pdf BibTex

 

Comments are closed.