2024
Conference papers
- titre
- Formally verifying Kyber: Episode V: Machine-checked IND-CCA security and correctness of ML-KEM in EasyCrypt
- auteur
- José Bacelar Almeida, Santiago Arranz Olmos, Manuel Barbosa, Gilles Barthe, François Dupressoir, Benjamin Grégoire, Vincent Laporte, Jean-Christophe Léchenet, Cameron Low, Tiago Oliveira, Hugo Pacheco, Miguel Quaresma, Peter Schwabe, Pierre-Yves Strub
- article
- Crypto 2024, International Association for Cryptologic Research, Aug 2024, Santa Barbara (CA), United States. ⟨10.1007/978-3-031-68379-4_12⟩
- Accès au texte intégral et bibtex
- titre
- CV2EC: Getting the Best of Both Worlds
- auteur
- Bruno Blanchet, Pierre Boutry, Christian Doczkal, Benjamin Grégoire, Pierre-Yves Strub
- article
- CSF 2024 – 37th IEEE Computer Security Foundations Symposium, IEEE, Jul 2024, Enschede, Netherlands. pp.283-298, ⟨10.1109/CSF61375.2024.00019⟩
- Accès au texte intégral et bibtex
- 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
- titre
- Artifact Report: 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.269-274, ⟨10.1007/978-3-031-57262-3_11⟩
- Accès au texte intégral et bibtex
Proceedings
- titre
- Higher-Order unification for free!
- auteur
- Davide Fissore, Enrico Tassi
- article
- PPDP 2024: 26th International Symposium on Principles and Practice of Declarative Programming, ACM, pp.1-13, 2024, ⟨10.1145/3678232.3678233⟩
- Accès au texte intégral et bibtex
Preprints, Working Papers, …
- titre
- Preservation of Speculative Constant-time by Compilation
- auteur
- Santiago Arranz Olmos, Gilles Barthe, Lionel Blatter, Benjamin Grégoire, Vincent Laporte
- article
- 2024
- Accès au texte intégral et bibtex
- titre
- Protecting cryptographic code against Spectre-RSB (and, in fact, all known Spectre variants)
- auteur
- Santiago Arranz Olmos, Gilles Barthe, Chitchanok Chuengsatiansup, Benjamin Grégoire, Vincent Laporte, Tiago Oliveira, Peter Schwabe, Yuval Yarom, Zhiyuan Zhang
- article
- 2024
- Accès au texte intégral et bibtex
- 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
2023
Journal articles
- titre
- High-assurance zeroization
- auteur
- Santiago Arranz Olmos, Gilles Barthe, Ruben Gonzalez, Benjamin Grégoire, Vincent Laporte, Jean-Christophe Léchenet, Tiago Oliveira, Peter Schwabe
- article
- IACR Transactions on Cryptographic Hardware and Embedded Systems, 2023, 2024 (1), pp.375-397. ⟨10.46586/tches.v2024.i1.375-397⟩
- Accès au texte intégral et bibtex
- 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
- 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
- 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
- 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
Conference papers
- titre
- Formally verifying Kyber: Episode IV: Implementation correctness
- 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
- 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
- CRYPTO 2023 : 43rd Annual International Cryptology Conference, Aug 2023, Santa Barbara, CA, United States. pp.421-454, ⟨10.1007/978-3-031-38554-4_14⟩
- Accès au texte intégral et 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
- 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
- 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
- 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
- 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
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
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
Preprints, Working Papers, …
- titre
- Safe smooth paths between straight line obstacles
- auteur
- Yves Bertot
- article
- 2023
- Accès au texte intégral et 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
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
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
- 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
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
- titre
- Primality Tests and Prime Certificate
- auteur
- Laurent Théry
- article
- 2022
- Accès au texte intégral et bibtex
- titre
- A Formalisation of Algorithms for Sorting Network
- auteur
- Laurent Théry
- article
- 2022
- Accès au texte intégral et 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
- 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
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
- 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
- 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
- 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
- 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
- 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
- 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
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
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
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
- 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
- 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
- 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
- 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
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
- 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, ⟨10.1007/978-3-030-51054-1_1⟩
- Accès au texte intégral et 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
- 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
- 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
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
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
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
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
- 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
- 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
- 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
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
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
- 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
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
- 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
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
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
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
- 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
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
- 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
- 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
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
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
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
- 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
- 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
- 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
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
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
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
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
- 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
Lectures
- titre
- Semantics for programming languages with Coq encodings
- auteur
- Yves Bertot
- article
- Master. France. 2015
- Accès au texte intégral et bibtex
Preprints, Working Papers, …
- titre
- Formally-Proven Kosaraju’s algorithm
- auteur
- Laurent Théry
- article
- 2015
- Accès au texte intégral et bibtex
2014
Journal articles
- 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
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
- 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
- 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
- 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
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
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
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
- 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
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
- 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
- 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
- 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
- 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
- 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
- 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
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
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
- 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
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
- 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
- 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
- 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
- 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
- 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
- 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
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
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
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
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
- 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
- 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
- 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
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
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
- 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
- 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
- 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
Preprints, Working Papers, …
- titre
- Formalizing real analysis for polynomials
- auteur
- Cyril Cohen
- article
- 2010
- Accès au texte intégral et bibtex
2009
Journal articles
- titre
- Résoudre le Mini-Rubik’s Cube
- auteur
- Laurent Théry
- article
- Interstices, 2009
- Accès au 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
- 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
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
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
- 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
- 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
- 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
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
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
- 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
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
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
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
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
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
- 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
- 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
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
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
- 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
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
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
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
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
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
- 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
- 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
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
- 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
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
- 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
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
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
- 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
- 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
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
- 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
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
- 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
- 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
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
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
- 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
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
- 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
- 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
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
- titre
- A certified Compiler for an Imperative Language
- auteur
- Yves Bertot
- article
- RR-3488, INRIA. 1998
- Accès au texte intégral et 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
- 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
- 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
- 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
- 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
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
- 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
- titre
- Reasoning with Executable Specifications
- auteur
- Yves Bertot, Ranan Fraer
- article
- RR-2780, INRIA. 1996
- Accès au texte intégral et 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
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
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
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
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
- 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
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
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