default search action
Google
Google Scholar
Semantic Scholar
Internet Archive Scholar
CiteSeerX
ORCIDPierre-Yves Strub
Person information
Refine list
refinements active!
zoomed in on ?? of ?? records
view refined list in
export refined list as
showing all ?? records
2020 – today
- 2024
[c55]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]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]Bruno Blanchet, Pierre Boutry, Christian Doczkal, Benjamin Grégoire, Pierre-Yves Strub:
CV2EC: Getting the Best of Both Worlds. CSF 2024: 279-294 - [i38]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]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
- [j11]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]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]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) - [c52]Xavier Allamigeon, Quentin Canu, Pierre-Yves Strub:
A Formal Disproof of Hirsch Conjecture. CPP 2023: 17-29 - [c51]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 - [i36]Xavier Allamigeon, Quentin Canu, Pierre-Yves Strub:
A Formal Disproof of the Hirsch Conjecture. CoRR abs/2301.04060 (2023) - [i35]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]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
- [j8]Xavier Allamigeon, Ricardo D. Katz, Pierre-Yves Strub:
Formalizing the Face Lattice of Polyhedra. Log. Methods Comput. Sci. 18(2) (2022) - [c50]Pablo Donato, Pierre-Yves Strub, Benjamin Werner:
A drag-and-drop proof tactic. CPP 2022: 197-209 - [c49]Andreas Hülsing, Matthias Meijers, Pierre-Yves Strub:
Formal Verification of Saber's Public-Key Encryption Scheme in EasyCrypt. CRYPTO (1) 2022: 622-653 - [i33]Li Zhou, Gilles Barthe, Pierre-Yves Strub, Junyi Liu, Mingsheng Ying:
CoqQ: Foundational Verification of Quantum Programs. CoRR abs/2207.11350 (2022) - [i32]Pablo Donato, Pierre-Yves Strub, Benjamin Werner:
A drag-and-drop proof tactic. CoRR abs/2210.11820 (2022) - [i31]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
- [c48]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]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]Sophie Bernard, Cyril Cohen, Assia Mahboubi, Pierre-Yves Strub:
Unsolvability of the Quintic Formalized in Dependent Type Theory. ITP 2021: 8:1-8:18 - [i30]Xavier Allamigeon, Ricardo D. Katz, Pierre-Yves Strub:
Formalizing the Face Lattice of Polyhedra. CoRR abs/2104.15021 (2021) - [i29]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]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) - 2020
- [j7]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) - [c45]Xavier Allamigeon, Ricardo D. Katz, Pierre-Yves Strub:
Formalizing the Face Lattice of Polyhedra. IJCAR (2) 2020: 185-203 - [c44]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
2010 – 2019
- 2019
- [j6]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]Gilles Barthe, Thomas Espitau, Justin Hsu, Tetsuya Sato, Pierre-Yves Strub:
Relational ⋆⋆\star-Liftings for Differential Privacy. Log. Methods Comput. Sci. 15(4) (2019) - [c43]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]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]Gilles Barthe, Benjamin Grégoire, Charlie Jacomme, Steve Kremer, Pierre-Yves Strub:
Symbolic Methods in Computational Cryptography Proofs. CSF 2019: 136-151 - [i27]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]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]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
- [j4]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) - [c40]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]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]Karthikeyan Bhargavan, Franziskus Kiefer, Pierre-Yves Strub:
hacspec: Towards Verifiable Crypto Standards. SSR 2018: 1-20 - [i24]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]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]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]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
- [j3]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]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) - [c37]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]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]Gilles Barthe, Thomas Espitau, Justin Hsu, Tetsuya Sato, Pierre-Yves Strub:
*-Liftings for Differential Privacy. ICALP 2017: 102:1-102:12 - [c34]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]Jean-Pierre Jouannaud, Pierre-Yves Strub:
Coq without Type Casts: A Complete Proof of Coq Modulo Theory. LPAR 2017: 474-489 - [c32]Gilles Barthe, Benjamin Grégoire, Justin Hsu, Pierre-Yves Strub:
Coupling proofs are probabilistic product programs. POPL 2017: 161-174 - [c31]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 - [i20]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]Alejandro Aguirre, Gilles Barthe, Marco Gaboardi, Deepak Garg, Pierre-Yves Strub:
A Relational Logic for Higher-Order Programs. CoRR abs/1703.05042 (2017) - [i18]Gilles Barthe, Thomas Espitau, Justin Hsu, Tetsuya Sato, Pierre-Yves Strub:
*-Liftings for Differential Privacy. CoRR abs/1705.00133 (2017) - [i17]Gilles Barthe, Thomas Espitau, Benjamin Grégoire, Justin Hsu, Pierre-Yves Strub:
Proving Expected Sensitivity of Probabilistic Programs. CoRR abs/1708.02537 (2017) - 2016
- [c30]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]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]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]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]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]Gilles Barthe, Marco Gaboardi, Benjamin Grégoire, Justin Hsu, Pierre-Yves Strub:
Proving Differential Privacy via Probabilistic Couplings. LICS 2016: 749-758 - [c24]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]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 - [i16]Gilles Barthe, Marco Gaboardi, Benjamin Grégoire, Justin Hsu, Pierre-Yves Strub:
Proving Differential Privacy via Probabilistic Couplings. CoRR abs/1601.05047 (2016) - [i15]Gilles Barthe, Marco Gaboardi, Benjamin Grégoire, Justin Hsu, Pierre-Yves Strub:
A program logic for union bounds. CoRR abs/1602.05681 (2016) - [i14]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]Gilles Barthe, Marco Gaboardi, Benjamin Grégoire, Justin Hsu, Pierre-Yves Strub:
Advanced Probabilistic Couplings for Differential Privacy. CoRR abs/1606.07143 (2016) - [i12]Gilles Barthe, Benjamin Grégoire, Justin Hsu, Pierre-Yves Strub:
Coupling proofs are probabilistic product programs. CoRR abs/1607.03455 (2016) - [i11]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
- [c22]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]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]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]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 - [i10]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]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]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]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
- [c18]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]Joseph A. Akinyele, Gilles Barthe, Benjamin Grégoire, Benedikt Schmidt, Pierre-Yves Strub:
Certified Synthesis of Efficient Batch Verifiers. CSF 2014: 153-165 - [c16]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]Evmorfia-Iro Bartzia, Pierre-Yves Strub:
A Formal Library for Elliptic Curves in the Coq Proof Assistant. ITP 2014: 77-92 - [c14]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]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]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 - [i6]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]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]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]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) - 2013
- [j1]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) - [c11]Gilles Barthe, François Dupressoir, Benjamin Grégoire, César Kunz, Benedikt Schmidt, Pierre-Yves Strub:
EasyCrypt: A Tutorial. FOSAD 2013: 146-166 - [c10]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]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]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]Cédric Fournet, Markulf Kohlweiss, Pierre-Yves Strub:
Modular code-based cryptographic verification. CCS 2011: 341-350 - [c6]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]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]Pierre-Yves Strub:
Coq Modulo Theory. CSL 2010: 529-543
2000 – 2009
- 2008
- [b1]Pierre-Yves Strub:
Type Theory and Decision Procedures. (Théorie des Types et Procédures de Décision). École Polytechnique, Palaiseau, France, 2008 - [c3]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 - [i2]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
- [c2]Frédéric Blanqui, Jean-Pierre Jouannaud, Pierre-Yves Strub:
Building Decision Procedures in the Calculus of Inductive Constructions. CSL 2007: 328-342 - [i1]Frédéric Blanqui, Jean-Pierre Jouannaud, Pierre-Yves Strub:
Building Decision Procedures in the Calculus of Inductive Constructions. CoRR abs/0707.1266 (2007) - 2001
- [c1]Thierry Géraud, Pierre-Yves Strub, Jérôme Darbon:
Color image segmentation based on automatic morphological clustering. ICIP (3) 2001: 70-73
Coauthor Index
[c54] [i38] [j11] [j10] [j9] [i35] [i33] [c48] [c47] [i29] [i28] [j7] [c44] [j6] [j5] [c43] [c42] [c41] [i27] [i26] [i25] [j4] [c39] [i24] [i21] [j2] [c37] [c36] [c35] [c34] [c32] [i20] [i19] [i18] [i17] [c30] [c29] [c28] [c26] [c25] [c23] [i16] [i15] [i14] [i13] [i12] [i11] [c22] [c21] [c20] [i10] [i9] [i7] [c17] [c16] [c14] [i6] [i5] [i3] [c11]
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.
Unpaywalled article links
Add open access links from 
to the list of external document links (if available).
Privacy notice: By enabling the option above, your browser will contact the API of unpaywall.org to load hyperlinks to open access articles. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Unpaywall privacy policy.
Archived links via Wayback Machine
For web page which are no longer available, try to retrieve content from the 
of the Internet Archive (if available).
Privacy notice: By enabling the option above, your browser will contact the API of archive.org to check for archived content of web pages that are no longer available. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Internet Archive privacy policy.
Reference lists
Add a list of references from 
, 
, and 
to record detail pages.
load references from crossref.org and opencitations.net
Privacy notice: By enabling the option above, your browser will contact the APIs of crossref.org, opencitations.net, and semanticscholar.org to load article reference information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Crossref privacy policy and the OpenCitations privacy policy, as well as the AI2 Privacy Policy covering Semantic Scholar.
Citation data
Add a list of citing articles from and to record detail pages.
load citations from opencitations.net
Privacy notice: By enabling the option above, your browser will contact the API of opencitations.net and semanticscholar.org to load citation information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the OpenCitations privacy policy as well as the AI2 Privacy Policy covering Semantic Scholar.
OpenAlex data
Load additional information about publications from 
.
Privacy notice: By enabling the option above, your browser will contact the API of openalex.org to load additional information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the information given by OpenAlex.
last updated on 2024-12-02 22:27 CET by the dblp team
all metadata released as open data under CC0 1.0 license
see also: Terms of Use | Privacy Policy | Imprint
dblp was originally created in 1993 at:
since 2018, dblp has been operated and maintained by:
the dblp computer science bibliography is funded and supported by:
