default search action

combined dblp search
author search
venue search
publication search

ask others

Pierre-Yves Strub

> Home > Persons

Person information

Refine list

refinements active!

zoomed in on ?? of ?? records

view refined list in

export refined list as

showing all ?? records

Books and Theses

see FAQ

What is the meaning of the colors in the publication lists?

2008
[b1]
- view
  - electronic edition @ archives-ouvertes.fr (open access)
  - details & citations
- export record
  dblp key:
  - phd/hal/Strub08
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/phd/hal/Strub08
Pierre-Yves Strub:
Type Theory and Decision Procedures. (Théorie des Types et Procédures de Décision). École Polytechnique, Palaiseau, France, 2008

Journal Articles

see FAQ

What is the meaning of the colors in the publication lists?

2023
[j11]
- view
  - electronic edition via DOI (open access)
  - details & citations
  authority control:
- export record
  dblp key:
  - journals/pacmpl/ZhouBSLY23
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/pacmpl/ZhouBSLY23
Li Zhou, Gilles Barthe, Pierre-Yves Strub, Junyi Liu, Mingsheng Ying:
CoqQ: Foundational Verification of Quantum Programs. Proc. ACM Program. Lang. 7(POPL): 833-865 (2023)
[j10]
- view
  - electronic edition via DOI (open access)
  - details & citations
  authority control:
- export record
  dblp key:
  - journals/tches/AlmeidaBBGLL00Q23
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/tches/AlmeidaBBGLL00Q23
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:
Formally verifying Kyber Episode IV: Implementation correctness. IACR Trans. Cryptogr. Hardw. Embed. Syst. 2023(3): 164-193 (2023)
[j9]
- view
  authority control:
- export record
  dblp key:
  - journals/tissec/BarbosaBGKS23
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/tissec/BarbosaBGKS23
Manuel Barbosa, Gilles Barthe, Benjamin Grégoire, Adrien Koutsos, Pierre-Yves Strub:
Mechanized Proofs of Adversarial Complexity and Application to Universal Composability. ACM Trans. Priv. Secur. 26(3): 41:1-41:34 (2023)
2022
[j8]
- view
  - electronic edition via DOI (open access)
  - details & citations
  authority control:
- export record
  dblp key:
  - journals/lmcs/AllamigeonKS22
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/lmcs/AllamigeonKS22
Xavier Allamigeon, Ricardo D. Katz, Pierre-Yves Strub:
Formalizing the Face Lattice of Polyhedra. Log. Methods Comput. Sci. 18(2) (2022)
2020
[j7]
- view
  authority control:
- export record
  dblp key:
  - journals/jce/BartheBDFGSS20
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/jce/BartheBDFGSS20
Gilles Barthe, Sonia Belaïd, François Dupressoir, Pierre-Alain Fouque, Benjamin Grégoire, François-Xavier Standaert, Pierre-Yves Strub:
Improved parallel mask refreshing algorithms: generic solutions with parametrized non-interference and automated optimizations. J. Cryptogr. Eng. 10(1): 17-26 (2020)
2019
[j6]
- view
  authority control:
- export record
  dblp key:
  - journals/jfp/AguirreBGGS19
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/jfp/AguirreBGGS19
Alejandro Aguirre, Gilles Barthe, Marco Gaboardi, Deepak Garg, Pierre-Yves Strub:
A relational logic for higher-order programs. J. Funct. Program. 29: e16 (2019)
[j5]
- view
  - electronic edition via DOI (open access)
  - details & citations
  authority control:
- export record
  dblp key:
  - journals/lmcs/BartheEHSS19
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/lmcs/BartheEHSS19
Gilles Barthe, Thomas Espitau, Justin Hsu, Tetsuya Sato, Pierre-Yves Strub:
Relational ⋆⋆\star-Liftings for Differential Privacy. Log. Methods Comput. Sci. 15(4) (2019)
2018
[j4]
- view
  - electronic edition via DOI (open access)
  - details & citations
  authority control:
- export record
  dblp key:
  - journals/pacmpl/BartheEGHS18
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/pacmpl/BartheEGHS18
Gilles Barthe, Thomas Espitau, Benjamin Grégoire, Justin Hsu, Pierre-Yves Strub:
Proving expected sensitivity of probabilistic programs. Proc. ACM Program. Lang. 2(POPL): 57:1-57:29 (2018)
2017
[j3]
- view
  authority control:
- export record
  dblp key:
  - journals/cacm/BeurdoucheBDFKP17
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/cacm/BeurdoucheBDFKP17
Benjamin Beurdouche, Karthikeyan Bhargavan, Antoine Delignat-Lavaud, Cédric Fournet, Markulf Kohlweiss, Alfredo Pironti, Pierre-Yves Strub, Jean Karim Zinzindohoue:
A messy state of the union: taming the composite state machines of TLS. Commun. ACM 60(2): 99-107 (2017)
[j2]
- view
  - electronic edition via DOI (open access)
  - details & citations
  authority control:
- export record
  dblp key:
  - journals/pacmpl/AguirreBG0S17
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/pacmpl/AguirreBG0S17
Alejandro Aguirre, Gilles Barthe, Marco Gaboardi, Deepak Garg, Pierre-Yves Strub:
A relational logic for higher-order programs. Proc. ACM Program. Lang. 1(ICFP): 21:1-21:29 (2017)
2013
[j1]
- view
  authority control:
- export record
  dblp key:
  - journals/jfp/SwamyCFSBY13
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/jfp/SwamyCFSBY13
Nikhil Swamy, Juan Chen, Cédric Fournet, Pierre-Yves Strub, Karthikeyan Bhargavan, Jean Yang:
Secure distributed programming with value-dependent types. J. Funct. Program. 23(4): 402-451 (2013)

Conference and Workshop Papers

see FAQ

What is the meaning of the colors in the publication lists?

2024
[c55]
- view
  authority control:
- export record
  dblp key:
  - conf/ashes/KundiMSH24
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/ashes/KundiMSH24
Dur-e-Shahwar Kundi, Jose M. Bermudo Mera, Pierre-Yves Strub, Michael Hutter:
High-Performance NTT Hardware Accelerator to Support ML-KEM and ML-DSA. ASHES@CCS 2024: 100-105
[c54]
- view
  authority control:
- export record
  dblp key:
  - conf/crypto/AlmeidaOBBDGLLLOPQSS24
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/crypto/AlmeidaOBBDGLLLOPQSS24
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:
Formally Verifying Kyber - Episode V: Machine-Checked IND-CCA Security and Correctness of ML-KEM in EasyCrypt. CRYPTO (2) 2024: 384-421
[c53]
- view
  authority control:
- export record
  dblp key:
  - conf/csfw/BlanchetBDGS24
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/csfw/BlanchetBDGS24
Bruno Blanchet, Pierre Boutry, Christian Doczkal, Benjamin Grégoire, Pierre-Yves Strub:
CV2EC: Getting the Best of Both Worlds. CSF 2024: 279-294
2023
[c52]
- view
  authority control:
- export record
  dblp key:
  - conf/cpp/AllamigeonCS23
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cpp/AllamigeonCS23
Xavier Allamigeon, Quentin Canu, Pierre-Yves Strub:
A Formal Disproof of Hirsch Conjecture. CPP 2023: 17-29
[c51]
- view
  authority control:
- export record
  dblp key:
  - conf/crypto/BarbosaDGHMS22
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/crypto/BarbosaDGHMS22
Manuel Barbosa, François Dupressoir, Benjamin Grégoire, Andreas Hülsing, Matthias Meijers, Pierre-Yves Strub:
Machine-Checked Security for rmXMSS as in RFC 8391 and $\mathrm {SPHINCS^{+}} $. CRYPTO (5) 2023: 421-454
2022
[c50]
- view
  authority control:
- export record
  dblp key:
  - conf/cpp/DonatoSW22
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cpp/DonatoSW22
Pablo Donato, Pierre-Yves Strub, Benjamin Werner:
A drag-and-drop proof tactic. CPP 2022: 197-209
[c49]
- view
  authority control:
- export record
  dblp key:
  - conf/crypto/HulsingMS22
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/crypto/HulsingMS22
Andreas Hülsing, Matthias Meijers, Pierre-Yves Strub:
Formal Verification of Saber's Public-Key Encryption Scheme in EasyCrypt. CRYPTO (1) 2022: 622-653
2021
[c48]
- view
  authority control:
- export record
  dblp key:
  - conf/ccs/BarbosaBGKS21
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/ccs/BarbosaBGKS21
Manuel Barbosa, Gilles Barthe, Benjamin Grégoire, Adrien Koutsos, Pierre-Yves Strub:
Mechanized Proofs of Adversarial Complexity and Application to Universal Composability. CCS 2021: 2541-2563
[c47]
- view
  authority control:
- export record
  dblp key:
  - conf/ccs/BarbosaBFGHKSWZ21
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/ccs/BarbosaBFGHKSWZ21
Manuel Barbosa, Gilles Barthe, Xiong Fan, Benjamin Grégoire, Shih-Han Hung, Jonathan Katz, Pierre-Yves Strub, Xiaodi Wu, Li Zhou:
EasyPQC: Verifying Post-Quantum Cryptography. CCS 2021: 2564-2586
[c46]
- view
  - electronic edition via DOI (open access)
  - details & citations
  authority control:
- export record
  dblp key:
  - conf/itp/BernardCMS21
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/itp/BernardCMS21
Sophie Bernard, Cyril Cohen, Assia Mahboubi, Pierre-Yves Strub:
Unsolvability of the Quintic Formalized in Dependent Type Theory. ITP 2021: 8:1-8:18
2020
[c45]
- view
  authority control:
- export record
  dblp key:
  - conf/cade/AllamigeonKS20
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cade/AllamigeonKS20
Xavier Allamigeon, Ricardo D. Katz, Pierre-Yves Strub:
Formalizing the Face Lattice of Polyhedra. IJCAR (2) 2020: 185-203
[c44]
- view
  authority control:
- export record
  dblp key:
  - conf/sp/AlmeidaBBGKL0S20
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/sp/AlmeidaBBGKL0S20
José Bacelar Almeida, Manuel Barbosa, Gilles Barthe, Benjamin Grégoire, Adrien Koutsos, Vincent Laporte, Tiago Oliveira, Pierre-Yves Strub:
The Last Mile: High-Assurance and High-Speed Cryptographic Implementations. SP 2020: 965-982
2019
[c43]
- view
  authority control:
- export record
  dblp key:
  - conf/ccs/AlmeidaBBCCGPPS19
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/ccs/AlmeidaBBCCGPPS19
José Bacelar Almeida, Manuel Barbosa, Gilles Barthe, Matthew Campagna, Ernie Cohen, Benjamin Grégoire, Vitor Pereira, Bernardo Portela, Pierre-Yves Strub, Serdar Tasiran:
A Machine-Checked Proof of Security for AWS Key Management Service. CCS 2019: 63-78
[c42]
- view
  authority control:
- export record
  dblp key:
  - conf/ccs/AlmeidaBBBDGL0S19
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/ccs/AlmeidaBBBDGL0S19
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:
Machine-Checked Proofs for Cryptographic Standards: Indifferentiability of Sponge and Secure High-Assurance Implementations of SHA-3. CCS 2019: 1607-1622
[c41]
- view
  authority control:
- export record
  dblp key:
  - conf/csfw/BartheGJKS19
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/csfw/BartheGJKS19
Gilles Barthe, Benjamin Grégoire, Charlie Jacomme, Steve Kremer, Pierre-Yves Strub:
Symbolic Methods in Computational Cryptography Proofs. CSF 2019: 136-151
2018
[c40]
- view
  authority control:
- export record
  dblp key:
  - conf/csfw/HaaghKOSS18
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/csfw/HaaghKOSS18
Helene Haagh, Aleksandr Karbyshev, Sabine Oechsner, Bas Spitters, Pierre-Yves Strub:
Computer-Aided Proofs for Multiparty Computation with Active Security. CSF 2018: 119-131
[c39]
- view
  - electronic edition via DOI (open access)
  - details & citations
  authority control:
- export record
  dblp key:
  - conf/esop/BartheEGGHS18
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/esop/BartheEGGHS18
Gilles Barthe, Thomas Espitau, Marco Gaboardi, Benjamin Grégoire, Justin Hsu, Pierre-Yves Strub:
An Assertion-Based Program Logic for Probabilistic Programs. ESOP 2018: 117-144
[c38]
- view
  authority control:
- export record
  dblp key:
  - conf/secsr/BhargavanKS18
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/secsr/BhargavanKS18
Karthikeyan Bhargavan, Franziskus Kiefer, Pierre-Yves Strub:
hacspec: Towards Verifiable Crypto Standards. SSR 2018: 1-20
2017
[c37]
- view
  authority control:
- export record
  dblp key:
  - conf/ccs/AlmeidaBBBGLOPS17
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/ccs/AlmeidaBBBGLOPS17
José Bacelar Almeida, Manuel Barbosa, Gilles Barthe, Arthur Blot, Benjamin Grégoire, Vincent Laporte, Tiago Oliveira, Hugo Pacheco, Benedikt Schmidt, Pierre-Yves Strub:
Jasmin: High-Assurance and High-Speed Cryptography. CCS 2017: 1807-1823
[c36]
- view
  authority control:
- export record
  dblp key:
  - conf/eurocrypt/BartheDFGSS17
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/eurocrypt/BartheDFGSS17
Gilles Barthe, François Dupressoir, Sebastian Faust, Benjamin Grégoire, François-Xavier Standaert, Pierre-Yves Strub:
Parallel Implementations of Masking Schemes and the Bounded Moment Leakage Model. EUROCRYPT (1) 2017: 535-566
[c35]
- view
  - electronic edition via DOI (open access)
  - details & citations
  authority control:
- export record
  dblp key:
  - conf/icalp/BartheEHSS17
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/icalp/BartheEHSS17
Gilles Barthe, Thomas Espitau, Justin Hsu, Tetsuya Sato, Pierre-Yves Strub:
*-Liftings for Differential Privacy. ICALP 2017: 102:1-102:12
[c34]
- view
  - electronic edition via DOI (open access)
  - details & citations
  authority control:
- export record
  dblp key:
  - conf/lpar/BartheEGHS17
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/lpar/BartheEGHS17
Gilles Barthe, Thomas Espitau, Benjamin Grégoire, Justin Hsu, Pierre-Yves Strub:
Proving uniformity and independence by self-composition and coupling. LPAR 2017: 385-403
[c33]
- view
  - electronic edition via DOI (open access)
  - details & citations
  authority control:
- export record
  dblp key:
  - conf/lpar/JouannaudS17
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/lpar/JouannaudS17
Jean-Pierre Jouannaud, Pierre-Yves Strub:
Coq without Type Casts: A Complete Proof of Coq Modulo Theory. LPAR 2017: 474-489
[c32]
- view
  authority control:
- export record
  dblp key:
  - conf/popl/BartheGHS17
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/popl/BartheGHS17
Gilles Barthe, Benjamin Grégoire, Justin Hsu, Pierre-Yves Strub:
Coupling proofs are probabilistic product programs. POPL 2017: 161-174
[c31]
- view
  authority control:
- export record
  dblp key:
  - conf/sp/CortierDDSSW17
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/sp/CortierDDSSW17
Véronique Cortier, Constantin Catalin Dragan, François Dupressoir, Benedikt Schmidt, Pierre-Yves Strub, Bogdan Warinschi:
Machine-Checked Proofs of Privacy for Electronic Voting Protocols. IEEE Symposium on Security and Privacy 2017: 993-1008
2016
[c30]
- view
  authority control:
- export record
  dblp key:
  - conf/ccs/BartheFGGHS16
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/ccs/BartheFGGHS16
Gilles Barthe, Noémie Fong, Marco Gaboardi, Benjamin Grégoire, Justin Hsu, Pierre-Yves Strub:
Advanced Probabilistic Couplings for Differential Privacy. CCS 2016: 55-67
[c29]
- view
  authority control:
- export record
  dblp key:
  - conf/ccs/BartheFGAGHS16
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/ccs/BartheFGAGHS16
Gilles Barthe, Gian Pietro Farina, Marco Gaboardi, Emilio Jesús Gallego Arias, Andy Gordon, Justin Hsu, Pierre-Yves Strub:
Differentially Private Bayesian Programming. CCS 2016: 68-79
[c28]
- view
  authority control:
- export record
  dblp key:
  - conf/ccs/BartheBDFGSZ16
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/ccs/BartheBDFGSZ16
Gilles Barthe, Sonia Belaïd, François Dupressoir, Pierre-Alain Fouque, Benjamin Grégoire, Pierre-Yves Strub, Rébecca Zucchini:
Strong Non-Interference and Type-Directed Higher-Order Masking. CCS 2016: 116-129
[c27]
- view
  authority control:
