BibTeX records: Pierre-Yves Strub

download as .bib file

@inproceedings{DBLP:conf/itp/BernardCMS21,
  author    = {Sophie Bernard and
               Cyril Cohen and
               Assia Mahboubi and
               Pierre{-}Yves Strub},
  title     = {Unsolvability of the Quintic Formalized in Dependent Type Theory},
  booktitle = {{ITP}},
  series    = {LIPIcs},
  volume    = {193},
  pages     = {8:1--8:18},
  publisher = {Schloss Dagstuhl - Leibniz-Zentrum f{\"{u}}r Informatik},
  year      = {2021}
}
@article{DBLP:journals/corr/abs-2104-15021,
  author    = {Xavier Allamigeon and
               Ricardo D. Katz and
               Pierre{-}Yves Strub},
  title     = {Formalizing the Face Lattice of Polyhedra},
  journal   = {CoRR},
  volume    = {abs/2104.15021},
  year      = {2021}
}
@article{DBLP:journals/iacr/BarbosaBGKS21,
  author    = {Manuel Barbosa and
               Gilles Barthe and
               Benjamin Gr{\'{e}}goire and
               Adrien Koutsos and
               Pierre{-}Yves Strub},
  title     = {Mechanized Proofs of Adversarial Complexity and Application to Universal
               Composability},
  journal   = {{IACR} Cryptol. ePrint Arch.},
  pages     = {156},
  year      = {2021}
}
@article{DBLP:journals/jce/BartheBDFGSS20,
  author    = {Gilles Barthe and
               Sonia Bela{\"{\i}}d and
               Fran{\c{c}}ois Dupressoir and
               Pierre{-}Alain Fouque and
               Benjamin Gr{\'{e}}goire and
               Fran{\c{c}}ois{-}Xavier Standaert and
               Pierre{-}Yves Strub},
  title     = {Improved parallel mask refreshing algorithms: generic solutions with
               parametrized non-interference and automated optimizations},
  journal   = {J. Cryptogr. Eng.},
  volume    = {10},
  number    = {1},
  pages     = {17--26},
  year      = {2020}
}
@inproceedings{DBLP:conf/cade/AllamigeonKS20,
  author    = {Xavier Allamigeon and
               Ricardo D. Katz and
               Pierre{-}Yves Strub},
  title     = {Formalizing the Face Lattice of Polyhedra},
  booktitle = {{IJCAR} {(2)}},
  series    = {Lecture Notes in Computer Science},
  volume    = {12167},
  pages     = {185--203},
  publisher = {Springer},
  year      = {2020}
}
@inproceedings{DBLP:conf/sp/AlmeidaBBGKL0S20,
  author    = {Jos{\'{e}} Bacelar Almeida and
               Manuel Barbosa and
               Gilles Barthe and
               Benjamin Gr{\'{e}}goire and
               Adrien Koutsos and
               Vincent Laporte and
               Tiago Oliveira and
               Pierre{-}Yves Strub},
  title     = {The Last Mile: High-Assurance and High-Speed Cryptographic Implementations},
  booktitle = {{IEEE} Symposium on Security and Privacy},
  pages     = {965--982},
  publisher = {{IEEE}},
  year      = {2020}
}
@article{DBLP:journals/jfp/AguirreBGGS19,
  author    = {Alejandro Aguirre and
               Gilles Barthe and
               Marco Gaboardi and
               Deepak Garg and
               Pierre{-}Yves Strub},
  title     = {A relational logic for higher-order programs},
  journal   = {J. Funct. Program.},
  volume    = {29},
  pages     = {e16},
  year      = {2019}
}
@article{DBLP:journals/lmcs/BartheEHSS19,
  author    = {Gilles Barthe and
               Thomas Espitau and
               Justin Hsu and
               Tetsuya Sato and
               Pierre{-}Yves Strub},
  title     = {Relational {\(\star\)}{\(\star\)}{\textbackslash}star-Liftings for
               Differential Privacy},
  journal   = {Log. Methods Comput. Sci.},
  volume    = {15},
  number    = {4},
  year      = {2019}
}
@inproceedings{DBLP:conf/ccs/AlmeidaBBCCGPPS19,
  author    = {Jos{\'{e}} Bacelar Almeida and
               Manuel Barbosa and
               Gilles Barthe and
               Matthew Campagna and
               Ernie Cohen and
               Benjamin Gr{\'{e}}goire and
               Vitor Pereira and
               Bernardo Portela and
               Pierre{-}Yves Strub and
               Serdar Tasiran},
  title     = {A Machine-Checked Proof of Security for {AWS} Key Management Service},
  booktitle = {{CCS}},
  pages     = {63--78},
  publisher = {{ACM}},
  year      = {2019}
}
@inproceedings{DBLP:conf/ccs/AlmeidaBBBDGL0S19,
  author    = {Jos{\'{e}} Bacelar Almeida and
               C{\'{e}}cile Baritel{-}Ruet and
               Manuel Barbosa and
               Gilles Barthe and
               Fran{\c{c}}ois Dupressoir and
               Benjamin Gr{\'{e}}goire and
               Vincent Laporte and
               Tiago Oliveira and
               Alley Stoughton and
               Pierre{-}Yves Strub},
  title     = {Machine-Checked Proofs for Cryptographic Standards: Indifferentiability
               of Sponge and Secure High-Assurance Implementations of {SHA-3}},
  booktitle = {{CCS}},
  pages     = {1607--1622},
  publisher = {{ACM}},
  year      = {2019}
}
@inproceedings{DBLP:conf/csfw/BartheGJKS19,
  author    = {Gilles Barthe and
               Benjamin Gr{\'{e}}goire and
               Charlie Jacomme and
               Steve Kremer and
               Pierre{-}Yves Strub},
  title     = {Symbolic Methods in Computational Cryptography Proofs},
  booktitle = {{CSF}},
  pages     = {136--151},
  publisher = {{IEEE}},
  year      = {2019}
}
@article{DBLP:journals/corr/abs-1904-04606,
  author    = {Jos{\'{e}} Bacelar Almeida and
               Manuel Barbosa and
               Gilles Barthe and
               Benjamin Gr{\'{e}}goire and
               Adrien Koutsos and
               Vincent Laporte and
               Tiago Oliveira and
               Pierre{-}Yves Strub},
  title     = {The Last Mile: High-Assurance and High-Speed Cryptographic Implementations},
  journal   = {CoRR},
  volume    = {abs/1904.04606},
  year      = {2019}
}
@article{DBLP:journals/iacr/AlmeidaBBCCGPPS19,
  author    = {Jos{\'{e}} Bacelar Almeida and
               Manuel Barbosa and
               Gilles Barthe and
               Matthew Campagna and
               Ernie Cohen and
               Benjamin Gr{\'{e}}goire and
               Vitor Pereira and
               Bernardo Portela and
               Pierre{-}Yves Strub and
               Serdar Tasiran},
  title     = {A Machine-Checked Proof of Security for {AWS} Key Management Service},
  journal   = {{IACR} Cryptol. ePrint Arch.},
  pages     = {1042},
  year      = {2019}
}
@article{DBLP:journals/iacr/AlmeidaBBBDGLOS19,
  author    = {Jos{\'{e}} Bacelar Almeida and
               C{\'{e}}cile Baritel{-}Ruet and
               Manuel Barbosa and
               Gilles Barthe and
               Fran{\c{c}}ois Dupressoir and
               Benjamin Gr{\'{e}}goire and
               Vincent Laporte and
               Tiago Oliveira and
               Alley Stoughton and
               Pierre{-}Yves Strub},
  title     = {Machine-Checked Proofs for Cryptographic Standards},
  journal   = {{IACR} Cryptol. ePrint Arch.},
  pages     = {1155},
  year      = {2019}
}
@article{DBLP:journals/pacmpl/BartheEGHS18,
  author    = {Gilles Barthe and
               Thomas Espitau and
               Benjamin Gr{\'{e}}goire and
               Justin Hsu and
               Pierre{-}Yves Strub},
  title     = {Proving expected sensitivity of probabilistic programs},
  journal   = {Proc. {ACM} Program. Lang.},
  volume    = {2},
  number    = {{POPL}},
  pages     = {57:1--57:29},
  year      = {2018}
}
@inproceedings{DBLP:conf/csfw/HaaghKOSS18,
  author    = {Helene Haagh and
               Aleksandr Karbyshev and
               Sabine Oechsner and
               Bas Spitters and
               Pierre{-}Yves Strub},
  title     = {Computer-Aided Proofs for Multiparty Computation with Active Security},
  booktitle = {{CSF}},
  pages     = {119--131},
  publisher = {{IEEE} Computer Society},
  year      = {2018}
}
@inproceedings{DBLP:conf/esop/BartheEGGHS18,
  author    = {Gilles Barthe and
               Thomas Espitau and
               Marco Gaboardi and
               Benjamin Gr{\'{e}}goire and
               Justin Hsu and
               Pierre{-}Yves Strub},
  title     = {An Assertion-Based Program Logic for Probabilistic Programs},
  booktitle = {{ESOP}},
  series    = {Lecture Notes in Computer Science},
  volume    = {10801},
  pages     = {117--144},
  publisher = {Springer},
  year      = {2018}
}
@inproceedings{DBLP:conf/secsr/BhargavanKS18,
  author    = {Karthikeyan Bhargavan and
               Franziskus Kiefer and
               Pierre{-}Yves Strub},
  title     = {hacspec: Towards Verifiable Crypto Standards},
  booktitle = {{SSR}},
  series    = {Lecture Notes in Computer Science},
  volume    = {11322},
  pages     = {1--20},
  publisher = {Springer},
  year      = {2018}
}
@article{DBLP:journals/corr/abs-1803-05535,
  author    = {Gilles Barthe and
               Thomas Espitau and
               Marco Gaboardi and
               Benjamin Gr{\'{e}}goire and
               Justin Hsu and
               Pierre{-}Yves Strub},
  title     = {An Assertion-Based Program Logic for Probabilistic Programs},
  journal   = {CoRR},
  volume    = {abs/1803.05535},
  year      = {2018}
}
@article{DBLP:journals/corr/abs-1806-07197,
  author    = {Helene Haagh and
               Aleksandr Karbyshev and
               Sabine Oechsner and
               Bas Spitters and
               Pierre{-}Yves Strub},
  title     = {Computer-aided proofs for multiparty computation with active security},
  journal   = {CoRR},
  volume    = {abs/1806.07197},
  year      = {2018}
}
@article{DBLP:journals/iacr/HaaghKOSS18,
  author    = {Helene Haagh and
               Aleksandr Karbyshev and
               Sabine Oechsner and
               Bas Spitters and
               Pierre{-}Yves Strub},
  title     = {Computer-aided proofs for multiparty computation with active security},
  journal   = {{IACR} Cryptol. ePrint Arch.},
  pages     = {502},
  year      = {2018}
}
@article{DBLP:journals/iacr/BartheBDFGSS18,
  author    = {Gilles Barthe and
               Sonia Bela{\"{\i}}d and
               Fran{\c{c}}ois Dupressoir and
               Pierre{-}Alain Fouque and
               Benjamin Gr{\'{e}}goire and
               Fran{\c{c}}ois{-}Xavier Standaert and
               Pierre{-}Yves Strub},
  title     = {Improved Parallel Mask Refreshing Algorithms: Generic Solutions with
               Parametrized Non-Interference {\&} Automated Optimizations},
  journal   = {{IACR} Cryptol. ePrint Arch.},
  pages     = {505},
  year      = {2018}
}
@article{DBLP:journals/cacm/BeurdoucheBDFKP17,
  author    = {Benjamin Beurdouche and
               Karthikeyan Bhargavan and
               Antoine Delignat{-}Lavaud and
               C{\'{e}}dric Fournet and
               Markulf Kohlweiss and
               Alfredo Pironti and
               Pierre{-}Yves Strub and
               Jean Karim Zinzindohoue},
  title     = {A messy state of the union: taming the composite state machines of
               {TLS}},
  journal   = {Commun. {ACM}},
  volume    = {60},
  number    = {2},
  pages     = {99--107},
  year      = {2017}
}
@article{DBLP:journals/pacmpl/AguirreBG0S17,
  author    = {Alejandro Aguirre and
               Gilles Barthe and
               Marco Gaboardi and
               Deepak Garg and
               Pierre{-}Yves Strub},
  title     = {A relational logic for higher-order programs},
  journal   = {Proc. {ACM} Program. Lang.},
  volume    = {1},
  number    = {{ICFP}},
  pages     = {21:1--21:29},
  year      = {2017}
}
@inproceedings{DBLP:conf/ccs/AlmeidaBBBGLOPS17,
  author    = {Jos{\'{e}} Bacelar Almeida and
               Manuel Barbosa and
               Gilles Barthe and
               Arthur Blot and
               Benjamin Gr{\'{e}}goire and
               Vincent Laporte and
               Tiago Oliveira and
               Hugo Pacheco and
               Benedikt Schmidt and
               Pierre{-}Yves Strub},
  title     = {Jasmin: High-Assurance and High-Speed Cryptography},
  booktitle = {{CCS}},
  pages     = {1807--1823},
  publisher = {{ACM}},
  year      = {2017}
}
@inproceedings{DBLP:conf/eurocrypt/BartheDFGSS17,
  author    = {Gilles Barthe and
               Fran{\c{c}}ois Dupressoir and
               Sebastian Faust and
               Benjamin Gr{\'{e}}goire and
               Fran{\c{c}}ois{-}Xavier Standaert and
               Pierre{-}Yves Strub},
  title     = {Parallel Implementations of Masking Schemes and the Bounded Moment
               Leakage Model},
  booktitle = {{EUROCRYPT} {(1)}},
  series    = {Lecture Notes in Computer Science},
  volume    = {10210},
  pages     = {535--566},
  year      = {2017}
}
@inproceedings{DBLP:conf/icalp/BartheEHSS17,
  author    = {Gilles Barthe and
               Thomas Espitau and
               Justin Hsu and
               Tetsuya Sato and
               Pierre{-}Yves Strub},
  title     = {*-Liftings for Differential Privacy},
  booktitle = {{ICALP}},
  series    = {LIPIcs},
  volume    = {80},
  pages     = {102:1--102:12},
  publisher = {Schloss Dagstuhl - Leibniz-Zentrum f{\"{u}}r Informatik},
  year      = {2017}
}
@inproceedings{DBLP:conf/lpar/BartheEGHS17,
  author    = {Gilles Barthe and
               Thomas Espitau and
               Benjamin Gr{\'{e}}goire and
               Justin Hsu and
               Pierre{-}Yves Strub},
  title     = {Proving uniformity and independence by self-composition and coupling},
  booktitle = {{LPAR}},
  series    = {EPiC Series in Computing},
  volume    = {46},
  pages     = {385--403},
  publisher = {EasyChair},
  year      = {2017}
}
@inproceedings{DBLP:conf/lpar/JouannaudS17,
  author    = {Jean{-}Pierre Jouannaud and
               Pierre{-}Yves Strub},
  title     = {Coq without Type Casts: {A} Complete Proof of Coq Modulo Theory},
  booktitle = {{LPAR}},
  series    = {EPiC Series in Computing},
  volume    = {46},
  pages     = {474--489},
  publisher = {EasyChair},
  year      = {2017}
}
@inproceedings{DBLP:conf/popl/BartheGHS17,
  author    = {Gilles Barthe and
               Benjamin Gr{\'{e}}goire and
               Justin Hsu and
               Pierre{-}Yves Strub},
  title     = {Coupling proofs are probabilistic product programs},
  booktitle = {{POPL}},
  pages     = {161--174},
  publisher = {{ACM}},
  year      = {2017}
}
@inproceedings{DBLP:conf/sp/CortierDDSSW17,
  author    = {V{\'{e}}ronique Cortier and
               Constantin Catalin Dragan and
               Fran{\c{c}}ois Dupressoir and
               Benedikt Schmidt and
               Pierre{-}Yves Strub and
               Bogdan Warinschi},
  title     = {Machine-Checked Proofs of Privacy for Electronic Voting Protocols},
  booktitle = {{IEEE} Symposium on Security and Privacy},
  pages     = {993--1008},
  publisher = {{IEEE} Computer Society},
  year      = {2017}
}
@article{DBLP:journals/corr/BartheEGHS17,
  author    = {Gilles Barthe and
               Thomas Espitau and
               Benjamin Gr{\'{e}}goire and
               Justin Hsu and
               Pierre{-}Yves Strub},
  title     = {Proving uniformity and independence by self-composition and coupling},
  journal   = {CoRR},
  volume    = {abs/1701.06477},
  year      = {2017}
}
@article{DBLP:journals/corr/AguirreBG0S17,
  author    = {Alejandro Aguirre and
               Gilles Barthe and
               Marco Gaboardi and
               Deepak Garg and
               Pierre{-}Yves Strub},
  title     = {A Relational Logic for Higher-Order Programs},
  journal   = {CoRR},
  volume    = {abs/1703.05042},
  year      = {2017}
}
@article{DBLP:journals/corr/BartheEHSS17,
  author    = {Gilles Barthe and
               Thomas Espitau and
               Justin Hsu and
               Tetsuya Sato and
               Pierre{-}Yves Strub},
  title     = {*-Liftings for Differential Privacy},
  journal   = {CoRR},
  volume    = {abs/1705.00133},
  year      = {2017}
}
@article{DBLP:journals/corr/abs-1708-02537,
  author    = {Gilles Barthe and
               Thomas Espitau and
               Benjamin Gr{\'{e}}goire and
               Justin Hsu and
               Pierre{-}Yves Strub},
  title     = {Proving Expected Sensitivity of Probabilistic Programs},
  journal   = {CoRR},
  volume    = {abs/1708.02537},
  year      = {2017}
}
@inproceedings{DBLP:conf/ccs/BartheFGGHS16,
  author    = {Gilles Barthe and
               No{\'{e}}mie Fong and
               Marco Gaboardi and
               Benjamin Gr{\'{e}}goire and
               Justin Hsu and
               Pierre{-}Yves Strub},
  title     = {Advanced Probabilistic Couplings for Differential Privacy},
  booktitle = {{CCS}},
  pages     = {55--67},
  publisher = {{ACM}},
  year      = {2016}
}
@inproceedings{DBLP:conf/ccs/BartheFGAGHS16,
  author    = {Gilles Barthe and
               Gian Pietro Farina and
               Marco Gaboardi and
               Emilio Jes{\'{u}}s Gallego Arias and
               Andy Gordon and
               Justin Hsu and
               Pierre{-}Yves Strub},
  title     = {Differentially Private Bayesian Programming},
  booktitle = {{CCS}},
  pages     = {68--79},
  publisher = {{ACM}},
  year      = {2016}
}
@inproceedings{DBLP:conf/ccs/BartheBDFGSZ16,
  author    = {Gilles Barthe and
               Sonia Bela{\"{\i}}d and
               Fran{\c{c}}ois Dupressoir and
               Pierre{-}Alain Fouque and
               Benjamin Gr{\'{e}}goire and
               Pierre{-}Yves Strub and
               R{\'{e}}becca Zucchini},
  title     = {Strong Non-Interference and Type-Directed Higher-Order Masking},
  booktitle = {{CCS}},
  pages     = {116--129},
  publisher = {{ACM}},
  year      = {2016}
}
@inproceedings{DBLP:conf/cpp/BernardBRS16,
  author    = {Sophie Bernard and
               Yves Bertot and
               Laurence Rideau and
               Pierre{-}Yves Strub},
  title     = {Formal proofs of transcendence for e and pi as an application of multivariate
               and symmetric polynomials},
  booktitle = {{CPP}},
  pages     = {76--87},
  publisher = {{ACM}},
  year      = {2016}
}
@inproceedings{DBLP:conf/icalp/BartheGGHS16,
  author    = {Gilles Barthe and
               Marco Gaboardi and
               Benjamin Gr{\'{e}}goire and
               Justin Hsu and
               Pierre{-}Yves Strub},
  title     = {A Program Logic for Union Bounds},
  booktitle = {{ICALP}},
  series    = {LIPIcs},
  volume    = {55},
  pages     = {107:1--107:15},
  publisher = {Schloss Dagstuhl - Leibniz-Zentrum f{\"{u}}r Informatik},
  year      = {2016}
}
@inproceedings{DBLP:conf/lics/BartheGGHS16,
  author    = {Gilles Barthe and
               Marco Gaboardi and
               Benjamin Gr{\'{e}}goire and
               Justin Hsu and
               Pierre{-}Yves Strub},
  title     = {Proving Differential Privacy via Probabilistic Couplings},
  booktitle = {{LICS}},
  pages     = {749--758},
  publisher = {{ACM}},
  year      = {2016}
}
@inproceedings{DBLP:conf/popl/SwamyHKRDFBFSKZ16,
  author    = {Nikhil Swamy and
               Catalin Hritcu and
               Chantal Keller and
               Aseem Rastogi and
               Antoine Delignat{-}Lavaud and
               Simon Forest and
               Karthikeyan Bhargavan and
               C{\'{e}}dric Fournet and
               Pierre{-}Yves Strub and
               Markulf Kohlweiss and
               Jean Karim Zinzindohoue and
               Santiago Zanella B{\'{e}}guelin},
  title     = {Dependent types and multi-monadic effects in {F}},
  booktitle = {{POPL}},
  pages     = {256--270},
  publisher = {{ACM}},
  year      = {2016}
}
@inproceedings{DBLP:conf/wine/BartheGAHRS16,
  author    = {Gilles Barthe and
               Marco Gaboardi and
               Emilio Jes{\'{u}}s Gallego Arias and
               Justin Hsu and
               Aaron Roth and
               Pierre{-}Yves Strub},
  title     = {Computer-Aided Verification for Mechanism Design},
  booktitle = {{WINE}},
  series    = {Lecture Notes in Computer Science},
  volume    = {10123},
  pages     = {279--293},
  publisher = {Springer},
  year      = {2016}
}
@article{DBLP:journals/corr/BartheGGHS16,
  author    = {Gilles Barthe and
               Marco Gaboardi and
               Benjamin Gr{\'{e}}goire and
               Justin Hsu and
               Pierre{-}Yves Strub},
  title     = {Proving Differential Privacy via Probabilistic Couplings},
  journal   = {CoRR},
  volume    = {abs/1601.05047},
  year      = {2016}
}
@article{DBLP:journals/corr/BartheGGHS16a,
  author    = {Gilles Barthe and
               Marco Gaboardi and
               Benjamin Gr{\'{e}}goire and
               Justin Hsu and
               Pierre{-}Yves Strub},
  title     = {A program logic for union bounds},
  journal   = {CoRR},
  volume    = {abs/1602.05681},
  year      = {2016}
}
@article{DBLP:journals/corr/BartheFGAGHS16,
  author    = {Gilles Barthe and
               Gian Pietro Farina and
               Marco Gaboardi and
               Emilio Jes{\'{u}}s Gallego Arias and
               Andy Gordon and
               Justin Hsu and
               Pierre{-}Yves Strub},
  title     = {Differentially Private Bayesian Programming},
  journal   = {CoRR},
  volume    = {abs/1605.00283},
  year      = {2016}
}
@article{DBLP:journals/corr/BartheGGHS16b,
  author    = {Gilles Barthe and
               Marco Gaboardi and
               Benjamin Gr{\'{e}}goire and
               Justin Hsu and
               Pierre{-}Yves Strub},
  title     = {Advanced Probabilistic Couplings for Differential Privacy},
  journal   = {CoRR},
  volume    = {abs/1606.07143},
  year      = {2016}
}
@article{DBLP:journals/corr/BartheGHS16,
  author    = {Gilles Barthe and
               Benjamin Gr{\'{e}}goire and
               Justin Hsu and
               Pierre{-}Yves Strub},
  title     = {Coupling proofs are probabilistic product programs},
  journal   = {CoRR},
  volume    = {abs/1607.03455},
  year      = {2016}
}
@article{DBLP:journals/iacr/BartheDFGSS16,
  author    = {Gilles Barthe and
               Fran{\c{c}}ois Dupressoir and
               Sebastian Faust and
               Benjamin Gr{\'{e}}goire and
               Fran{\c{c}}ois{-}Xavier Standaert and
               Pierre{-}Yves Strub},
  title     = {Parallel Implementations of Masking Schemes and the Bounded Moment
               Leakage Model},
  journal   = {{IACR} Cryptol. ePrint Arch.},
  pages     = {912},
  year      = {2016}
}
@inproceedings{DBLP:conf/eurocrypt/BartheBDFGS15,
  author    = {Gilles Barthe and
               Sonia Bela{\"{\i}}d and
               Fran{\c{c}}ois Dupressoir and
               Pierre{-}Alain Fouque and
               Benjamin Gr{\'{e}}goire and
               Pierre{-}Yves Strub},
  title     = {Verified Proofs of Higher-Order Masking},
  booktitle = {{EUROCRYPT} {(1)}},
  series    = {Lecture Notes in Computer Science},
  volume    = {9056},
  pages     = {457--485},
  publisher = {Springer},
  year      = {2015}
}
@inproceedings{DBLP:conf/lpar/BartheEGHSS15,
  author    = {Gilles Barthe and
               Thomas Espitau and
               Benjamin Gr{\'{e}}goire and
               Justin Hsu and
               L{\'{e}}o Stefanesco and
               Pierre{-}Yves Strub},
  title     = {Relational Reasoning via Probabilistic Coupling},
  booktitle = {{LPAR}},
  series    = {Lecture Notes in Computer Science},
  volume    = {9450},
  pages     = {387--401},
  publisher = {Springer},
  year      = {2015}
}
@inproceedings{DBLP:conf/popl/BartheGAHRS15,
  author    = {Gilles Barthe and
               Marco Gaboardi and
               Emilio Jes{\'{u}}s Gallego Arias and
               Justin Hsu and
               Aaron Roth and
               Pierre{-}Yves Strub},
  title     = {Higher-Order Approximate Relational Refinement Types for Mechanism
               Design and Differential Privacy},
  booktitle = {{POPL}},
  pages     = {55--68},
  publisher = {{ACM}},
  year      = {2015}
}
@inproceedings{DBLP:conf/sp/BeurdoucheBDFKP15,
  author    = {Benjamin Beurdouche and
               Karthikeyan Bhargavan and
               Antoine Delignat{-}Lavaud and
               C{\'{e}}dric Fournet and
               Markulf Kohlweiss and
               Alfredo Pironti and
               Pierre{-}Yves Strub and
               Jean Karim Zinzindohoue},
  title     = {A Messy State of the Union: Taming the Composite State Machines of
               {TLS}},
  booktitle = {{IEEE} Symposium on Security and Privacy},
  pages     = {535--552},
  publisher = {{IEEE} Computer Society},
  year      = {2015}
}
@article{DBLP:journals/corr/BartheGAHRS15,
  author    = {Gilles Barthe and
               Marco Gaboardi and
               Emilio Jes{\'{u}}s Gallego Arias and
               Justin Hsu and
               Aaron Roth and
               Pierre{-}Yves Strub},
  title     = {Computer-aided verification in mechanism design},
  journal   = {CoRR},
  volume    = {abs/1502.04052},
  year      = {2015}
}
@article{DBLP:journals/corr/BartheEGHSS15,
  author    = {Gilles Barthe and
               Thomas Espitau and
               Benjamin Gr{\'{e}}goire and
               Justin Hsu and
               L{\'{e}}o Stefanesco and
               Pierre{-}Yves Strub},
  title     = {Relational reasoning via probabilistic coupling},
  journal   = {CoRR},
  volume    = {abs/1509.03476},
  year      = {2015}
}
@article{DBLP:journals/corr/BernardBRS15,
  author    = {Sophie Bernard and
               Yves Bertot and
               Laurence Rideau and
               Pierre{-}Yves Strub},
  title     = {Formal Proofs of Transcendence for e and {\textdollar}{\(\pi\)}{\textdollar}
               as an Application of Multivariate and Symmetric Polynomials},
  journal   = {CoRR},
  volume    = {abs/1512.02791},
  year      = {2015}
}
@article{DBLP:journals/iacr/BartheBDFGS15,
  author    = {Gilles Barthe and
               Sonia Bela{\"{\i}}d and
               Fran{\c{c}}ois Dupressoir and
               Pierre{-}Alain Fouque and
               Benjamin Gr{\'{e}}goire and
               Pierre{-}Yves Strub},
  title     = {Verified Proofs of Higher-Order Masking},
  journal   = {{IACR} Cryptol. ePrint Arch.},
  pages     = {60},
  year      = {2015}
}
@inproceedings{DBLP:conf/crypto/BhargavanFKPSB14,
  author    = {Karthikeyan Bhargavan and
               C{\'{e}}dric Fournet and
               Markulf Kohlweiss and
               Alfredo Pironti and
               Pierre{-}Yves Strub and
               Santiago Zanella B{\'{e}}guelin},
  title     = {Proving the {TLS} Handshake Secure (As It Is)},
  booktitle = {{CRYPTO} {(2)}},
  series    = {Lecture Notes in Computer Science},
  volume    = {8617},
  pages     = {235--255},
  publisher = {Springer},
  year      = {2014}
}
@inproceedings{DBLP:conf/csfw/AkinyeleBGSS14,
  author    = {Joseph A. Akinyele and
               Gilles Barthe and
               Benjamin Gr{\'{e}}goire and
               Benedikt Schmidt and
               Pierre{-}Yves Strub},
  title     = {Certified Synthesis of Efficient Batch Verifiers},
  booktitle = {{CSF}},
  pages     = {153--165},
  publisher = {{IEEE} Computer Society},
  year      = {2014}
}
@inproceedings{DBLP:conf/csfw/BartheGAHKS14,
  author    = {Gilles Barthe and
               Marco Gaboardi and
               Emilio Jes{\'{u}}s Gallego Arias and
               Justin Hsu and
               C{\'{e}}sar Kunz and
               Pierre{-}Yves Strub},
  title     = {Proving Differential Privacy in Hoare Logic},
  booktitle = {{CSF}},
  pages     = {411--424},
  publisher = {{IEEE} Computer Society},
  year      = {2014}
}
@inproceedings{DBLP:conf/itp/BartziaS14,
  author    = {Evmorfia{-}Iro Bartzia and
               Pierre{-}Yves Strub},
  title     = {A Formal Library for Elliptic Curves in the Coq Proof Assistant},
  booktitle = {{ITP}},
  series    = {Lecture Notes in Computer Science},
  volume    = {8558},
  pages     = {77--92},
  publisher = {Springer},
  year      = {2014}
}
@inproceedings{DBLP:conf/popl/BartheFGSSB14,
  author    = {Gilles Barthe and
               C{\'{e}}dric Fournet and
               Benjamin Gr{\'{e}}goire and
               Pierre{-}Yves Strub and
               Nikhil Swamy and
               Santiago Zanella B{\'{e}}guelin},
  title     = {Probabilistic relational verification for cryptographic implementations},
  booktitle = {{POPL}},
  pages     = {193--206},
  publisher = {{ACM}},
  year      = {2014}
}
@inproceedings{DBLP:conf/popl/SwamyFRBCSB14,
  author    = {Nikhil Swamy and
               C{\'{e}}dric Fournet and
               Aseem Rastogi and
               Karthikeyan Bhargavan and
               Juan Chen and
               Pierre{-}Yves Strub and
               Gavin M. Bierman},
  title     = {Gradual typing embedded securely in JavaScript},
  booktitle = {{POPL}},
  pages     = {425--438},
  publisher = {{ACM}},
  year      = {2014}
}
@inproceedings{DBLP:conf/sp/BhargavanDFPS14,
  author    = {Karthikeyan Bhargavan and
               Antoine Delignat{-}Lavaud and
               C{\'{e}}dric Fournet and
               Alfredo Pironti and
               Pierre{-}Yves Strub},
  title     = {Triple Handshakes and Cookie Cutters: Breaking and Fixing Authentication
               over {TLS}},
  booktitle = {{IEEE} Symposium on Security and Privacy},
  pages     = {98--113},
  publisher = {{IEEE} Computer Society},
  year      = {2014}
}
@article{DBLP:journals/corr/BartheGAHKS14,
  author    = {Gilles Barthe and
               Marco Gaboardi and
               Emilio Jes{\'{u}}s Gallego Arias and
               Justin Hsu and
               C{\'{e}}sar Kunz and
               Pierre{-}Yves Strub},
  title     = {Proving differential privacy in Hoare logic},
  journal   = {CoRR},
  volume    = {abs/1407.2988},
  year      = {2014}
}
@article{DBLP:journals/corr/BartheGAHRS14,
  author    = {Gilles Barthe and
               Marco Gaboardi and
               Emilio Jes{\'{u}}s Gallego Arias and
               Justin Hsu and
               Aaron Roth and
               Pierre{-}Yves Strub},
  title     = {Higher-Order Approximate Relational Refinement Types for Mechanism
               Design and Differential Privacy},
  journal   = {CoRR},
  volume    = {abs/1407.6845},
  year      = {2014}
}
@article{DBLP:journals/iacr/BhargavanFKPSB14,
  author    = {Karthikeyan Bhargavan and
               C{\'{e}}dric Fournet and
               Markulf Kohlweiss and
               Alfredo Pironti and
               Pierre{-}Yves Strub and
               Santiago Zanella B{\'{e}}guelin},
  title     = {Proving the {TLS} Handshake Secure (as it is)},
  journal   = {{IACR} Cryptol. ePrint Arch.},
  pages     = {182},
  year      = {2014}
}
@article{DBLP:journals/iacr/AlmeidaBBDDGS14,
  author    = {Jos{\'{e}} Bacelar Almeida and
               Manuel Barbosa and
               Gilles Barthe and
               Guillaume Davy and
               Fran{\c{c}}ois Dupressoir and
               Benjamin Gr{\'{e}}goire and
               Pierre{-}Yves Strub},
  title     = {Verified Implementations for Secure and Verifiable Computation},
  journal   = {{IACR} Cryptol. ePrint Arch.},
  pages     = {456},
  year      = {2014}
}
@article{DBLP:journals/jfp/SwamyCFSBY13,
  author    = {Nikhil Swamy and
               Juan Chen and
               C{\'{e}}dric Fournet and
               Pierre{-}Yves Strub and
               Karthikeyan Bhargavan and
               Jean Yang},
  title     = {Secure distributed programming with value-dependent types},
  journal   = {J. Funct. Program.},
  volume    = {23},
  number    = {4},
  pages     = {402--451},
  year      = {2013}
}
@inproceedings{DBLP:conf/fosad/BartheDGKSS13,
  author    = {Gilles Barthe and
               Fran{\c{c}}ois Dupressoir and
               Benjamin Gr{\'{e}}goire and
               C{\'{e}}sar Kunz and
               Benedikt Schmidt and
               Pierre{-}Yves Strub},
  title     = {EasyCrypt: {A} Tutorial},
  booktitle = {{FOSAD}},
  series    = {Lecture Notes in Computer Science},
  volume    = {8604},
  pages     = {146--166},
  publisher = {Springer},
  year      = {2013}
}
@inproceedings{DBLP:conf/popl/FournetSCDSL13,
  author    = {C{\'{e}}dric Fournet and
               Nikhil Swamy and
               Juan Chen and
               Pierre{-}{\'{E}}variste Dagand and
               Pierre{-}Yves Strub and
               Benjamin Livshits},
  title     = {Fully abstract compilation to JavaScript},
  booktitle = {{POPL}},
  pages     = {371--384},
  publisher = {{ACM}},
  year      = {2013}
}
@inproceedings{DBLP:conf/sp/BhargavanFKPS13,
  author    = {Karthikeyan Bhargavan and
               C{\'{e}}dric Fournet and
               Markulf Kohlweiss and
               Alfredo Pironti and
               Pierre{-}Yves Strub},
  title     = {Implementing {TLS} with Verified Cryptographic Security},
  booktitle = {{IEEE} Symposium on Security and Privacy},
  pages     = {445--459},
  publisher = {{IEEE} Computer Society},
  year      = {2013}
}
@inproceedings{DBLP:conf/popl/StrubSFC12,
  author    = {Pierre{-}Yves Strub and
               Nikhil Swamy and
               C{\'{e}}dric Fournet and
               Juan Chen},
  title     = {Self-certification: bootstrapping certified typecheckers in F* with
               Coq},
  booktitle = {{POPL}},
  pages     = {571--584},
  publisher = {{ACM}},
  year      = {2012}
}
@inproceedings{DBLP:conf/ccs/FournetKS11,
  author    = {C{\'{e}}dric Fournet and
               Markulf Kohlweiss and
               Pierre{-}Yves Strub},
  title     = {Modular code-based cryptographic verification},
  booktitle = {{CCS}},
  pages     = {341--350},
  publisher = {{ACM}},
  year      = {2011}
}
@inproceedings{DBLP:conf/icfp/SwamyCFSBY11,
  author    = {Nikhil Swamy and
               Juan Chen and
               C{\'{e}}dric Fournet and
               Pierre{-}Yves Strub and
               Karthikeyan Bhargavan and
               Jean Yang},
  title     = {Secure distributed programming with value-dependent types},
  booktitle = {{ICFP}},
  pages     = {266--278},
  publisher = {{ACM}},
  year      = {2011}
}
@inproceedings{DBLP:conf/lics/BarrasJSW11,
  author    = {Bruno Barras and
               Jean{-}Pierre Jouannaud and
               Pierre{-}Yves Strub and
               Qian Wang},
  title     = {CoQMTU: {A} Higher-Order Type Theory with a Predicative Hierarchy
               of Universes Parametrized by a Decidable First-Order Theory},
  booktitle = {{LICS}},
  pages     = {143--151},
  publisher = {{IEEE} Computer Society},
  year      = {2011}
}
@inproceedings{DBLP:conf/csl/Strub10,
  author    = {Pierre{-}Yves Strub},
  title     = {Coq Modulo Theory},
  booktitle = {{CSL}},
  series    = {Lecture Notes in Computer Science},
  volume    = {6247},
  pages     = {529--543},
  publisher = {Springer},
  year      = {2010}
}
@phdthesis{DBLP:phd/hal/Strub08,
  author    = {Pierre{-}Yves Strub},
  title     = {Type Theory and Decision Procedures. (Th{\'{e}}orie des Types
               et Proc{\'{e}}dures de D{\'{e}}cision)},
  school    = {{\'{E}}cole Polytechnique, Palaiseau, France},
  year      = {2008}
}
@inproceedings{DBLP:conf/ifipTCS/BlanquiJS08,
  author    = {Fr{\'{e}}d{\'{e}}ric Blanqui and
               Jean{-}Pierre Jouannaud and
               Pierre{-}Yves Strub},
  title     = {From Formal Proofs to Mathematical Proofs: {A} Safe, Incremental Way
               for Building in First-order Decision Procedures},
  booktitle = {{IFIP} {TCS}},
  series    = {{IFIP}},
  volume    = {273},
  pages     = {349--365},
  publisher = {Springer},
  year      = {2008}
}
@article{DBLP:journals/corr/abs-0804-3762,
  author    = {Fr{\'{e}}d{\'{e}}ric Blanqui and
               Jean{-}Pierre Jouannaud and
               Pierre{-}Yves Strub},
  title     = {From formal proofs to mathematical proofs: a safe, incremental way
               for building in first-order decision procedures},
  journal   = {CoRR},
  volume    = {abs/0804.3762},
  year      = {2008}
}
@inproceedings{DBLP:conf/csl/BlanquiJS07,
  author    = {Fr{\'{e}}d{\'{e}}ric Blanqui and
               Jean{-}Pierre Jouannaud and
               Pierre{-}Yves Strub},
  title     = {Building Decision Procedures in the Calculus of Inductive Constructions},
  booktitle = {{CSL}},
  series    = {Lecture Notes in Computer Science},
  volume    = {4646},
  pages     = {328--342},
  publisher = {Springer},
  year      = {2007}
}
@article{DBLP:journals/corr/abs-0707-1266,
  author    = {Fr{\'{e}}d{\'{e}}ric Blanqui and
               Jean{-}Pierre Jouannaud and
               Pierre{-}Yves Strub},
  title     = {Building Decision Procedures in the Calculus of Inductive Constructions},
  journal   = {CoRR},
  volume    = {abs/0707.1266},
  year      = {2007}
}
@inproceedings{DBLP:conf/icip/GeraudSD01,
  author    = {Thierry G{\'{e}}raud and
               Pierre{-}Yves Strub and
               J{\'{e}}r{\^{o}}me Darbon},
  title     = {Color image segmentation based on automatic morphological clustering},
  booktitle = {{ICIP} {(3)}},
  pages     = {70--73},
  publisher = {{IEEE}},
  year      = {2001}
}
a service of  Schloss Dagstuhl - Leibniz Center for Informatics