×
Author ID: strub.pierre-yves Recent zbMATH articles by "Strub, Pierre-Yves"
Published as: Strub, Pierre-Yves
Documents Indexed: 32 Publications since 2007, including 1 Book
Co-Authors: 44 Co-Authors with 30 Joint Publications
1,087 Co-Co-Authors

Publications by Year

Citations contained in zbMATH Open

24 Publications have been cited 154 times in 118 Documents Cited by Year
Verified proofs of higher-order masking. Zbl 1370.94486
Barthe, Gilles; Belaïd, Sonia; Dupressoir, François; Fouque, Pierre-Alain; Grégoire, Benjamin; Strub, Pierre-Yves
21
2015
Parallel implementations of masking schemes and the bounded moment leakage model. Zbl 1411.94050
Barthe, Gilles; Dupressoir, François; Faust, Sebastian; Grégoire, Benjamin; Standaert, François-Xavier; Strub, Pierre-Yves
20
2017
Secure distributed programming with value-dependent types. Zbl 1323.68229
Swamy, Nikhil; Chen, Juan; Fournet, Cédric; Strub, Pierre-Yves; Bhargavan, Karthikeyan; Yang, Jean
14
2011
Proving the TLS handshake secure (as it is). Zbl 1334.94060
Bhargavan, Karthikeyan; Fournet, Cédric; Kohlweiss, Markulf; Pironti, Alfredo; Strub, Pierre-Yves; Zanella-Béguelin, Santiago
14
2014
Probabilistic relational verification for cryptographic implementations. Zbl 1284.68380
Barthe, Gilles; Fournet, Cédric; Grégoire, Benjamin; Strub, Pierre-Yves; Swamy, Nikhil; Zanella-Béguelin, Santiago
12
2014
Proving differential privacy via probabilistic couplings. Zbl 1401.68184
Barthe, Gilles; Gaboardi, Marco; Grégoire, Benjamin; Hsu, Justin; Strub, Pierre-Yves
11
2016
Dependent types and multi-monadic effects in \(\mathrm{F}^*\). Zbl 1347.68038
Swamy, Nikhil; Hriţcu, Cătălin; Keller, Chantal; Rastogi, Aseem; Delignat-Lavaud, Antoine; Forest, Simon; Bhargavan, Karthikeyan; Fournet, Cédric; Strub, Pierre-Yves; Kohlweiss, Markulf; Zinzindohoue, Jean-Karim; Zanella-Béguelin, Santiago
10
2016
Higher-order approximate relational refinement types for mechanism design and differential privacy. Zbl 1346.68058
Barthe, Gilles; Gaboardi, Marco; Gallego Arias, Emilio Jesús; Hsu, Justin; Roth, Aaron; Strub, Pierre-Yves
9
2015
Secure distributed programming with value-dependent types. Zbl 1290.68033
Swamy, Nikhil; Chen, Juan; Fournet, Cédric; Strub, Pierre-Yves; Bhargavan, Karthikeyan; Yang, Jean
8
2013
EasyCrypt: a tutorial. Zbl 1448.68184
Barthe, Gilles; Dupressoir, François; Grégoire, Benjamin; Kunz, César; Schmidt, Benedikt; Strub, Pierre-Yves
5
2014
Coq Modulo Theory. Zbl 1287.68154
Strub, Pierre-Yves
4
2010
Coupling proofs are probabilistic product programs. Zbl 1380.68267
Barthe, Gilles; Grégoire, Benjamin; Hsu, Justin; Strub, Pierre-Yves
4
2017
Fully abstract compilation to JavaScript. Zbl 1301.68100
Fournet, Cedric; Swamy, Nikhil; Chen, Juan; Dagand, Pierre-Evariste; Strub, Pierre-Yves; Livshits, Benjamin
4
2013
A formal library for elliptic curves in the Coq proof assistant. Zbl 1416.68150
Bartzia, Evmorfia-Iro; Strub, Pierre-Yves
3
2014
Building decision procedures in the calculus of inductive constructions. Zbl 1179.68135
Blanqui, Frédéric; Jouannaud, Jean-Pierre; Strub, Pierre-Yves
2
2007
A program logic for union bounds. Zbl 1388.68022
Barthe, Gilles; Gaboardi, Marco; Grégoire, Benjamin; Hsu, Justin; Strub, Pierre-Yves
2
2016
Gradual typing embedded securely in JavaScript. Zbl 1284.68108
Swamy, Nikhil; Fournet, Cedric; Rastogi, Aseem; Bhargavan, Karthikeyan; Chen, Juan; Strub, Pierre-Yves; Bierman, Gavin
2
2014
An assertion-based program logic for probabilistic programs. Zbl 1418.68049
Barthe, Gilles; Espitau, Thomas; Gaboardi, Marco; Grégoire, Benjamin; Hsu, Justin; Strub, Pierre-Yves
2
2018
\(*\)-liftings for differential privacy. Zbl 1442.68100
Barthe, Gilles; Espitau, Thomas; Hsu, Justin; Sato, Tetsuya; Strub, Pierre-Yves
2
2017
Relational reasoning via probabilistic coupling. Zbl 1471.68127
Barthe, Gilles; Espitau, Thomas; Grégoire, Benjamin; Hsu, Justin; Stefanesco, Léo; Strub, Pierre-Yves
1
2015
Self-certification: bootstrapping certified typecheckers in F\(^\ast\) with Coq. Zbl 1321.68205
Strub, Pierre-Yves; Swamy, Nikhil; Fournet, Cedric; Chen, Juan
1
2012
Coq without type casts: a complete proof of Coq Modulo Theory. Zbl 1403.68227
Jouannaud, Jean-Pierre; Strub, Pierre-Yves
1
2017
Formal verification of Saber’s public-key encryption scheme in easycrypt. Zbl 1516.94035
Hülsing, Andreas; Meijers, Matthias; Strub, Pierre-Yves
1
2022
Unsolvability of the quintic formalized in dependent type theory. Zbl 07699425
Bernard, Sophie; Cohen, Cyril; Mahboubi, Assia; Strub, Pierre-Yves
1
2021
Formal verification of Saber’s public-key encryption scheme in easycrypt. Zbl 1516.94035
Hülsing, Andreas; Meijers, Matthias; Strub, Pierre-Yves
1
2022
Unsolvability of the quintic formalized in dependent type theory. Zbl 07699425
Bernard, Sophie; Cohen, Cyril; Mahboubi, Assia; Strub, Pierre-Yves
1
2021
An assertion-based program logic for probabilistic programs. Zbl 1418.68049
Barthe, Gilles; Espitau, Thomas; Gaboardi, Marco; Grégoire, Benjamin; Hsu, Justin; Strub, Pierre-Yves
2
2018
Parallel implementations of masking schemes and the bounded moment leakage model. Zbl 1411.94050
Barthe, Gilles; Dupressoir, François; Faust, Sebastian; Grégoire, Benjamin; Standaert, François-Xavier; Strub, Pierre-Yves
20
2017
Coupling proofs are probabilistic product programs. Zbl 1380.68267
Barthe, Gilles; Grégoire, Benjamin; Hsu, Justin; Strub, Pierre-Yves
4
2017
\(*\)-liftings for differential privacy. Zbl 1442.68100
Barthe, Gilles; Espitau, Thomas; Hsu, Justin; Sato, Tetsuya; Strub, Pierre-Yves
2
2017
Coq without type casts: a complete proof of Coq Modulo Theory. Zbl 1403.68227
Jouannaud, Jean-Pierre; Strub, Pierre-Yves
1
2017
Proving differential privacy via probabilistic couplings. Zbl 1401.68184
Barthe, Gilles; Gaboardi, Marco; Grégoire, Benjamin; Hsu, Justin; Strub, Pierre-Yves
11
2016
Dependent types and multi-monadic effects in \(\mathrm{F}^*\). Zbl 1347.68038
Swamy, Nikhil; Hriţcu, Cătălin; Keller, Chantal; Rastogi, Aseem; Delignat-Lavaud, Antoine; Forest, Simon; Bhargavan, Karthikeyan; Fournet, Cédric; Strub, Pierre-Yves; Kohlweiss, Markulf; Zinzindohoue, Jean-Karim; Zanella-Béguelin, Santiago
10
2016
A program logic for union bounds. Zbl 1388.68022
Barthe, Gilles; Gaboardi, Marco; Grégoire, Benjamin; Hsu, Justin; Strub, Pierre-Yves
2
2016
Verified proofs of higher-order masking. Zbl 1370.94486
Barthe, Gilles; Belaïd, Sonia; Dupressoir, François; Fouque, Pierre-Alain; Grégoire, Benjamin; Strub, Pierre-Yves
21
2015
Higher-order approximate relational refinement types for mechanism design and differential privacy. Zbl 1346.68058
Barthe, Gilles; Gaboardi, Marco; Gallego Arias, Emilio Jesús; Hsu, Justin; Roth, Aaron; Strub, Pierre-Yves
9
2015
Relational reasoning via probabilistic coupling. Zbl 1471.68127
Barthe, Gilles; Espitau, Thomas; Grégoire, Benjamin; Hsu, Justin; Stefanesco, Léo; Strub, Pierre-Yves
1
2015
Proving the TLS handshake secure (as it is). Zbl 1334.94060
Bhargavan, Karthikeyan; Fournet, Cédric; Kohlweiss, Markulf; Pironti, Alfredo; Strub, Pierre-Yves; Zanella-Béguelin, Santiago
14
2014
Probabilistic relational verification for cryptographic implementations. Zbl 1284.68380
Barthe, Gilles; Fournet, Cédric; Grégoire, Benjamin; Strub, Pierre-Yves; Swamy, Nikhil; Zanella-Béguelin, Santiago
12
2014
EasyCrypt: a tutorial. Zbl 1448.68184
Barthe, Gilles; Dupressoir, François; Grégoire, Benjamin; Kunz, César; Schmidt, Benedikt; Strub, Pierre-Yves
5
2014
A formal library for elliptic curves in the Coq proof assistant. Zbl 1416.68150
Bartzia, Evmorfia-Iro; Strub, Pierre-Yves
3
2014
Gradual typing embedded securely in JavaScript. Zbl 1284.68108
Swamy, Nikhil; Fournet, Cedric; Rastogi, Aseem; Bhargavan, Karthikeyan; Chen, Juan; Strub, Pierre-Yves; Bierman, Gavin
2
2014
Secure distributed programming with value-dependent types. Zbl 1290.68033
Swamy, Nikhil; Chen, Juan; Fournet, Cédric; Strub, Pierre-Yves; Bhargavan, Karthikeyan; Yang, Jean
8
2013
Fully abstract compilation to JavaScript. Zbl 1301.68100
Fournet, Cedric; Swamy, Nikhil; Chen, Juan; Dagand, Pierre-Evariste; Strub, Pierre-Yves; Livshits, Benjamin
4
2013
Self-certification: bootstrapping certified typecheckers in F\(^\ast\) with Coq. Zbl 1321.68205
Strub, Pierre-Yves; Swamy, Nikhil; Fournet, Cedric; Chen, Juan
1
2012
Secure distributed programming with value-dependent types. Zbl 1323.68229
Swamy, Nikhil; Chen, Juan; Fournet, Cédric; Strub, Pierre-Yves; Bhargavan, Karthikeyan; Yang, Jean
14
2011
Coq Modulo Theory. Zbl 1287.68154
Strub, Pierre-Yves
4
2010
Building decision procedures in the calculus of inductive constructions. Zbl 1179.68135
Blanqui, Frédéric; Jouannaud, Jean-Pierre; Strub, Pierre-Yves
2
2007
all top 5

Cited by 302 Authors

10 Barthe, Gilles
8 Standaert, Francois-Xavier
6 Jager, Tibor
5 Rivain, Matthieu
4 Belaïd, Sonia
4 Gaboardi, Marco
4 Grégoire, Benjamin
4 Lochbihler, Andreas
4 Sato, Tetsuya
4 Strub, Pierre-Yves
3 Brzuska, Chris
3 Cassiers, Gaëtan
3 Chatterjee, Krishnendu
3 Dezani-Ciancaglini, Mariangiola
3 Dupressoir, François
3 Faust, Sebastian
3 Fournet, Cédric
3 Guilley, Sylvain
3 Günther, Felix
3 Momin, Charles
3 Taleb, Abdul Rahman
3 Thiemann, Peter J.
2 Barbosa, Manuel
2 Batz, Kevin
2 Bhargavan, Karthikeyan
2 Caires, Luís
2 Coppo, Mario
2 Coron, Jean-Sébastien
2 Dagand, Pierre-Evariste
2 Danger, Jean-Luc
2 Delignat-Lavaud, Antoine
2 Diemert, Denis
2 Dowling, Benjamin
2 Espitau, Thomas
2 Goudarzi, Dahmun
2 Hale, Britta
2 Hoffmann, Clément
2 Hsu, Justin
2 Katoen, Joost-Pieter
2 Katsumata, Shin-ya
2 Kobayashi, Naoki
2 Kohbrok, Konrad
2 Kohlweiss, Markulf
2 Lauer, Sebastian
2 Lepigre, Rodolphe
2 Liu, Depeng
2 Méaux, Pierrick
2 Norrish, Michael
2 Novotný, Petr
2 Orchard, Dominic A.
2 Padovani, Luca
2 Pichardie, David
2 Primas, Robert
2 Schwabe, Peter
2 Schwenk, Jorg
2 Stebila, Douglas
2 Toninho, Bernardo
2 Wadler, Philip Lee
2 Wang, Bow-Yaw
2 Ying, Mingsheng
2 Yoshida, Nobuko
2 Zdancewic, Steve
2 Zhang, Lijun
2 Žikelić, {D}or{d}e
1 Aviram, Nimrod
1 Bacelar Almeida, José
1 Baillot, Patrick
1 Bartoletti, Massimo
1 Basin, David A.
1 Benveniste, Albert
1 Berndt, Sebastian
1 Betarte, Gustavo
1 Beyne, Tim
1 Bi, Xuan
1 Bichhawat, Abhishek
1 Biewer, Sebastian
1 Blanqui, Frédéric
1 Bloem, Roderick
1 Blot, Arthur
1 Boldyreva, Alexandra
1 Bordes, Nicolas
1 Brázdil, Tomáš
1 Breitner, Joachim
1 Bruneau, Nicolas
1 Bugliesi, Michele
1 Burel, Guillaume
1 Bury, Guillaume
1 Buzzard, Kevin
1 Calzavara, Stefano
1 Campo, Juan Diego
1 Carette, Jacques
1 Carlet, Claude
1 Castellani, Ilaria
1 Cauderlier, Raphaël
1 Chakravarty, Manuel M. T.
1 Chan, Hing-Lun
1 Chen, Shan
1 Chen, Yulong
1 Cheng, Wei
1 Chong, Stephen
...and 202 more Authors

Citations by Year