- export record
  dblp key:
  - conf/cpp/BernardBRS16
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cpp/BernardBRS16
Sophie Bernard, Yves Bertot, Laurence Rideau, Pierre-Yves Strub:
Formal proofs of transcendence for e and pi as an application of multivariate and symmetric polynomials. CPP 2016: 76-87
[c26]
- view
  - electronic edition via DOI (open access)
  - details & citations
  authority control:
- export record
  dblp key:
  - conf/icalp/BartheGGHS16
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/icalp/BartheGGHS16
Gilles Barthe, Marco Gaboardi, Benjamin Grégoire, Justin Hsu, Pierre-Yves Strub:
A Program Logic for Union Bounds. ICALP 2016: 107:1-107:15
[c25]
- view
  authority control:
- export record
  dblp key:
  - conf/lics/BartheGGHS16
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/lics/BartheGGHS16
Gilles Barthe, Marco Gaboardi, Benjamin Grégoire, Justin Hsu, Pierre-Yves Strub:
Proving Differential Privacy via Probabilistic Couplings. LICS 2016: 749-758
[c24]
- view
  authority control:
- export record
  dblp key:
  - conf/popl/SwamyHKRDFBFSKZ16
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/popl/SwamyHKRDFBFSKZ16
Nikhil Swamy, Catalin Hritcu, Chantal Keller, Aseem Rastogi, Antoine Delignat-Lavaud, Simon Forest, Karthikeyan Bhargavan, Cédric Fournet, Pierre-Yves Strub, Markulf Kohlweiss, Jean Karim Zinzindohoue, Santiago Zanella Béguelin:
Dependent types and multi-monadic effects in F. POPL 2016: 256-270
[c23]
- view
  authority control:
- export record
  dblp key:
  - conf/wine/BartheGAHRS16
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/wine/BartheGAHRS16
Gilles Barthe, Marco Gaboardi, Emilio Jesús Gallego Arias, Justin Hsu, Aaron Roth, Pierre-Yves Strub:
Computer-Aided Verification for Mechanism Design. WINE 2016: 279-293
2015
[c22]
- view
  - electronic edition via DOI (open access)
  - details & citations
  authority control:
- export record
  dblp key:
  - conf/eurocrypt/BartheBDFGS15
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/eurocrypt/BartheBDFGS15
Gilles Barthe, Sonia Belaïd, François Dupressoir, Pierre-Alain Fouque, Benjamin Grégoire, Pierre-Yves Strub:
Verified Proofs of Higher-Order Masking. EUROCRYPT (1) 2015: 457-485
[c21]
- view
  authority control:
- export record
  dblp key:
  - conf/lpar/BartheEGHSS15
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/lpar/BartheEGHSS15
Gilles Barthe, Thomas Espitau, Benjamin Grégoire, Justin Hsu, Léo Stefanesco, Pierre-Yves Strub:
Relational Reasoning via Probabilistic Coupling. LPAR 2015: 387-401
[c20]
- view
  authority control:
- export record
  dblp key:
  - conf/popl/BartheGAHRS15
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/popl/BartheGAHRS15
Gilles Barthe, Marco Gaboardi, Emilio Jesús Gallego Arias, Justin Hsu, Aaron Roth, Pierre-Yves Strub:
Higher-Order Approximate Relational Refinement Types for Mechanism Design and Differential Privacy. POPL 2015: 55-68
[c19]
- view
  authority control:
- export record
  dblp key:
  - conf/sp/BeurdoucheBDFKP15
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/sp/BeurdoucheBDFKP15
Benjamin Beurdouche, Karthikeyan Bhargavan, Antoine Delignat-Lavaud, Cédric Fournet, Markulf Kohlweiss, Alfredo Pironti, Pierre-Yves Strub, Jean Karim Zinzindohoue:
A Messy State of the Union: Taming the Composite State Machines of TLS. IEEE Symposium on Security and Privacy 2015: 535-552
2014
[c18]
- view
  - electronic edition via DOI (open access)
  - details & citations
  authority control:
- export record
  dblp key:
  - conf/crypto/BhargavanFKPSB14
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/crypto/BhargavanFKPSB14
Karthikeyan Bhargavan, Cédric Fournet, Markulf Kohlweiss, Alfredo Pironti, Pierre-Yves Strub, Santiago Zanella Béguelin:
Proving the TLS Handshake Secure (As It Is). CRYPTO (2) 2014: 235-255
[c17]
- view
  authority control:
- export record
  dblp key:
  - conf/csfw/AkinyeleBGSS14
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/csfw/AkinyeleBGSS14
Joseph A. Akinyele, Gilles Barthe, Benjamin Grégoire, Benedikt Schmidt, Pierre-Yves Strub:
Certified Synthesis of Efficient Batch Verifiers. CSF 2014: 153-165
[c16]
- view
  authority control:
- export record
  dblp key:
  - conf/csfw/BartheGAHKS14
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/csfw/BartheGAHKS14
Gilles Barthe, Marco Gaboardi, Emilio Jesús Gallego Arias, Justin Hsu, César Kunz, Pierre-Yves Strub:
Proving Differential Privacy in Hoare Logic. CSF 2014: 411-424
[c15]
- view
  authority control:
- export record
  dblp key:
  - conf/itp/BartziaS14
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/itp/BartziaS14
Evmorfia-Iro Bartzia, Pierre-Yves Strub:
A Formal Library for Elliptic Curves in the Coq Proof Assistant. ITP 2014: 77-92
[c14]
- view
  authority control:
- export record
  dblp key:
  - conf/popl/BartheFGSSB14
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/popl/BartheFGSSB14
Gilles Barthe, Cédric Fournet, Benjamin Grégoire, Pierre-Yves Strub, Nikhil Swamy, Santiago Zanella Béguelin:
Probabilistic relational verification for cryptographic implementations. POPL 2014: 193-206
[c13]
- view
  authority control:
- export record
  dblp key:
  - conf/popl/SwamyFRBCSB14
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/popl/SwamyFRBCSB14
Nikhil Swamy, Cédric Fournet, Aseem Rastogi, Karthikeyan Bhargavan, Juan Chen, Pierre-Yves Strub, Gavin M. Bierman:
Gradual typing embedded securely in JavaScript. POPL 2014: 425-438
[c12]
- view
  authority control:
- export record
  dblp key:
  - conf/sp/BhargavanDFPS14
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/sp/BhargavanDFPS14
Karthikeyan Bhargavan, Antoine Delignat-Lavaud, Cédric Fournet, Alfredo Pironti, Pierre-Yves Strub:
Triple Handshakes and Cookie Cutters: Breaking and Fixing Authentication over TLS. IEEE Symposium on Security and Privacy 2014: 98-113
2013
[c11]
- view
  authority control:
- export record
  dblp key:
  - conf/fosad/BartheDGKSS13
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/fosad/BartheDGKSS13
Gilles Barthe, François Dupressoir, Benjamin Grégoire, César Kunz, Benedikt Schmidt, Pierre-Yves Strub:
EasyCrypt: A Tutorial. FOSAD 2013: 146-166
[c10]
- view
  authority control:
- export record
  dblp key:
  - conf/popl/FournetSCDSL13
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/popl/FournetSCDSL13
Cédric Fournet, Nikhil Swamy, Juan Chen, Pierre-Évariste Dagand, Pierre-Yves Strub, Benjamin Livshits:
Fully abstract compilation to JavaScript. POPL 2013: 371-384
[c9]
- view
  authority control:
- export record
  dblp key:
  - conf/sp/BhargavanFKPS13
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/sp/BhargavanFKPS13
Karthikeyan Bhargavan, Cédric Fournet, Markulf Kohlweiss, Alfredo Pironti, Pierre-Yves Strub:
Implementing TLS with Verified Cryptographic Security. IEEE Symposium on Security and Privacy 2013: 445-459
2012
[c8]
- view
  authority control:
- export record
  dblp key:
  - conf/popl/StrubSFC12
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/popl/StrubSFC12
Pierre-Yves Strub, Nikhil Swamy, Cédric Fournet, Juan Chen:
Self-certification: bootstrapping certified typecheckers in F* with Coq. POPL 2012: 571-584
2011
[c7]
- view
  authority control:
- export record
  dblp key:
  - conf/ccs/FournetKS11
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/ccs/FournetKS11
Cédric Fournet, Markulf Kohlweiss, Pierre-Yves Strub:
Modular code-based cryptographic verification. CCS 2011: 341-350
[c6]
- view
  authority control:
- export record
  dblp key:
  - conf/icfp/SwamyCFSBY11
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/icfp/SwamyCFSBY11
Nikhil Swamy, Juan Chen, Cédric Fournet, Pierre-Yves Strub, Karthikeyan Bhargavan, Jean Yang:
Secure distributed programming with value-dependent types. ICFP 2011: 266-278
[c5]
- view
  authority control:
- export record
  dblp key:
  - conf/lics/BarrasJSW11
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/lics/BarrasJSW11
Bruno Barras, Jean-Pierre Jouannaud, Pierre-Yves Strub, Qian Wang:
CoQMTU: A Higher-Order Type Theory with a Predicative Hierarchy of Universes Parametrized by a Decidable First-Order Theory. LICS 2011: 143-151
2010
[c4]
- view
  authority control:
- export record
  dblp key:
  - conf/csl/Strub10
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/csl/Strub10
Pierre-Yves Strub:
Coq Modulo Theory. CSL 2010: 529-543
2008
[c3]
- view
  - electronic edition via DOI (open access)
  - details & citations
  authority control:
- export record
  dblp key:
  - conf/ifipTCS/BlanquiJS08
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/ifipTCS/BlanquiJS08
Frédéric Blanqui, Jean-Pierre Jouannaud, Pierre-Yves Strub:
From Formal Proofs to Mathematical Proofs: A Safe, Incremental Way for Building in First-order Decision Procedures. IFIP TCS 2008: 349-365
2007
[c2]
- view
  authority control:
- export record
  dblp key:
  - conf/csl/BlanquiJS07
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/csl/BlanquiJS07
Frédéric Blanqui, Jean-Pierre Jouannaud, Pierre-Yves Strub:
Building Decision Procedures in the Calculus of Inductive Constructions. CSL 2007: 328-342
2001
[c1]
- view
  authority control:
- export record
  dblp key:
  - conf/icip/GeraudSD01
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/icip/GeraudSD01
Thierry Géraud, Pierre-Yves Strub, Jérôme Darbon:
Color image segmentation based on automatic morphological clustering. ICIP (3) 2001: 70-73

Informal and Other Publications

see FAQ

What is the meaning of the colors in the publication lists?

2024
[i38]
- view
  - electronic edition @ iacr.org (open access)
  - details & citations
- export record
  dblp key:
  - journals/iacr/AlmeidaOBBDGLLLOPQSS24
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/iacr/AlmeidaOBBDGLLLOPQSS24
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:
Formally verifying Kyber Episode V: Machine-checked IND-CCA security and correctness of ML-KEM in EasyCrypt. IACR Cryptol. ePrint Arch. 2024: 843 (2024)
[i37]
- view
  - electronic edition @ iacr.org (open access)
  - details & citations
- export record
  dblp key:
  - journals/iacr/BarbosaDHMS24
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/iacr/BarbosaDHMS24
Manuel Barbosa, François Dupressoir, Andreas Hülsing, Matthias Meijers, Pierre-Yves Strub:
A Tight Security Proof for $\mathrm{SPHINCS^{+}}$, Formally Verified. IACR Cryptol. ePrint Arch. 2024: 910 (2024)
2023
[i36]
- view
  - electronic edition via DOI (open access)
  - details & citations
  authority control:
- export record
  dblp key:
  - journals/corr/abs-2301-04060
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/corr/abs-2301-04060
Xavier Allamigeon, Quentin Canu, Pierre-Yves Strub:
A Formal Disproof of the Hirsch Conjecture. CoRR abs/2301.04060 (2023)
[i35]
- view
  - electronic edition @ iacr.org (open access)
  - details & citations
- export record
  dblp key:
  - journals/iacr/AlmeidaBBGLLOPQSSS23
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/iacr/AlmeidaBBGLLOPQSSS23
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:
Formally verifying Kyber Part I: Implementation Correctness. IACR Cryptol. ePrint Arch. 2023: 215 (2023)
[i34]
- view
  - electronic edition @ iacr.org (open access)
  - details & citations
- export record
  dblp key:
  - journals/iacr/BarbosaDGHMS23
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/iacr/BarbosaDGHMS23
Manuel Barbosa, François Dupressoir, Benjamin Grégoire, Andreas Hülsing, Matthias Meijers, Pierre-Yves Strub:
Machine-Checked Security for $\mathrm{XMSS}$ as in RFC 8391 and $\mathrm{SPHINCS}^{+}$. IACR Cryptol. ePrint Arch. 2023: 408 (2023)
2022
[i33]
- view
  - electronic edition via DOI (open access)
  - details & citations
  authority control:
- export record
  dblp key:
  - journals/corr/abs-2207-11350
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/corr/abs-2207-11350
Li Zhou, Gilles Barthe, Pierre-Yves Strub, Junyi Liu, Mingsheng Ying:
CoqQ: Foundational Verification of Quantum Programs. CoRR abs/2207.11350 (2022)
[i32]
- view
  - electronic edition via DOI (open access)
  - details & citations
  authority control:
- export record
  dblp key:
  - journals/corr/abs-2210-11820
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/corr/abs-2210-11820
Pablo Donato, Pierre-Yves Strub, Benjamin Werner:
A drag-and-drop proof tactic. CoRR abs/2210.11820 (2022)
[i31]
- view
  - electronic edition @ iacr.org (open access)
  - details & citations
- export record
  dblp key:
  - journals/iacr/HulsingMS22
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/iacr/HulsingMS22
Andreas Hülsing, Matthias Meijers, Pierre-Yves Strub:
Formal Verification of Saber's Public-Key Encryption Scheme in EasyCrypt. IACR Cryptol. ePrint Arch. 2022: 351 (2022)
2021
[i30]
- view
  - electronic edition @ arxiv.org (open access)
  - details & citations
- export record
  dblp key:
  - journals/corr/abs-2104-15021
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/corr/abs-2104-15021
Xavier Allamigeon, Ricardo D. Katz, Pierre-Yves Strub:
Formalizing the Face Lattice of Polyhedra. CoRR abs/2104.15021 (2021)
[i29]
- view
  - electronic edition @ iacr.org (open access)
  - details & citations
- export record
  dblp key:
  - journals/iacr/BarbosaBGKS21
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/iacr/BarbosaBGKS21
Manuel Barbosa, Gilles Barthe, Benjamin Grégoire, Adrien Koutsos, Pierre-Yves Strub:
Mechanized Proofs of Adversarial Complexity and Application to Universal Composability. IACR Cryptol. ePrint Arch. 2021: 156 (2021)
[i28]
- view
  - electronic edition @ iacr.org (open access)
  - details & citations
- export record
  dblp key:
  - journals/iacr/BarbosaBFGHKSWZ21
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/iacr/BarbosaBFGHKSWZ21
Manuel Barbosa, Gilles Barthe, Xiong Fan, Benjamin Grégoire, Shih-Han Hung, Jonathan Katz, Pierre-Yves Strub, Xiaodi Wu, Li Zhou:
EasyPQC: Verifying Post-Quantum Cryptography. IACR Cryptol. ePrint Arch. 2021: 1253 (2021)
2019
[i27]
- view
  - electronic edition @ arxiv.org (open access)
  - details & citations
- export record
  dblp key:
  - journals/corr/abs-1904-04606
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/corr/abs-1904-04606
José Bacelar Almeida, Manuel Barbosa, Gilles Barthe, Benjamin Grégoire, Adrien Koutsos, Vincent Laporte, Tiago Oliveira, Pierre-Yves Strub:
The Last Mile: High-Assurance and High-Speed Cryptographic Implementations. CoRR abs/1904.04606 (2019)
[i26]
- view
  - electronic edition @ iacr.org (open access)
  - details & citations
- export record
  dblp key:
  - journals/iacr/AlmeidaBBCCGPPS19
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/iacr/AlmeidaBBCCGPPS19
José Bacelar Almeida, Manuel Barbosa, Gilles Barthe, Matthew Campagna, Ernie Cohen, Benjamin Grégoire, Vitor Pereira, Bernardo Portela, Pierre-Yves Strub, Serdar Tasiran:
A Machine-Checked Proof of Security for AWS Key Management Service. IACR Cryptol. ePrint Arch. 2019: 1042 (2019)
[i25]
- view
  - electronic edition @ iacr.org (open access)
  - details & citations
- export record
  dblp key:
  - journals/iacr/AlmeidaBBBDGLOS19
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/iacr/AlmeidaBBBDGLOS19
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:
Machine-Checked Proofs for Cryptographic Standards. IACR Cryptol. ePrint Arch. 2019: 1155 (2019)
2018
[i24]
- view
  - electronic edition @ arxiv.org (open access)
  - details & citations
- export record
  dblp key:
  - journals/corr/abs-1803-05535
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/corr/abs-1803-05535
Gilles Barthe, Thomas Espitau, Marco Gaboardi, Benjamin Grégoire, Justin Hsu, Pierre-Yves Strub:
An Assertion-Based Program Logic for Probabilistic Programs. CoRR abs/1803.05535 (2018)
[i23]
- view
  - electronic edition @ arxiv.org (open access)
  - details & citations
- export record
  dblp key:
  - journals/corr/abs-1806-07197
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/corr/abs-1806-07197
Helene Haagh, Aleksandr Karbyshev, Sabine Oechsner, Bas Spitters, Pierre-Yves Strub:
Computer-aided proofs for multiparty computation with active security. CoRR abs/1806.07197 (2018)
[i22]
- view
  - electronic edition @ iacr.org (open access)
  - details & citations
- export record
  dblp key:
  - journals/iacr/HaaghKOSS18
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/iacr/HaaghKOSS18
Helene Haagh, Aleksandr Karbyshev, Sabine Oechsner, Bas Spitters, Pierre-Yves Strub:
Computer-aided proofs for multiparty computation with active security. IACR Cryptol. ePrint Arch. 2018: 502 (2018)
[i21]
- view
  - electronic edition @ iacr.org (open access)
  - details & citations
- export record
  dblp key:
  - journals/iacr/BartheBDFGSS18
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/iacr/BartheBDFGSS18
Gilles Barthe, Sonia Belaïd, François Dupressoir, Pierre-Alain Fouque, Benjamin Grégoire, François-Xavier Standaert, Pierre-Yves Strub:
Improved Parallel Mask Refreshing Algorithms: Generic Solutions with Parametrized Non-Interference & Automated Optimizations. IACR Cryptol. ePrint Arch. 2018: 505 (2018)
2017
[i20]
- view
  - electronic edition @ arxiv.org (open access)
  - details & citations
- export record
  dblp key:
  - journals/corr/BartheEGHS17
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/corr/BartheEGHS17
Gilles Barthe, Thomas Espitau, Benjamin Grégoire, Justin Hsu, Pierre-Yves Strub:
Proving uniformity and independence by self-composition and coupling. CoRR abs/1701.06477 (2017)
[i19]
- view
  - electronic edition @ arxiv.org (open access)
  - details & citations
- export record
  dblp key:
  - journals/corr/AguirreBG0S17
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/corr/AguirreBG0S17
Alejandro Aguirre, Gilles Barthe, Marco Gaboardi, Deepak Garg, Pierre-Yves Strub:
A Relational Logic for Higher-Order Programs. CoRR abs/1703.05042 (2017)
[i18]
- view
  - electronic edition @ arxiv.org (open access)
  - details & citations
- export record
  dblp key:
  - journals/corr/BartheEHSS17
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/corr/BartheEHSS17
Gilles Barthe, Thomas Espitau, Justin Hsu, Tetsuya Sato, Pierre-Yves Strub:
*-Liftings for Differential Privacy. CoRR abs/1705.00133 (2017)
[i17]
- view
  - electronic edition @ arxiv.org (open access)
  - details & citations
- export record
  dblp key:
  - journals/corr/abs-1708-02537
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/corr/abs-1708-02537
Gilles Barthe, Thomas Espitau, Benjamin Grégoire, Justin Hsu, Pierre-Yves Strub:
Proving Expected Sensitivity of Probabilistic Programs. CoRR abs/1708.02537 (2017)
2016
[i16]
- view
  - electronic edition @ arxiv.org (open access)
  - details & citations
- export record
  dblp key:
  - journals/corr/BartheGGHS16
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/corr/BartheGGHS16
Gilles Barthe, Marco Gaboardi, Benjamin Grégoire, Justin Hsu, Pierre-Yves Strub:
Proving Differential Privacy via Probabilistic Couplings. CoRR abs/1601.05047 (2016)
[i15]
- view
  - electronic edition @ arxiv.org (open access)
  - details & citations
- export record
  dblp key:
  - journals/corr/BartheGGHS16a
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/corr/BartheGGHS16a
Gilles Barthe, Marco Gaboardi, Benjamin Grégoire, Justin Hsu, Pierre-Yves Strub:
A program logic for union bounds. CoRR abs/1602.05681 (2016)
[i14]
- view
  - electronic edition @ arxiv.org (open access)
  - details & citations
- export record
  dblp key:
  - journals/corr/BartheFGAGHS16
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/corr/BartheFGAGHS16
Gilles Barthe, Gian Pietro Farina, Marco Gaboardi, Emilio Jesús Gallego Arias, Andy Gordon, Justin Hsu, Pierre-Yves Strub:
Differentially Private Bayesian Programming. CoRR abs/1605.00283 (2016)
[i13]
- view
  - electronic edition @ arxiv.org (open access)
  - details & citations
- export record
  dblp key:
  - journals/corr/BartheGGHS16b
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/corr/BartheGGHS16b
Gilles Barthe, Marco Gaboardi, Benjamin Grégoire, Justin Hsu, Pierre-Yves Strub:
Advanced Probabilistic Couplings for Differential Privacy. CoRR abs/1606.07143 (2016)
[i12]
- view
  - electronic edition @ arxiv.org (open access)
  - details & citations
- export record
  dblp key:
  - journals/corr/BartheGHS16
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/corr/BartheGHS16
Gilles Barthe, Benjamin Grégoire, Justin Hsu, Pierre-Yves Strub:
Coupling proofs are probabilistic product programs. CoRR abs/1607.03455 (2016)
[i11]
- view
  - electronic edition @ iacr.org (open access)
  - details & citations
- export record
  dblp key:
  - journals/iacr/BartheDFGSS16
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/iacr/BartheDFGSS16
Gilles Barthe, François Dupressoir, Sebastian Faust, Benjamin Grégoire, François-Xavier Standaert, Pierre-Yves Strub:
Parallel Implementations of Masking Schemes and the Bounded Moment Leakage Model. IACR Cryptol. ePrint Arch. 2016: 912 (2016)
2015
[i10]
- view
  - electronic edition @ arxiv.org (open access)
  - details & citations
- export record
  dblp key:
  - journals/corr/BartheGAHRS15
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/corr/BartheGAHRS15
Gilles Barthe, Marco Gaboardi, Emilio Jesús Gallego Arias, Justin Hsu, Aaron Roth, Pierre-Yves Strub:
Computer-aided verification in mechanism design. CoRR abs/1502.04052 (2015)
[i9]
- view
  - electronic edition @ arxiv.org (open access)
  - details & citations
- export record
  dblp key:
  - journals/corr/BartheEGHSS15
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/corr/BartheEGHSS15
Gilles Barthe, Thomas Espitau, Benjamin Grégoire, Justin Hsu, Léo Stefanesco, Pierre-Yves Strub:
Relational reasoning via probabilistic coupling. CoRR abs/1509.03476 (2015)
[i8]
- view
  - electronic edition @ arxiv.org (open access)
  - details & citations
- export record
  dblp key:
  - journals/corr/BernardBRS15
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/corr/BernardBRS15
Sophie Bernard, Yves Bertot, Laurence Rideau, Pierre-Yves Strub:
Formal Proofs of Transcendence for e and $π$ as an Application of Multivariate and Symmetric Polynomials. CoRR abs/1512.02791 (2015)
[i7]
- view
  - electronic edition @ iacr.org (open access)
  - details & citations
- export record
  dblp key:
  - journals/iacr/BartheBDFGS15
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/iacr/BartheBDFGS15
Gilles Barthe, Sonia Belaïd, François Dupressoir, Pierre-Alain Fouque, Benjamin Grégoire, Pierre-Yves Strub:
Verified Proofs of Higher-Order Masking. IACR Cryptol. ePrint Arch. 2015: 60 (2015)
2014
[i6]
- view
  - electronic edition @ arxiv.org (open access)
  - details & citations
- export record
  dblp key:
  - journals/corr/BartheGAHKS14
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/corr/BartheGAHKS14
Gilles Barthe, Marco Gaboardi, Emilio Jesús Gallego Arias, Justin Hsu, César Kunz, Pierre-Yves Strub:
Proving differential privacy in Hoare logic. CoRR abs/1407.2988 (2014)
[i5]
- view
  - electronic edition @ arxiv.org (open access)
  - details & citations
- export record
  dblp key:
  - journals/corr/BartheGAHRS14
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/corr/BartheGAHRS14
Gilles Barthe, Marco Gaboardi, Emilio Jesús Gallego Arias, Justin Hsu, Aaron Roth, Pierre-Yves Strub:
Higher-Order Approximate Relational Refinement Types for Mechanism Design and Differential Privacy. CoRR abs/1407.6845 (2014)
[i4]
- view
  - electronic edition @ iacr.org (open access)
  - details & citations
- export record
  dblp key:
  - journals/iacr/BhargavanFKPSB14
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/iacr/BhargavanFKPSB14
Karthikeyan Bhargavan, Cédric Fournet, Markulf Kohlweiss, Alfredo Pironti, Pierre-Yves Strub, Santiago Zanella Béguelin:
Proving the TLS Handshake Secure (as it is). IACR Cryptol. ePrint Arch. 2014: 182 (2014)
[i3]
- view
  - electronic edition @ iacr.org (open access)
  - details & citations
- export record
  dblp key:
  - journals/iacr/AlmeidaBBDDGS14
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/iacr/AlmeidaBBDDGS14
José Bacelar Almeida, Manuel Barbosa, Gilles Barthe, Guillaume Davy, François Dupressoir, Benjamin Grégoire, Pierre-Yves Strub:
Verified Implementations for Secure and Verifiable Computation. IACR Cryptol. ePrint Arch. 2014: 456 (2014)
2008
[i2]
- view
  - electronic edition @ arxiv.org (open access)
  - details & citations
- export record
  dblp key:
  - journals/corr/abs-0804-3762
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/corr/abs-0804-3762
Frédéric Blanqui, Jean-Pierre Jouannaud, Pierre-Yves Strub:
From formal proofs to mathematical proofs: a safe, incremental way for building in first-order decision procedures. CoRR abs/0804.3762 (2008)
2007
[i1]
- view
  - electronic edition @ arxiv.org (open access)
  - details & citations
- export record
  dblp key:
  - journals/corr/abs-0707-1266
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/corr/abs-0707-1266
Frédéric Blanqui, Jean-Pierre Jouannaud, Pierre-Yves Strub:
Building Decision Procedures in the Calculus of Inductive Constructions. CoRR abs/0707.1266 (2007)

Coauthor Index

see FAQ

manage site settings

To protect your privacy, all features that rely on external API calls from your browser are turned off by default. You need to opt-in for them to become active. All settings here will be stored as cookies with your web browser. For more information see our F.A.Q.