var bibbase_data = {"data":"\"Loading..\"\n\n
\n\n \n\n \n\n \n \n\n \n\n \n \n\n \n\n \n
\n generated by\n \n \"bibbase.org\"\n\n \n
\n \n\n
\n\n \n\n\n
\n\n Excellent! Next you can\n create a new website with this list, or\n embed it in an existing web page by copying & pasting\n any of the following snippets.\n\n
\n JavaScript\n (easiest)\n
\n \n <script src=\"https://bibbase.org/show?bib=http%3A%2F%2Fwww.strub.nu%2Fbiblio%2Fstrub.bib&jsonp=1&nocache=1&jsonp=1\"></script>\n \n
\n\n PHP\n
\n \n <?php\n $contents = file_get_contents(\"https://bibbase.org/show?bib=http%3A%2F%2Fwww.strub.nu%2Fbiblio%2Fstrub.bib&jsonp=1&nocache=1\");\n print_r($contents);\n ?>\n \n
\n\n iFrame\n (not recommended)\n
\n \n <iframe src=\"https://bibbase.org/show?bib=http%3A%2F%2Fwww.strub.nu%2Fbiblio%2Fstrub.bib&jsonp=1&nocache=1\"></iframe>\n \n
\n\n

\n For more details see the documention.\n

\n
\n
\n\n
\n\n This is a preview! To use this list on your own web site\n or create a new web site from it,\n create a free account. The file will be added\n and you will be able to edit it in the File Manager.\n We will show you instructions once you've created your account.\n
\n\n
\n\n

To the site owner:

\n\n

Action required! Mendeley is changing its\n API. In order to keep using Mendeley with BibBase past April\n 14th, you need to:\n

    \n
  1. renew the authorization for BibBase on Mendeley, and
  2. \n
  3. update the BibBase URL\n in your page the same way you did when you initially set up\n this page.\n
  4. \n
\n

\n\n

\n \n \n Fix it now\n

\n
\n\n
\n\n\n
\n \n \n
\n
\n  \n 2022\n \n \n (2)\n \n \n
\n
\n \n \n
\n \n\n \n \n \n \n \n \n A drag-and-drop proof tactic.\n \n \n \n \n\n\n \n Donato, P.; Strub, P.; and Werner, B.\n\n\n \n\n\n\n In Popescu, A.; and Zdancewic, S., editor(s), CPP '22: 11th ACM SIGPLAN International Conference on Certified Programs and Proofs, Philadelphia, PA, USA, January 17 - 18, 2022, pages 197–209, 2022. ACM\n \n\n\n\n
\n\n\n\n \n \n \"APaper\n  \n \n\n \n \n doi\n  \n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n  \n \n 3 downloads\n \n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{DBLP:conf/cpp/DonatoSW22,\n  author = {Pablo Donato and Pierre{-}Yves Strub and\nBenjamin Werner},\n  bibsource = {dblp computer science bibliography, https://dblp.org},\n  biburl = {https://dblp.org/rec/conf/cpp/DonatoSW22.bib},\n  booktitle = {{CPP} '22: 11th {ACM} {SIGPLAN} International\nConference on Certified Programs and Proofs,\nPhiladelphia, PA, USA, January 17 - 18, 2022},\n  doi = {10.1145/3497775.3503692},\n  editor = {Andrei Popescu and Steve Zdancewic},\n  isbn = {978-1-4503-9182-5},\n  pages = {197--209},\n  publisher = {{ACM}},\n  timestamp = {Mon, 17 Jan 2022 09:44:17 +0100},\n  title = {A drag-and-drop proof tactic},\n  url = {https://doi.org/10.1145/3497775.3503692},\n  year = {2022}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Formal Verification of Saber's Public-Key Encryption Scheme in EasyCrypt.\n \n \n \n \n\n\n \n Hülsing, A.; Meijers, M.; and Strub, P.\n\n\n \n\n\n\n In Dodis, Y.; and Shrimpton, T., editor(s), Advances in Cryptology - CRYPTO 2022 - 42nd Annual International Cryptology Conference, CRYPTO 2022, Santa Barbara, CA, USA, August 15-18, 2022, Proceedings, Part I, volume 13507, of Lecture Notes in Computer Science, pages 622–653, 2022. Springer\n \n\n\n\n
\n\n\n\n \n \n \"FormalPaper\n  \n \n\n \n \n doi\n  \n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{DBLP:conf/crypto/HulsingMS22,\n  author = {Andreas H{\\"{u}}lsing and Matthias Meijers and\nPierre{-}Yves Strub},\n  bibsource = {dblp computer science bibliography, https://dblp.org},\n  biburl = {https://dblp.org/rec/conf/crypto/HulsingMS22.bib},\n  booktitle = {Advances in Cryptology - {CRYPTO} 2022 - 42nd Annual\nInternational Cryptology Conference, {CRYPTO} 2022,\nSanta Barbara, CA, USA, August 15-18, 2022,\nProceedings, Part {I}},\n  doi = {10.1007/978-3-031-15802-5\\_22},\n  editor = {Yevgeniy Dodis and Thomas Shrimpton},\n  isbn = {978-3-031-15801-8},\n  pages = {622--653},\n  publisher = {Springer},\n  series = {Lecture Notes in Computer Science},\n  timestamp = {Sun, 13 Nov 2022 00:00:00 +0100},\n  title = {Formal Verification of Saber's Public-Key Encryption\nScheme in EasyCrypt},\n  url = {https://doi.org/10.1007/978-3-031-15802-5\\_22},\n  volume = {13507},\n  year = {2022}\n}\n\n
\n
\n\n\n\n
\n\n\n\n\n\n
\n
\n\n
\n
\n  \n 2021\n \n \n (3)\n \n \n
\n
\n \n \n
\n \n\n \n \n \n \n \n \n EasyPQC: Verifying Post-Quantum Cryptography.\n \n \n \n \n\n\n \n Barbosa, M.; Barthe, G.; Fan, X.; Grégoire, B.; Hung, S.; Katz, J.; Strub, P.; Wu, X.; and Zhou, L.\n\n\n \n\n\n\n In Kim, Y.; Kim, J.; Vigna, G.; and Shi, E., editor(s), CCS '21: 2021 ACM SIGSAC Conference on Computer and Communications Security, Virtual Event, Republic of Korea, November 15 - 19, 2021, pages 2564–2586, 2021. ACM\n \n\n\n\n
\n\n\n\n \n \n \"EasyPQC:Paper\n  \n \n\n \n \n doi\n  \n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n  \n \n 1 download\n \n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{DBLP:conf/ccs/BarbosaBFGHKSWZ21,\n  author = {Manuel Barbosa and Gilles Barthe and Xiong Fan and\nBenjamin Gr{\\'{e}}goire and Shih{-}Han Hung and\nJonathan Katz and Pierre{-}Yves Strub and Xiaodi Wu and\nLi Zhou},\n  bibsource = {dblp computer science bibliography, https://dblp.org},\n  biburl = {https://dblp.org/rec/conf/ccs/BarbosaBFGHKSWZ21.bib},\n  booktitle = {{CCS} '21: 2021 {ACM} {SIGSAC} Conference on Computer\nand Communications Security, Virtual Event, Republic\nof Korea, November 15 - 19, 2021},\n  doi = {10.1145/3460120.3484567},\n  editor = {Yongdae Kim and Jong Kim and Giovanni Vigna and\nElaine Shi},\n  isbn = {978-1-4503-8454-4},\n  pages = {2564--2586},\n  publisher = {{ACM}},\n  timestamp = {Mon, 03 Jan 2022 00:00:00 +0100},\n  title = {EasyPQC: Verifying Post-Quantum Cryptography},\n  url = {https://doi.org/10.1145/3460120.3484567},\n  year = {2021}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Mechanized Proofs of Adversarial Complexity and Application to Universal Composability.\n \n \n \n \n\n\n \n Barbosa, M.; Barthe, G.; Grégoire, B.; Koutsos, A.; and Strub, P.\n\n\n \n\n\n\n In Kim, Y.; Kim, J.; Vigna, G.; and Shi, E., editor(s), CCS '21: 2021 ACM SIGSAC Conference on Computer and Communications Security, Virtual Event, Republic of Korea, November 15 - 19, 2021, pages 2541–2563, 2021. ACM\n \n\n\n\n
\n\n\n\n \n \n \"MechanizedPaper\n  \n \n\n \n \n doi\n  \n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n  \n \n 1 download\n \n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{DBLP:conf/ccs/BarbosaBGKS21,\n  author = {Manuel Barbosa and Gilles Barthe and\nBenjamin Gr{\\'{e}}goire and Adrien Koutsos and\nPierre{-}Yves Strub},\n  bibsource = {dblp computer science bibliography, https://dblp.org},\n  biburl = {https://dblp.org/rec/conf/ccs/BarbosaBGKS21.bib},\n  booktitle = {{CCS} '21: 2021 {ACM} {SIGSAC} Conference on Computer\nand Communications Security, Virtual Event, Republic\nof Korea, November 15 - 19, 2021},\n  doi = {10.1145/3460120.3484548},\n  editor = {Yongdae Kim and Jong Kim and Giovanni Vigna and\nElaine Shi},\n  isbn = {978-1-4503-8454-4},\n  pages = {2541--2563},\n  publisher = {{ACM}},\n  timestamp = {Thu, 23 Jun 2022 01:00:00 +0200},\n  title = {Mechanized Proofs of Adversarial Complexity and\nApplication to Universal Composability},\n  url = {https://doi.org/10.1145/3460120.3484548},\n  year = {2021}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Unsolvability of the Quintic Formalized in Dependent Type Theory.\n \n \n \n \n\n\n \n Bernard, S.; Cohen, C.; Mahboubi, A.; and Strub, P.\n\n\n \n\n\n\n In Cohen, L.; and Kaliszyk, C., editor(s), 12th International Conference on Interactive Theorem Proving, ITP 2021, June 29 to July 1, 2021, Rome, Italy (Virtual Conference), volume 193, of LIPIcs, pages 8:1–8:18, 2021. Schloss Dagstuhl - Leibniz-Zentrum für Informatik\n \n\n\n\n
\n\n\n\n \n \n \"UnsolvabilityPaper\n  \n \n\n \n \n doi\n  \n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{DBLP:conf/itp/BernardCMS21,\n  author = {Sophie Bernard and Cyril Cohen and Assia Mahboubi and\nPierre{-}Yves Strub},\n  bibsource = {dblp computer science bibliography, https://dblp.org},\n  biburl = {https://dblp.org/rec/conf/itp/BernardCMS21.bib},\n  booktitle = {12th International Conference on Interactive Theorem\nProving, {ITP} 2021, June 29 to July 1, 2021, Rome,\nItaly (Virtual Conference)},\n  doi = {10.4230/LIPIcs.ITP.2021.8},\n  editor = {Liron Cohen and Cezary Kaliszyk},\n  isbn = {978-3-95977-188-7},\n  pages = {8:1--8:18},\n  publisher = {Schloss Dagstuhl - Leibniz-Zentrum f{\\"{u}}r\nInformatik},\n  series = {LIPIcs},\n  timestamp = {Mon, 21 Jun 2021 14:45:49 +0200},\n  title = {Unsolvability of the Quintic Formalized in Dependent\nType Theory},\n  url = {https://doi.org/10.4230/LIPIcs.ITP.2021.8},\n  volume = {193},\n  year = {2021}\n}\n\n
\n
\n\n\n\n
\n\n\n\n\n\n
\n
\n\n
\n
\n  \n 2020\n \n \n (3)\n \n \n
\n
\n \n \n
\n \n\n \n \n \n \n \n \n Formalizing the Face Lattice of Polyhedra.\n \n \n \n \n\n\n \n Allamigeon, X.; Katz, R. D.; and Strub, P.\n\n\n \n\n\n\n In Peltier, N.; and Sofronie-Stokkermans, V., editor(s), Automated Reasoning - 10th International Joint Conference, IJCAR 2020, Paris, France, July 1-4, 2020, Proceedings, Part II, volume 12167, of Lecture Notes in Computer Science, pages 185–203, 2020. Springer\n \n\n\n\n
\n\n\n\n \n \n \"FormalizingPaper\n  \n \n\n \n \n doi\n  \n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n  \n \n 10 downloads\n \n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{DBLP:conf/cade/AllamigeonKS20,\n  author = {Xavier Allamigeon and Ricardo D. Katz and\nPierre{-}Yves Strub},\n  bibsource = {dblp computer science bibliography, https://dblp.org},\n  biburl = {https://dblp.org/rec/conf/cade/AllamigeonKS20.bib},\n  booktitle = {Automated Reasoning - 10th International Joint\nConference, {IJCAR} 2020, Paris, France, July 1-4,\n2020, Proceedings, Part {II}},\n  doi = {10.1007/978-3-030-51054-1\\_11},\n  editor = {Nicolas Peltier and Viorica Sofronie{-}Stokkermans},\n  isbn = {978-3-030-51053-4},\n  pages = {185--203},\n  publisher = {Springer},\n  series = {Lecture Notes in Computer Science},\n  timestamp = {Fri, 03 Jul 2020 13:56:19 +0200},\n  title = {Formalizing the Face Lattice of Polyhedra},\n  url = {https://doi.org/10.1007/978-3-030-51054-1\\_11},\n  volume = {12167},\n  year = {2020}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n The Last Mile: High-Assurance and High-Speed Cryptographic Implementations.\n \n \n \n \n\n\n \n Almeida, J. B.; Barbosa, M.; Barthe, G.; Grégoire, B.; Koutsos, A.; Laporte, V.; Oliveira, T.; and Strub, P.\n\n\n \n\n\n\n In 2020 IEEE Symposium on Security and Privacy, SP 2020, San Francisco, CA, USA, May 18-21, 2020, pages 965–982, 2020. IEEE\n \n\n\n\n
\n\n\n\n \n \n \"ThePaper\n  \n \n\n \n \n doi\n  \n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n  \n \n 1 download\n \n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{DBLP:conf/sp/AlmeidaBBGKL0S20,\n  author = {Jos{\\'{e}} Bacelar Almeida and Manuel Barbosa and\nGilles Barthe and Benjamin Gr{\\'{e}}goire and\nAdrien Koutsos and Vincent Laporte and Tiago Oliveira and\nPierre{-}Yves Strub},\n  bibsource = {dblp computer science bibliography, https://dblp.org},\n  biburl = {https://dblp.org/rec/conf/sp/AlmeidaBBGKL0S20.bib},\n  booktitle = {2020 {IEEE} Symposium on Security and Privacy, {SP}\n2020, San Francisco, CA, USA, May 18-21, 2020},\n  doi = {10.1109/SP40000.2020.00028},\n  pages = {965--982},\n  publisher = {{IEEE}},\n  timestamp = {Tue, 29 Dec 2020 00:00:00 +0100},\n  title = {The Last Mile: High-Assurance and High-Speed\nCryptographic Implementations},\n  url = {https://doi.org/10.1109/SP40000.2020.00028},\n  year = {2020}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Improved parallel mask refreshing algorithms: generic solutions with parametrized non-interference and automated optimizations.\n \n \n \n \n\n\n \n Barthe, G.; Belaïd, S.; Dupressoir, F.; Fouque, P.; Grégoire, B.; Standaert, F.; and Strub, P.\n\n\n \n\n\n\n J. Cryptogr. Eng., 10(1): 17–26. 2020.\n \n\n\n\n
\n\n\n\n \n \n \"ImprovedPaper\n  \n \n\n \n \n doi\n  \n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n  \n \n 1 download\n \n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@article{DBLP:journals/jce/BartheBDFGSS20,\n  author = {Gilles Barthe and Sonia Bela{\\"{\\i}}d and\nFran{\\c{c}}ois Dupressoir and Pierre{-}Alain Fouque and\nBenjamin Gr{\\'{e}}goire and\nFran{\\c{c}}ois{-}Xavier Standaert and\nPierre{-}Yves Strub},\n  bibsource = {dblp computer science bibliography, https://dblp.org},\n  biburl = {https://dblp.org/rec/journals/jce/BartheBDFGSS20.bib},\n  doi = {10.1007/s13389-018-00202-2},\n  journal = {J. Cryptogr. Eng.},\n  number = {1},\n  pages = {17--26},\n  timestamp = {Thu, 14 Oct 2021 01:00:00 +0200},\n  title = {Improved parallel mask refreshing algorithms: generic\nsolutions with parametrized non-interference and\nautomated optimizations},\n  url = {https://doi.org/10.1007/s13389-018-00202-2},\n  volume = {10},\n  year = {2020}\n}\n\n
\n
\n\n\n\n
\n\n\n\n\n\n
\n
\n\n
\n
\n  \n 2019\n \n \n (4)\n \n \n
\n
\n \n \n
\n \n\n \n \n \n \n \n \n Machine-Checked Proofs for Cryptographic Standards: Indifferentiability of Sponge and Secure High-Assurance Implementations of SHA-3.\n \n \n \n \n\n\n \n Almeida, J. B.; Baritel-Ruet, C.; Barbosa, M.; Barthe, G.; Dupressoir, F.; Grégoire, B.; Laporte, V.; Oliveira, T.; Stoughton, A.; and Strub, P.\n\n\n \n\n\n\n In Cavallaro, L.; Kinder, J.; Wang, X.; and Katz, J., editor(s), Proceedings of the 2019 ACM SIGSAC Conference on Computer and Communications Security, CCS 2019, London, UK, November 11-15, 2019, pages 1607–1622, 2019. ACM\n \n\n\n\n
\n\n\n\n \n \n \"Machine-CheckedPaper\n  \n \n\n \n \n doi\n  \n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n  \n \n 2 downloads\n \n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{DBLP:conf/ccs/AlmeidaBBBDGL0S19,\n  author = {Jos{\\'{e}} Bacelar Almeida and\nC{\\'{e}}cile Baritel{-}Ruet and Manuel Barbosa and\nGilles Barthe and Fran{\\c{c}}ois Dupressoir and\nBenjamin Gr{\\'{e}}goire and Vincent Laporte and\nTiago Oliveira and Alley Stoughton and\nPierre{-}Yves Strub},\n  bibsource = {dblp computer science bibliography, https://dblp.org},\n  biburl = {https://dblp.org/rec/conf/ccs/AlmeidaBBBDGL0S19.bib},\n  booktitle = {Proceedings of the 2019 {ACM} {SIGSAC} Conference on\nComputer and Communications Security, {CCS} 2019,\nLondon, UK, November 11-15, 2019},\n  doi = {10.1145/3319535.3363211},\n  editor = {Lorenzo Cavallaro and Johannes Kinder and\nXiaoFeng Wang and Jonathan Katz},\n  isbn = {978-1-4503-6747-9},\n  pages = {1607--1622},\n  publisher = {{ACM}},\n  timestamp = {Mon, 29 Mar 2021 01:00:00 +0200},\n  title = {Machine-Checked Proofs for Cryptographic Standards:\nIndifferentiability of Sponge and Secure\nHigh-Assurance Implementations of {SHA-3}},\n  url = {https://doi.org/10.1145/3319535.3363211},\n  year = {2019}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n A Machine-Checked Proof of Security for AWS Key Management Service.\n \n \n \n \n\n\n \n Almeida, J. B.; Barbosa, M.; Barthe, G.; Campagna, M.; Cohen, E.; Grégoire, B.; Pereira, V.; Portela, B.; Strub, P.; and Tasiran, S.\n\n\n \n\n\n\n In Cavallaro, L.; Kinder, J.; Wang, X.; and Katz, J., editor(s), Proceedings of the 2019 ACM SIGSAC Conference on Computer and Communications Security, CCS 2019, London, UK, November 11-15, 2019, pages 63–78, 2019. ACM\n \n\n\n\n
\n\n\n\n \n \n \"APaper\n  \n \n\n \n \n doi\n  \n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n  \n \n 2 downloads\n \n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{DBLP:conf/ccs/AlmeidaBBCCGPPS19,\n  author = {Jos{\\'{e}} Bacelar Almeida and Manuel Barbosa and\nGilles Barthe and Matthew Campagna and Ernie Cohen and\nBenjamin Gr{\\'{e}}goire and Vitor Pereira and\nBernardo Portela and Pierre{-}Yves Strub and\nSerdar Tasiran},\n  bibsource = {dblp computer science bibliography, https://dblp.org},\n  biburl = {https://dblp.org/rec/conf/ccs/AlmeidaBBCCGPPS19.bib},\n  booktitle = {Proceedings of the 2019 {ACM} {SIGSAC} Conference on\nComputer and Communications Security, {CCS} 2019,\nLondon, UK, November 11-15, 2019},\n  doi = {10.1145/3319535.3354228},\n  editor = {Lorenzo Cavallaro and Johannes Kinder and\nXiaoFeng Wang and Jonathan Katz},\n  isbn = {978-1-4503-6747-9},\n  pages = {63--78},\n  publisher = {{ACM}},\n  timestamp = {Fri, 29 Apr 2022 01:00:00 +0200},\n  title = {A Machine-Checked Proof of Security for {AWS} Key\nManagement Service},\n  url = {https://doi.org/10.1145/3319535.3354228},\n  year = {2019}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Symbolic Methods in Computational Cryptography Proofs.\n \n \n \n \n\n\n \n Barthe, G.; Grégoire, B.; Jacomme, C.; Kremer, S.; and Strub, P.\n\n\n \n\n\n\n In 32nd IEEE Computer Security Foundations Symposium, CSF 2019, Hoboken, NJ, USA, June 25-28, 2019, pages 136–151, 2019. IEEE\n \n\n\n\n
\n\n\n\n \n \n \"SymbolicPaper\n  \n \n\n \n \n doi\n  \n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n  \n \n 3 downloads\n \n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{DBLP:conf/csfw/BartheGJKS19,\n  author = {Gilles Barthe and Benjamin Gr{\\'{e}}goire and\nCharlie Jacomme and Steve Kremer and\nPierre{-}Yves Strub},\n  bibsource = {dblp computer science bibliography, https://dblp.org},\n  biburl = {https://dblp.org/rec/conf/csfw/BartheGJKS19.bib},\n  booktitle = {32nd {IEEE} Computer Security Foundations Symposium,\n{CSF} 2019, Hoboken, NJ, USA, June 25-28, 2019},\n  doi = {10.1109/CSF.2019.00017},\n  isbn = {978-1-7281-1407-1},\n  pages = {136--151},\n  publisher = {{IEEE}},\n  timestamp = {Wed, 16 Oct 2019 14:14:49 +0200},\n  title = {Symbolic Methods in Computational Cryptography\nProofs},\n  url = {https://doi.org/10.1109/CSF.2019.00017},\n  year = {2019}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Relational \\(⋆\\)\\(⋆\\)\\star-Liftings for Differential Privacy.\n \n \n \n \n\n\n \n Barthe, G.; Espitau, T.; Hsu, J.; Sato, T.; and Strub, P.\n\n\n \n\n\n\n Log. Methods Comput. Sci., 15(4). 2019.\n \n\n\n\n
\n\n\n\n \n \n \"RelationalPaper\n  \n \n\n \n \n doi\n  \n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@article{DBLP:journals/lmcs/BartheEHSS19,\n  author = {Gilles Barthe and Thomas Espitau and Justin Hsu and\nTetsuya Sato and Pierre{-}Yves Strub},\n  bibsource = {dblp computer science bibliography, https://dblp.org},\n  biburl = {https://dblp.org/rec/journals/lmcs/BartheEHSS19.bib},\n  doi = {10.23638/LMCS-15(4:18)2019},\n  journal = {Log. Methods Comput. Sci.},\n  number = {4},\n  timestamp = {Thu, 14 Oct 2021 01:00:00 +0200},\n  title = {Relational\n{\\(\\star\\)}{\\(\\star\\)}{\\textbackslash}star-Liftings\nfor Differential Privacy},\n  url = {https://doi.org/10.23638/LMCS-15(4:18)2019},\n  volume = {15},\n  year = {2019}\n}\n\n
\n
\n\n\n\n
\n\n\n\n\n\n
\n
\n\n
\n
\n  \n 2018\n \n \n (4)\n \n \n
\n
\n \n \n
\n \n\n \n \n \n \n \n \n Computer-Aided Proofs for Multiparty Computation with Active Security.\n \n \n \n \n\n\n \n Haagh, H.; Karbyshev, A.; Oechsner, S.; Spitters, B.; and Strub, P.\n\n\n \n\n\n\n In 31st IEEE Computer Security Foundations Symposium, CSF 2018, Oxford, United Kingdom, July 9-12, 2018, pages 119–131, 2018. IEEE Computer Society\n \n\n\n\n
\n\n\n\n \n \n \"Computer-AidedPaper\n  \n \n\n \n \n doi\n  \n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n  \n \n 3 downloads\n \n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{DBLP:conf/csfw/HaaghKOSS18,\n  author = {Helene Haagh and Aleksandr Karbyshev and\nSabine Oechsner and Bas Spitters and\nPierre{-}Yves Strub},\n  bibsource = {dblp computer science bibliography, https://dblp.org},\n  biburl = {https://dblp.org/rec/conf/csfw/HaaghKOSS18.bib},\n  booktitle = {31st {IEEE} Computer Security Foundations Symposium,\n{CSF} 2018, Oxford, United Kingdom, July 9-12, 2018},\n  doi = {10.1109/CSF.2018.00016},\n  isbn = {978-1-5386-6680-7},\n  pages = {119--131},\n  publisher = {{IEEE} Computer Society},\n  timestamp = {Sun, 02 Oct 2022 01:00:00 +0200},\n  title = {Computer-Aided Proofs for Multiparty Computation with\nActive Security},\n  url = {https://doi.org/10.1109/CSF.2018.00016},\n  year = {2018}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n An Assertion-Based Program Logic for Probabilistic Programs.\n \n \n \n \n\n\n \n Barthe, G.; Espitau, T.; Gaboardi, M.; Grégoire, B.; Hsu, J.; and Strub, P.\n\n\n \n\n\n\n In Ahmed, A., editor(s), Programming Languages and Systems - 27th European Symposium on Programming, ESOP 2018, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2018, Thessaloniki, Greece, April 14-20, 2018, Proceedings, volume 10801, of Lecture Notes in Computer Science, pages 117–144, 2018. Springer\n \n\n\n\n
\n\n\n\n \n \n \"AnPaper\n  \n \n\n \n \n doi\n  \n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n  \n \n 1 download\n \n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{DBLP:conf/esop/BartheEGGHS18,\n  author = {Gilles Barthe and Thomas Espitau and Marco Gaboardi and\nBenjamin Gr{\\'{e}}goire and Justin Hsu and\nPierre{-}Yves Strub},\n  bibsource = {dblp computer science bibliography, https://dblp.org},\n  biburl = {https://dblp.org/rec/conf/esop/BartheEGGHS18.bib},\n  booktitle = {Programming Languages and Systems - 27th European\nSymposium on Programming, {ESOP} 2018, Held as Part\nof the European Joint Conferences on Theory and\nPractice of Software, {ETAPS} 2018, Thessaloniki,\nGreece, April 14-20, 2018, Proceedings},\n  doi = {10.1007/978-3-319-89884-1\\_5},\n  editor = {Amal Ahmed},\n  isbn = {978-3-319-89883-4},\n  pages = {117--144},\n  publisher = {Springer},\n  series = {Lecture Notes in Computer Science},\n  timestamp = {Tue, 05 Jul 2022 08:30:25 +0200},\n  title = {An Assertion-Based Program Logic for Probabilistic\nPrograms},\n  url = {https://doi.org/10.1007/978-3-319-89884-1\\_5},\n  volume = {10801},\n  year = {2018}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n hacspec: Towards Verifiable Crypto Standards.\n \n \n \n \n\n\n \n Bhargavan, K.; Kiefer, F.; and Strub, P.\n\n\n \n\n\n\n In Cremers, C.; and Lehmann, A., editor(s), Security Standardisation Research - 4th International Conference, SSR 2018, Darmstadt, Germany, November 26-27, 2018, Proceedings, volume 11322, of Lecture Notes in Computer Science, pages 1–20, 2018. Springer\n \n\n\n\n
\n\n\n\n \n \n \"hacspec:Paper\n  \n \n\n \n \n doi\n  \n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{DBLP:conf/secsr/BhargavanKS18,\n  author = {Karthikeyan Bhargavan and Franziskus Kiefer and\nPierre{-}Yves Strub},\n  bibsource = {dblp computer science bibliography, https://dblp.org},\n  biburl = {https://dblp.org/rec/conf/secsr/BhargavanKS18.bib},\n  booktitle = {Security Standardisation Research - 4th International\nConference, {SSR} 2018, Darmstadt, Germany, November\n26-27, 2018, Proceedings},\n  doi = {10.1007/978-3-030-04762-7\\_1},\n  editor = {Cas Cremers and Anja Lehmann},\n  isbn = {978-3-030-04761-0},\n  pages = {1--20},\n  publisher = {Springer},\n  series = {Lecture Notes in Computer Science},\n  timestamp = {Tue, 14 May 2019 10:00:40 +0200},\n  title = {hacspec: Towards Verifiable Crypto Standards},\n  url = {https://doi.org/10.1007/978-3-030-04762-7\\_1},\n  volume = {11322},\n  year = {2018}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Proving expected sensitivity of probabilistic programs.\n \n \n \n \n\n\n \n Barthe, G.; Espitau, T.; Grégoire, B.; Hsu, J.; and Strub, P.\n\n\n \n\n\n\n Proc. ACM Program. Lang., 2(POPL): 57:1–57:29. 2018.\n \n\n\n\n
\n\n\n\n \n \n \"ProvingPaper\n  \n \n\n \n \n doi\n  \n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@article{DBLP:journals/pacmpl/BartheEGHS18,\n  author = {Gilles Barthe and Thomas Espitau and\nBenjamin Gr{\\'{e}}goire and Justin Hsu and\nPierre{-}Yves Strub},\n  bibsource = {dblp computer science bibliography, https://dblp.org},\n  biburl = {https://dblp.org/rec/journals/pacmpl/BartheEGHS18.bib},\n  doi = {10.1145/3158145},\n  journal = {Proc. {ACM} Program. Lang.},\n  number = {{POPL}},\n  pages = {57:1--57:29},\n  timestamp = {Wed, 17 Feb 2021 00:00:00 +0100},\n  title = {Proving expected sensitivity of probabilistic\nprograms},\n  url = {https://doi.org/10.1145/3158145},\n  volume = {2},\n  year = {2018}\n}\n
\n
\n\n\n\n
\n\n\n\n\n\n
\n
\n\n
\n
\n  \n 2017\n \n \n (9)\n \n \n
\n
\n \n \n
\n \n\n \n \n \n \n \n \n Jasmin: High-Assurance and High-Speed Cryptography.\n \n \n \n \n\n\n \n Almeida, J. B.; Barbosa, M.; Barthe, G.; Blot, A.; Grégoire, B.; Laporte, V.; Oliveira, T.; Pacheco, H.; Schmidt, B.; and Strub, P.\n\n\n \n\n\n\n In Thuraisingham, B.; Evans, D.; Malkin, T.; and Xu, D., editor(s), Proceedings of the 2017 ACM SIGSAC Conference on Computer and Communications Security, CCS 2017, Dallas, TX, USA, October 30 - November 03, 2017, pages 1807–1823, 2017. ACM\n \n\n\n\n
\n\n\n\n \n \n \"Jasmin:Paper\n  \n \n\n \n \n doi\n  \n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n  \n \n 1 download\n \n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{DBLP:conf/ccs/AlmeidaBBBGLOPS17,\n  author = {Jos{\\'{e}} Bacelar Almeida and Manuel Barbosa and\nGilles Barthe and Arthur Blot and\nBenjamin Gr{\\'{e}}goire and Vincent Laporte and\nTiago Oliveira and Hugo Pacheco and Benedikt Schmidt and\nPierre{-}Yves Strub},\n  bibsource = {dblp computer science bibliography, https://dblp.org},\n  biburl = {https://dblp.org/rec/conf/ccs/AlmeidaBBBGLOPS17.bib},\n  booktitle = {Proceedings of the 2017 {ACM} {SIGSAC} Conference on\nComputer and Communications Security, {CCS} 2017,\nDallas, TX, USA, October 30 - November 03, 2017},\n  doi = {10.1145/3133956.3134078},\n  editor = {Bhavani Thuraisingham and David Evans and Tal Malkin and\nDongyan Xu},\n  isbn = {978-1-4503-4946-8},\n  pages = {1807--1823},\n  publisher = {{ACM}},\n  timestamp = {Wed, 29 Jun 2022 15:37:41 +0200},\n  title = {Jasmin: High-Assurance and High-Speed Cryptography},\n  url = {https://doi.org/10.1145/3133956.3134078},\n  year = {2017}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Parallel Implementations of Masking Schemes and the Bounded Moment Leakage Model.\n \n \n \n \n\n\n \n Barthe, G.; Dupressoir, F.; Faust, S.; Grégoire, B.; Standaert, F.; and Strub, P.\n\n\n \n\n\n\n In Coron, J.; and Nielsen, J. B., editor(s), Advances in Cryptology - EUROCRYPT 2017 - 36th Annual International Conference on the Theory and Applications of Cryptographic Techniques, Paris, France, April 30 - May 4, 2017, Proceedings, Part I, volume 10210, of Lecture Notes in Computer Science, pages 535–566, 2017. \n \n\n\n\n
\n\n\n\n \n \n \"ParallelPaper\n  \n \n\n \n \n doi\n  \n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{DBLP:conf/eurocrypt/BartheDFGSS17,\n  author = {Gilles Barthe and Fran{\\c{c}}ois Dupressoir and\nSebastian Faust and Benjamin Gr{\\'{e}}goire and\nFran{\\c{c}}ois{-}Xavier Standaert and\nPierre{-}Yves Strub},\n  bibsource = {dblp computer science bibliography, https://dblp.org},\n  biburl = {https://dblp.org/rec/conf/eurocrypt/BartheDFGSS17.bib},\n  booktitle = {Advances in Cryptology - {EUROCRYPT} 2017 - 36th\nAnnual International Conference on the Theory and\nApplications of Cryptographic Techniques, Paris,\nFrance, April 30 - May 4, 2017, Proceedings, Part\n{I}},\n  doi = {10.1007/978-3-319-56620-7\\_19},\n  editor = {Jean{-}S{\\'{e}}bastien Coron and Jesper Buus Nielsen},\n  isbn = {978-3-319-56619-1},\n  pages = {535--566},\n  series = {Lecture Notes in Computer Science},\n  timestamp = {Thu, 14 Oct 2021 01:00:00 +0200},\n  title = {Parallel Implementations of Masking Schemes and the\nBounded Moment Leakage Model},\n  url = {https://doi.org/10.1007/978-3-319-56620-7\\_19},\n  volume = {10210},\n  year = {2017}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n *-Liftings for Differential Privacy.\n \n \n \n \n\n\n \n Barthe, G.; Espitau, T.; Hsu, J.; Sato, T.; and Strub, P.\n\n\n \n\n\n\n In Chatzigiannakis, I.; Indyk, P.; Kuhn, F.; and Muscholl, A., editor(s), 44th International Colloquium on Automata, Languages, and Programming, ICALP 2017, July 10-14, 2017, Warsaw, Poland, volume 80, of LIPIcs, pages 102:1–102:12, 2017. Schloss Dagstuhl - Leibniz-Zentrum für Informatik\n \n\n\n\n
\n\n\n\n \n \n \"*-LiftingsPaper\n  \n \n\n \n \n doi\n  \n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{DBLP:conf/icalp/BartheEHSS17,\n  author = {Gilles Barthe and Thomas Espitau and Justin Hsu and\nTetsuya Sato and Pierre{-}Yves Strub},\n  bibsource = {dblp computer science bibliography, https://dblp.org},\n  biburl = {https://dblp.org/rec/conf/icalp/BartheEHSS17.bib},\n  booktitle = {44th International Colloquium on Automata, Languages,\nand Programming, {ICALP} 2017, July 10-14, 2017,\nWarsaw, Poland},\n  doi = {10.4230/LIPIcs.ICALP.2017.102},\n  editor = {Ioannis Chatzigiannakis and Piotr Indyk and\nFabian Kuhn and Anca Muscholl},\n  isbn = {978-3-95977-041-5},\n  pages = {102:1--102:12},\n  publisher = {Schloss Dagstuhl - Leibniz-Zentrum f{\\"{u}}r\nInformatik},\n  series = {LIPIcs},\n  timestamp = {Mon, 11 Oct 2021 01:00:00 +0200},\n  title = {*-Liftings for Differential Privacy},\n  url = {https://doi.org/10.4230/LIPIcs.ICALP.2017.102},\n  volume = {80},\n  year = {2017}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Proving uniformity and independence by self-composition and coupling.\n \n \n \n \n\n\n \n Barthe, G.; Espitau, T.; Grégoire, B.; Hsu, J.; and Strub, P.\n\n\n \n\n\n\n In Eiter, T.; and Sands, D., editor(s), LPAR-21, 21st International Conference on Logic for Programming, Artificial Intelligence and Reasoning, Maun, Botswana, May 7-12, 2017, volume 46, of EPiC Series in Computing, pages 385–403, 2017. EasyChair\n \n\n\n\n
\n\n\n\n \n \n \"ProvingPaper\n  \n \n\n \n \n doi\n  \n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{DBLP:conf/lpar/BartheEGHS17,\n  author = {Gilles Barthe and Thomas Espitau and\nBenjamin Gr{\\'{e}}goire and Justin Hsu and\nPierre{-}Yves Strub},\n  bibsource = {dblp computer science bibliography, https://dblp.org},\n  biburl = {https://dblp.org/rec/conf/lpar/BartheEGHS17.bib},\n  booktitle = {LPAR-21, 21st International Conference on Logic for\nProgramming, Artificial Intelligence and Reasoning,\nMaun, Botswana, May 7-12, 2017},\n  doi = {10.29007/vz48},\n  editor = {Thomas Eiter and David Sands},\n  pages = {385--403},\n  publisher = {EasyChair},\n  series = {EPiC Series in Computing},\n  timestamp = {Thu, 14 Oct 2021 01:00:00 +0200},\n  title = {Proving uniformity and independence by\nself-composition and coupling},\n  url = {https://doi.org/10.29007/vz48},\n  volume = {46},\n  year = {2017}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Coq without Type Casts: A Complete Proof of Coq Modulo Theory.\n \n \n \n \n\n\n \n Jouannaud, J.; and Strub, P.\n\n\n \n\n\n\n In Eiter, T.; and Sands, D., editor(s), LPAR-21, 21st International Conference on Logic for Programming, Artificial Intelligence and Reasoning, Maun, Botswana, May 7-12, 2017, volume 46, of EPiC Series in Computing, pages 474–489, 2017. EasyChair\n \n\n\n\n
\n\n\n\n \n \n \"CoqPaper\n  \n \n\n \n \n doi\n  \n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n  \n \n 2 downloads\n \n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{DBLP:conf/lpar/JouannaudS17,\n  author = {Jean{-}Pierre Jouannaud and Pierre{-}Yves Strub},\n  bibsource = {dblp computer science bibliography, https://dblp.org},\n  biburl = {https://dblp.org/rec/conf/lpar/JouannaudS17.bib},\n  booktitle = {LPAR-21, 21st International Conference on Logic for\nProgramming, Artificial Intelligence and Reasoning,\nMaun, Botswana, May 7-12, 2017},\n  doi = {10.29007/bjpg},\n  editor = {Thomas Eiter and David Sands},\n  pages = {474--489},\n  publisher = {EasyChair},\n  series = {EPiC Series in Computing},\n  timestamp = {Sun, 15 Aug 2021 01:00:00 +0200},\n  title = {Coq without Type Casts: {A} Complete Proof of Coq\nModulo Theory},\n  url = {https://doi.org/10.29007/bjpg},\n  volume = {46},\n  year = {2017}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Coupling proofs are probabilistic product programs.\n \n \n \n \n\n\n \n Barthe, G.; Grégoire, B.; Hsu, J.; and Strub, P.\n\n\n \n\n\n\n In Castagna, G.; and Gordon, A. D., editor(s), Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, POPL 2017, Paris, France, January 18-20, 2017, pages 161–174, 2017. ACM\n \n\n\n\n
\n\n\n\n \n \n \"CouplingPaper\n  \n \n\n \n \n doi\n  \n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{DBLP:conf/popl/BartheGHS17,\n  author = {Gilles Barthe and Benjamin Gr{\\'{e}}goire and\nJustin Hsu and Pierre{-}Yves Strub},\n  bibsource = {dblp computer science bibliography, https://dblp.org},\n  biburl = {https://dblp.org/rec/conf/popl/BartheGHS17.bib},\n  booktitle = {Proceedings of the 44th {ACM} {SIGPLAN} Symposium on\nPrinciples of Programming Languages, {POPL} 2017,\nParis, France, January 18-20, 2017},\n  doi = {10.1145/3009837.3009896},\n  editor = {Giuseppe Castagna and Andrew D. Gordon},\n  isbn = {978-1-4503-4660-3},\n  pages = {161--174},\n  publisher = {{ACM}},\n  timestamp = {Mon, 14 Feb 2022 09:20:26 +0100},\n  title = {Coupling proofs are probabilistic product programs},\n  url = {https://doi.org/10.1145/3009837.3009896},\n  year = {2017}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Machine-Checked Proofs of Privacy for Electronic Voting Protocols.\n \n \n \n \n\n\n \n Cortier, V.; Dragan, C. C.; Dupressoir, F.; Schmidt, B.; Strub, P.; and Warinschi, B.\n\n\n \n\n\n\n In 2017 IEEE Symposium on Security and Privacy, SP 2017, San Jose, CA, USA, May 22-26, 2017, pages 993–1008, 2017. IEEE Computer Society\n \n\n\n\n
\n\n\n\n \n \n \"Machine-CheckedPaper\n  \n \n\n \n \n doi\n  \n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{DBLP:conf/sp/CortierDDSSW17,\n  author = {V{\\'{e}}ronique Cortier and Constantin Catalin Dragan and\nFran{\\c{c}}ois Dupressoir and Benedikt Schmidt and\nPierre{-}Yves Strub and Bogdan Warinschi},\n  bibsource = {dblp computer science bibliography, https://dblp.org},\n  biburl = {https://dblp.org/rec/conf/sp/CortierDDSSW17.bib},\n  booktitle = {2017 {IEEE} Symposium on Security and Privacy, {SP}\n2017, San Jose, CA, USA, May 22-26, 2017},\n  doi = {10.1109/SP.2017.28},\n  isbn = {978-1-5090-5533-3},\n  pages = {993--1008},\n  publisher = {{IEEE} Computer Society},\n  timestamp = {Sat, 19 Oct 2019 01:00:00 +0200},\n  title = {Machine-Checked Proofs of Privacy for Electronic\nVoting Protocols},\n  url = {https://doi.org/10.1109/SP.2017.28},\n  year = {2017}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n A messy state of the union: taming the composite state machines of TLS.\n \n \n \n \n\n\n \n Beurdouche, B.; Bhargavan, K.; Delignat-Lavaud, A.; Fournet, C.; Kohlweiss, M.; Pironti, A.; Strub, P.; and Zinzindohoue, J. K.\n\n\n \n\n\n\n Commun. ACM, 60(2): 99–107. 2017.\n \n\n\n\n
\n\n\n\n \n \n \"APaper\n  \n \n\n \n \n doi\n  \n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@article{DBLP:journals/cacm/BeurdoucheBDFKP17,\n  author = {Benjamin Beurdouche and Karthikeyan Bhargavan and\nAntoine Delignat{-}Lavaud and C{\\'{e}}dric Fournet and\nMarkulf Kohlweiss and Alfredo Pironti and\nPierre{-}Yves Strub and Jean Karim Zinzindohoue},\n  bibsource = {dblp computer science bibliography, https://dblp.org},\n  biburl = {https://dblp.org/rec/journals/cacm/BeurdoucheBDFKP17.bib},\n  doi = {10.1145/3023357},\n  journal = {Commun. {ACM}},\n  number = {2},\n  pages = {99--107},\n  timestamp = {Tue, 06 Nov 2018 00:00:00 +0100},\n  title = {A messy state of the union: taming the composite\nstate machines of {TLS}},\n  url = {https://doi.org/10.1145/3023357},\n  volume = {60},\n  year = {2017}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n A relational logic for higher-order programs.\n \n \n \n \n\n\n \n Aguirre, A.; Barthe, G.; Gaboardi, M.; Garg, D.; and Strub, P.\n\n\n \n\n\n\n Proc. ACM Program. Lang., 1(ICFP): 21:1–21:29. 2017.\n \n\n\n\n
\n\n\n\n \n \n \"APaper\n  \n \n\n \n \n doi\n  \n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n  \n \n 2 downloads\n \n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@article{DBLP:journals/pacmpl/AguirreBG0S17,\n  author = {Alejandro Aguirre and Gilles Barthe and\nMarco Gaboardi and Deepak Garg and\nPierre{-}Yves Strub},\n  bibsource = {dblp computer science bibliography, https://dblp.org},\n  biburl = {https://dblp.org/rec/journals/pacmpl/AguirreBG0S17.bib},\n  doi = {10.1145/3110265},\n  journal = {Proc. {ACM} Program. Lang.},\n  number = {{ICFP}},\n  pages = {21:1--21:29},\n  timestamp = {Wed, 17 Feb 2021 00:00:00 +0100},\n  title = {A relational logic for higher-order programs},\n  url = {https://doi.org/10.1145/3110265},\n  volume = {1},\n  year = {2017}\n}\n\n
\n
\n\n\n\n
\n\n\n\n\n\n
\n
\n\n
\n
\n  \n 2016\n \n \n (8)\n \n \n
\n
\n \n \n
\n \n\n \n \n \n \n \n \n Strong Non-Interference and Type-Directed Higher-Order Masking.\n \n \n \n \n\n\n \n Barthe, G.; Belaïd, S.; Dupressoir, F.; Fouque, P.; Grégoire, B.; Strub, P.; and Zucchini, R.\n\n\n \n\n\n\n In Weippl, E. R.; Katzenbeisser, S.; Kruegel, C.; Myers, A. C.; and Halevi, S., editor(s), Proceedings of the 2016 ACM SIGSAC Conference on Computer and Communications Security, Vienna, Austria, October 24-28, 2016, pages 116–129, 2016. ACM\n \n\n\n\n
\n\n\n\n \n \n \"StrongPaper\n  \n \n\n \n \n doi\n  \n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n  \n \n 1 download\n \n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{DBLP:conf/ccs/BartheBDFGSZ16,\n  author = {Gilles Barthe and Sonia Bela{\\"{\\i}}d and\nFran{\\c{c}}ois Dupressoir and Pierre{-}Alain Fouque and\nBenjamin Gr{\\'{e}}goire and Pierre{-}Yves Strub and\nR{\\'{e}}becca Zucchini},\n  bibsource = {dblp computer science bibliography, https://dblp.org},\n  biburl = {https://dblp.org/rec/conf/ccs/BartheBDFGSZ16.bib},\n  booktitle = {Proceedings of the 2016 {ACM} {SIGSAC} Conference on\nComputer and Communications Security, Vienna,\nAustria, October 24-28, 2016},\n  doi = {10.1145/2976749.2978427},\n  editor = {Edgar R. Weippl and Stefan Katzenbeisser and\nChristopher Kruegel and Andrew C. Myers and\nShai Halevi},\n  isbn = {978-1-4503-4139-4},\n  pages = {116--129},\n  publisher = {{ACM}},\n  timestamp = {Tue, 10 Nov 2020 00:00:00 +0100},\n  title = {Strong Non-Interference and Type-Directed\nHigher-Order Masking},\n  url = {https://doi.org/10.1145/2976749.2978427},\n  year = {2016}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Differentially Private Bayesian Programming.\n \n \n \n \n\n\n \n Barthe, G.; Farina, G. P.; Gaboardi, M.; Arias, E. J. G.; Gordon, A.; Hsu, J.; and Strub, P.\n\n\n \n\n\n\n In Weippl, E. R.; Katzenbeisser, S.; Kruegel, C.; Myers, A. C.; and Halevi, S., editor(s), Proceedings of the 2016 ACM SIGSAC Conference on Computer and Communications Security, Vienna, Austria, October 24-28, 2016, pages 68–79, 2016. ACM\n \n\n\n\n
\n\n\n\n \n \n \"DifferentiallyPaper\n  \n \n\n \n \n doi\n  \n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{DBLP:conf/ccs/BartheFGAGHS16,\n  author = {Gilles Barthe and Gian Pietro Farina and\nMarco Gaboardi and Emilio Jes{\\'{u}}s Gallego Arias and\nAndy Gordon and Justin Hsu and Pierre{-}Yves Strub},\n  bibsource = {dblp computer science bibliography, https://dblp.org},\n  biburl = {https://dblp.org/rec/conf/ccs/BartheFGAGHS16.bib},\n  booktitle = {Proceedings of the 2016 {ACM} {SIGSAC} Conference on\nComputer and Communications Security, Vienna,\nAustria, October 24-28, 2016},\n  doi = {10.1145/2976749.2978371},\n  editor = {Edgar R. Weippl and Stefan Katzenbeisser and\nChristopher Kruegel and Andrew C. Myers and\nShai Halevi},\n  isbn = {978-1-4503-4139-4},\n  pages = {68--79},\n  publisher = {{ACM}},\n  timestamp = {Mon, 14 Feb 2022 00:00:00 +0100},\n  title = {Differentially Private Bayesian Programming},\n  url = {https://doi.org/10.1145/2976749.2978371},\n  year = {2016}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Advanced Probabilistic Couplings for Differential Privacy.\n \n \n \n \n\n\n \n Barthe, G.; Fong, N.; Gaboardi, M.; Grégoire, B.; Hsu, J.; and Strub, P.\n\n\n \n\n\n\n In Weippl, E. R.; Katzenbeisser, S.; Kruegel, C.; Myers, A. C.; and Halevi, S., editor(s), Proceedings of the 2016 ACM SIGSAC Conference on Computer and Communications Security, Vienna, Austria, October 24-28, 2016, pages 55–67, 2016. ACM\n \n\n\n\n
\n\n\n\n \n \n \"AdvancedPaper\n  \n \n\n \n \n doi\n  \n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{DBLP:conf/ccs/BartheFGGHS16,\n  author = {Gilles Barthe and No{\\'{e}}mie Fong and\nMarco Gaboardi and Benjamin Gr{\\'{e}}goire and\nJustin Hsu and Pierre{-}Yves Strub},\n  bibsource = {dblp computer science bibliography, https://dblp.org},\n  biburl = {https://dblp.org/rec/conf/ccs/BartheFGGHS16.bib},\n  booktitle = {Proceedings of the 2016 {ACM} {SIGSAC} Conference on\nComputer and Communications Security, Vienna,\nAustria, October 24-28, 2016},\n  doi = {10.1145/2976749.2978391},\n  editor = {Edgar R. Weippl and Stefan Katzenbeisser and\nChristopher Kruegel and Andrew C. Myers and\nShai Halevi},\n  isbn = {978-1-4503-4139-4},\n  pages = {55--67},\n  publisher = {{ACM}},\n  timestamp = {Tue, 10 Nov 2020 20:00:49 +0100},\n  title = {Advanced Probabilistic Couplings for Differential\nPrivacy},\n  url = {https://doi.org/10.1145/2976749.2978391},\n  year = {2016}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Formal proofs of transcendence for e and pi as an application of multivariate and symmetric polynomials.\n \n \n \n \n\n\n \n Bernard, S.; Bertot, Y.; Rideau, L.; and Strub, P.\n\n\n \n\n\n\n In Avigad, J.; and Chlipala, A., editor(s), Proceedings of the 5th ACM SIGPLAN Conference on Certified Programs and Proofs, Saint Petersburg, FL, USA, January 20-22, 2016, pages 76–87, 2016. ACM\n \n\n\n\n
\n\n\n\n \n \n \"FormalPaper\n  \n \n \n \"Formal link\n  \n \n\n \n \n doi\n  \n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{DBLP:conf/cpp/BernardBRS16,\n  author = {Sophie Bernard and Yves Bertot and Laurence Rideau and\nPierre{-}Yves Strub},\n  bibsource = {dblp computer science bibliography, https://dblp.org},\n  biburl = {https://dblp.org/rec/conf/cpp/BernardBRS16.bib},\n  booktitle = {Proceedings of the 5th {ACM} {SIGPLAN} Conference on\nCertified Programs and Proofs, Saint Petersburg, FL,\nUSA, January 20-22, 2016},\n  doi = {10.1145/2854065.2854072},\n  editor = {Jeremy Avigad and Adam Chlipala},\n  isbn = {978-1-4503-4127-1},\n  pages = {76--87},\n  publisher = {{ACM}},\n  timestamp = {Tue, 06 Nov 2018 00:00:00 +0100},\n  title = {Formal proofs of transcendence for e and pi as an\napplication of multivariate and symmetric\npolynomials},\n  url = {https://doi.org/10.1145/2854065.2854072},\n  url_Link = {http://www.strub.nu/biblio/pdf/conf-cpp-BernardBRS16.pdf},\n  year = {2016}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n A Program Logic for Union Bounds.\n \n \n \n \n\n\n \n Barthe, G.; Gaboardi, M.; Grégoire, B.; Hsu, J.; and Strub, P.\n\n\n \n\n\n\n In Chatzigiannakis, I.; Mitzenmacher, M.; Rabani, Y.; and Sangiorgi, D., editor(s), 43rd International Colloquium on Automata, Languages, and Programming, ICALP 2016, July 11-15, 2016, Rome, Italy, volume 55, of LIPIcs, pages 107:1–107:15, 2016. Schloss Dagstuhl - Leibniz-Zentrum für Informatik\n \n\n\n\n
\n\n\n\n \n \n \"APaper\n  \n \n \n \"A link\n  \n \n\n \n \n doi\n  \n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{DBLP:conf/icalp/BartheGGHS16,\n  author = {Gilles Barthe and Marco Gaboardi and\nBenjamin Gr{\\'{e}}goire and Justin Hsu and\nPierre{-}Yves Strub},\n  bibsource = {dblp computer science bibliography, https://dblp.org},\n  biburl = {https://dblp.org/rec/conf/icalp/BartheGGHS16.bib},\n  booktitle = {43rd International Colloquium on Automata, Languages,\nand Programming, {ICALP} 2016, July 11-15, 2016,\nRome, Italy},\n  doi = {10.4230/LIPIcs.ICALP.2016.107},\n  editor = {Ioannis Chatzigiannakis and Michael Mitzenmacher and\nYuval Rabani and Davide Sangiorgi},\n  isbn = {978-3-95977-013-2},\n  pages = {107:1--107:15},\n  publisher = {Schloss Dagstuhl - Leibniz-Zentrum f{\\"{u}}r\nInformatik},\n  series = {LIPIcs},\n  timestamp = {Mon, 15 Jun 2020 01:00:00 +0200},\n  title = {A Program Logic for Union Bounds},\n  url = {https://doi.org/10.4230/LIPIcs.ICALP.2016.107},\n  url_Link = {http://www.strub.nu/biblio/pdf/conf-icalp-BartheGGHS16.pdf},\n  volume = {55},\n  year = {2016}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Proving Differential Privacy via Probabilistic Couplings.\n \n \n \n \n\n\n \n Barthe, G.; Gaboardi, M.; Grégoire, B.; Hsu, J.; and Strub, P.\n\n\n \n\n\n\n In Grohe, M.; Koskinen, E.; and Shankar, N., editor(s), Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science, LICS '16, New York, NY, USA, July 5-8, 2016, pages 749–758, 2016. ACM\n \n\n\n\n
\n\n\n\n \n \n \"ProvingPaper\n  \n \n\n \n \n doi\n  \n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{DBLP:conf/lics/BartheGGHS16,\n  author = {Gilles Barthe and Marco Gaboardi and\nBenjamin Gr{\\'{e}}goire and Justin Hsu and\nPierre{-}Yves Strub},\n  bibsource = {dblp computer science bibliography, https://dblp.org},\n  biburl = {https://dblp.org/rec/conf/lics/BartheGGHS16.bib},\n  booktitle = {Proceedings of the 31st Annual {ACM/IEEE} Symposium\non Logic in Computer Science, {LICS} '16, New York,\nNY, USA, July 5-8, 2016},\n  doi = {10.1145/2933575.2934554},\n  editor = {Martin Grohe and Eric Koskinen and Natarajan Shankar},\n  isbn = {978-1-4503-4391-6},\n  pages = {749--758},\n  publisher = {{ACM}},\n  timestamp = {Wed, 11 Aug 2021 01:00:00 +0200},\n  title = {Proving Differential Privacy via Probabilistic\nCouplings},\n  url = {https://doi.org/10.1145/2933575.2934554},\n  year = {2016}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Dependent types and multi-monadic effects in F.\n \n \n \n \n\n\n \n Swamy, N.; Hritcu, C.; Keller, C.; Rastogi, A.; Delignat-Lavaud, A.; Forest, S.; Bhargavan, K.; Fournet, C.; Strub, P.; Kohlweiss, M.; Zinzindohoue, J. K.; and Béguelin, S. Z.\n\n\n \n\n\n\n In Bodík, R.; and Majumdar, R., editor(s), Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2016, St. Petersburg, FL, USA, January 20 - 22, 2016, pages 256–270, 2016. ACM\n \n\n\n\n
\n\n\n\n \n \n \"DependentPaper\n  \n \n \n \"Dependent link\n  \n \n\n \n \n doi\n  \n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n  \n \n 1 download\n \n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{DBLP:conf/popl/SwamyHKRDFBFSKZ16,\n  author = {Nikhil Swamy and Catalin Hritcu and Chantal Keller and\nAseem Rastogi and Antoine Delignat{-}Lavaud and\nSimon Forest and Karthikeyan Bhargavan and\nC{\\'{e}}dric Fournet and Pierre{-}Yves Strub and\nMarkulf Kohlweiss and Jean Karim Zinzindohoue and\nSantiago Zanella B{\\'{e}}guelin},\n  bibsource = {dblp computer science bibliography, https://dblp.org},\n  biburl = {https://dblp.org/rec/conf/popl/SwamyHKRDFBFSKZ16.bib},\n  booktitle = {Proceedings of the 43rd Annual {ACM} {SIGPLAN-SIGACT}\nSymposium on Principles of Programming Languages,\n{POPL} 2016, St. Petersburg, FL, USA, January 20 -\n22, 2016},\n  doi = {10.1145/2837614.2837655},\n  editor = {Rastislav Bod{\\'{\\i}}k and Rupak Majumdar},\n  isbn = {978-1-4503-3549-2},\n  pages = {256--270},\n  publisher = {{ACM}},\n  timestamp = {Wed, 23 Jun 2021 15:34:31 +0200},\n  title = {Dependent types and multi-monadic effects in {F}},\n  url = {https://doi.org/10.1145/2837614.2837655},\n  url_Link = {http://www.strub.nu/biblio/pdf/conf-popl-SwamyHKRDFBFSKZ16.pdf},\n  year = {2016}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Computer-Aided Verification for Mechanism Design.\n \n \n \n \n\n\n \n Barthe, G.; Gaboardi, M.; Arias, E. J. G.; Hsu, J.; Roth, A.; and Strub, P.\n\n\n \n\n\n\n In Cai, Y.; and Vetta, A., editor(s), Web and Internet Economics - 12th International Conference, WINE 2016, Montreal, Canada, December 11-14, 2016, Proceedings, volume 10123, of Lecture Notes in Computer Science, pages 279–293, 2016. Springer\n \n\n\n\n
\n\n\n\n \n \n \"Computer-AidedPaper\n  \n \n\n \n \n doi\n  \n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{DBLP:conf/wine/BartheGAHRS16,\n  author = {Gilles Barthe and Marco Gaboardi and\nEmilio Jes{\\'{u}}s Gallego Arias and Justin Hsu and\nAaron Roth and Pierre{-}Yves Strub},\n  bibsource = {dblp computer science bibliography, https://dblp.org},\n  biburl = {https://dblp.org/rec/conf/wine/BartheGAHRS16.bib},\n  booktitle = {Web and Internet Economics - 12th International\nConference, {WINE} 2016, Montreal, Canada, December\n11-14, 2016, Proceedings},\n  doi = {10.1007/978-3-662-54110-4\\_20},\n  editor = {Yang Cai and Adrian Vetta},\n  isbn = {978-3-662-54109-8},\n  pages = {279--293},\n  publisher = {Springer},\n  series = {Lecture Notes in Computer Science},\n  timestamp = {Sat, 09 Apr 2022 12:47:11 +0200},\n  title = {Computer-Aided Verification for Mechanism Design},\n  url = {https://doi.org/10.1007/978-3-662-54110-4\\_20},\n  volume = {10123},\n  year = {2016}\n}\n\n
\n
\n\n\n\n
\n\n\n\n\n\n
\n
\n\n
\n
\n  \n 2015\n \n \n (4)\n \n \n
\n
\n \n \n
\n \n\n \n \n \n \n \n \n Verified Proofs of Higher-Order Masking.\n \n \n \n \n\n\n \n Barthe, G.; Belaïd, S.; Dupressoir, F.; Fouque, P.; Grégoire, B.; and Strub, P.\n\n\n \n\n\n\n In Oswald, E.; and Fischlin, M., editor(s), Advances in Cryptology - EUROCRYPT 2015 - 34th Annual International Conference on the Theory and Applications of Cryptographic Techniques, Sofia, Bulgaria, April 26-30, 2015, Proceedings, Part I, volume 9056, of Lecture Notes in Computer Science, pages 457–485, 2015. Springer\n \n\n\n\n
\n\n\n\n \n \n \"VerifiedPaper\n  \n \n\n \n \n doi\n  \n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{DBLP:conf/eurocrypt/BartheBDFGS15,\n  author = {Gilles Barthe and Sonia Bela{\\"{\\i}}d and\nFran{\\c{c}}ois Dupressoir and Pierre{-}Alain Fouque and\nBenjamin Gr{\\'{e}}goire and Pierre{-}Yves Strub},\n  bibsource = {dblp computer science bibliography, https://dblp.org},\n  biburl = {https://dblp.org/rec/conf/eurocrypt/BartheBDFGS15.bib},\n  booktitle = {Advances in Cryptology - {EUROCRYPT} 2015 - 34th\nAnnual International Conference on the Theory and\nApplications of Cryptographic Techniques, Sofia,\nBulgaria, April 26-30, 2015, Proceedings, Part {I}},\n  doi = {10.1007/978-3-662-46800-5\\_18},\n  editor = {Elisabeth Oswald and Marc Fischlin},\n  isbn = {978-3-662-46799-2},\n  pages = {457--485},\n  publisher = {Springer},\n  series = {Lecture Notes in Computer Science},\n  timestamp = {Thu, 14 Oct 2021 09:58:16 +0200},\n  title = {Verified Proofs of Higher-Order Masking},\n  url = {https://doi.org/10.1007/978-3-662-46800-5\\_18},\n  volume = {9056},\n  year = {2015}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Relational Reasoning via Probabilistic Coupling.\n \n \n \n \n\n\n \n Barthe, G.; Espitau, T.; Grégoire, B.; Hsu, J.; Stefanesco, L.; and Strub, P.\n\n\n \n\n\n\n In Davis, M.; Fehnker, A.; McIver, A.; and Voronkov, A., editor(s), Logic for Programming, Artificial Intelligence, and Reasoning - 20th International Conference, LPAR-20 2015, Suva, Fiji, November 24-28, 2015, Proceedings, volume 9450, of Lecture Notes in Computer Science, pages 387–401, 2015. Springer\n \n\n\n\n
\n\n\n\n \n \n \"RelationalPaper\n  \n \n\n \n \n doi\n  \n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{DBLP:conf/lpar/BartheEGHSS15,\n  author = {Gilles Barthe and Thomas Espitau and\nBenjamin Gr{\\'{e}}goire and Justin Hsu and\nL{\\'{e}}o Stefanesco and Pierre{-}Yves Strub},\n  bibsource = {dblp computer science bibliography, https://dblp.org},\n  biburl = {https://dblp.org/rec/conf/lpar/BartheEGHSS15.bib},\n  booktitle = {Logic for Programming, Artificial Intelligence, and\nReasoning - 20th International Conference, {LPAR-20}\n2015, Suva, Fiji, November 24-28, 2015, Proceedings},\n  doi = {10.1007/978-3-662-48899-7\\_27},\n  editor = {Martin Davis and Ansgar Fehnker and Annabelle McIver and\nAndrei Voronkov},\n  isbn = {978-3-662-48898-0},\n  pages = {387--401},\n  publisher = {Springer},\n  series = {Lecture Notes in Computer Science},\n  timestamp = {Mon, 03 Jan 2022 22:31:30 +0100},\n  title = {Relational Reasoning via Probabilistic Coupling},\n  url = {https://doi.org/10.1007/978-3-662-48899-7\\_27},\n  volume = {9450},\n  year = {2015}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Higher-Order Approximate Relational Refinement Types for Mechanism Design and Differential Privacy.\n \n \n \n \n\n\n \n Barthe, G.; Gaboardi, M.; Arias, E. J. G.; Hsu, J.; Roth, A.; and Strub, P.\n\n\n \n\n\n\n In Rajamani, S. K.; and Walker, D., editor(s), Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2015, Mumbai, India, January 15-17, 2015, pages 55–68, 2015. ACM\n \n\n\n\n
\n\n\n\n \n \n \"Higher-OrderPaper\n  \n \n\n \n \n doi\n  \n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{DBLP:conf/popl/BartheGAHRS15,\n  author = {Gilles Barthe and Marco Gaboardi and\nEmilio Jes{\\'{u}}s Gallego Arias and Justin Hsu and\nAaron Roth and Pierre{-}Yves Strub},\n  bibsource = {dblp computer science bibliography, https://dblp.org},\n  biburl = {https://dblp.org/rec/conf/popl/BartheGAHRS15.bib},\n  booktitle = {Proceedings of the 42nd Annual {ACM} {SIGPLAN-SIGACT}\nSymposium on Principles of Programming Languages,\n{POPL} 2015, Mumbai, India, January 15-17, 2015},\n  doi = {10.1145/2676726.2677000},\n  editor = {Sriram K. Rajamani and David Walker},\n  isbn = {978-1-4503-3300-9},\n  pages = {55--68},\n  publisher = {{ACM}},\n  timestamp = {Wed, 23 Jun 2021 17:06:05 +0200},\n  title = {Higher-Order Approximate Relational Refinement Types\nfor Mechanism Design and Differential Privacy},\n  url = {https://doi.org/10.1145/2676726.2677000},\n  year = {2015}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n A Messy State of the Union: Taming the Composite State Machines of TLS.\n \n \n \n \n\n\n \n Beurdouche, B.; Bhargavan, K.; Delignat-Lavaud, A.; Fournet, C.; Kohlweiss, M.; Pironti, A.; Strub, P.; and Zinzindohoue, J. K.\n\n\n \n\n\n\n In 2015 IEEE Symposium on Security and Privacy, SP 2015, San Jose, CA, USA, May 17-21, 2015, pages 535–552, 2015. IEEE Computer Society\n \n\n\n\n
\n\n\n\n \n \n \"APaper\n  \n \n\n \n \n doi\n  \n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{DBLP:conf/sp/BeurdoucheBDFKP15,\n  author = {Benjamin Beurdouche and Karthikeyan Bhargavan and\nAntoine Delignat{-}Lavaud and C{\\'{e}}dric Fournet and\nMarkulf Kohlweiss and Alfredo Pironti and\nPierre{-}Yves Strub and Jean Karim Zinzindohoue},\n  bibsource = {dblp computer science bibliography, https://dblp.org},\n  biburl = {https://dblp.org/rec/conf/sp/BeurdoucheBDFKP15.bib},\n  booktitle = {2015 {IEEE} Symposium on Security and Privacy, {SP}\n2015, San Jose, CA, USA, May 17-21, 2015},\n  doi = {10.1109/SP.2015.39},\n  isbn = {978-1-4673-6949-7},\n  pages = {535--552},\n  publisher = {{IEEE} Computer Society},\n  timestamp = {Wed, 16 Oct 2019 14:14:51 +0200},\n  title = {A Messy State of the Union: Taming the Composite\nState Machines of {TLS}},\n  url = {https://doi.org/10.1109/SP.2015.39},\n  year = {2015}\n}\n\n
\n
\n\n\n\n
\n\n\n\n\n\n
\n
\n\n
\n
\n  \n 2014\n \n \n (7)\n \n \n
\n
\n \n \n
\n \n\n \n \n \n \n \n \n Proving the TLS Handshake Secure (As It Is).\n \n \n \n \n\n\n \n Bhargavan, K.; Fournet, C.; Kohlweiss, M.; Pironti, A.; Strub, P.; and Béguelin, S. Z.\n\n\n \n\n\n\n In Garay, J. A.; and Gennaro, R., editor(s), Advances in Cryptology - CRYPTO 2014 - 34th Annual Cryptology Conference, Santa Barbara, CA, USA, August 17-21, 2014, Proceedings, Part II, volume 8617, of Lecture Notes in Computer Science, pages 235–255, 2014. Springer\n \n\n\n\n
\n\n\n\n \n \n \"ProvingPaper\n  \n \n\n \n \n doi\n  \n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{DBLP:conf/crypto/BhargavanFKPSB14,\n  author = {Karthikeyan Bhargavan and C{\\'{e}}dric Fournet and\nMarkulf Kohlweiss and Alfredo Pironti and\nPierre{-}Yves Strub and\nSantiago Zanella B{\\'{e}}guelin},\n  bibsource = {dblp computer science bibliography, https://dblp.org},\n  biburl = {https://dblp.org/rec/conf/crypto/BhargavanFKPSB14.bib},\n  booktitle = {Advances in Cryptology - {CRYPTO} 2014 - 34th Annual\nCryptology Conference, Santa Barbara, CA, USA, August\n17-21, 2014, Proceedings, Part {II}},\n  doi = {10.1007/978-3-662-44381-1\\_14},\n  editor = {Juan A. Garay and Rosario Gennaro},\n  isbn = {978-3-662-44380-4},\n  pages = {235--255},\n  publisher = {Springer},\n  series = {Lecture Notes in Computer Science},\n  timestamp = {Sun, 25 Oct 2020 01:00:00 +0200},\n  title = {Proving the {TLS} Handshake Secure (As It Is)},\n  url = {https://doi.org/10.1007/978-3-662-44381-1\\_14},\n  volume = {8617},\n  year = {2014}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Certified Synthesis of Efficient Batch Verifiers.\n \n \n \n \n\n\n \n Akinyele, J. A.; Barthe, G.; Grégoire, B.; Schmidt, B.; and Strub, P.\n\n\n \n\n\n\n In IEEE 27th Computer Security Foundations Symposium, CSF 2014, Vienna, Austria, 19-22 July, 2014, pages 153–165, 2014. IEEE Computer Society\n \n\n\n\n
\n\n\n\n \n \n \"CertifiedPaper\n  \n \n\n \n \n doi\n  \n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{DBLP:conf/csfw/AkinyeleBGSS14,\n  author = {Joseph A. Akinyele and Gilles Barthe and\nBenjamin Gr{\\'{e}}goire and Benedikt Schmidt and\nPierre{-}Yves Strub},\n  bibsource = {dblp computer science bibliography, https://dblp.org},\n  biburl = {https://dblp.org/rec/conf/csfw/AkinyeleBGSS14.bib},\n  booktitle = {{IEEE} 27th Computer Security Foundations Symposium,\n{CSF} 2014, Vienna, Austria, 19-22 July, 2014},\n  doi = {10.1109/CSF.2014.19},\n  isbn = {978-1-4799-4290-9},\n  pages = {153--165},\n  publisher = {{IEEE} Computer Society},\n  timestamp = {Sat, 19 Oct 2019 01:00:00 +0200},\n  title = {Certified Synthesis of Efficient Batch Verifiers},\n  url = {https://doi.org/10.1109/CSF.2014.19},\n  year = {2014}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Proving Differential Privacy in Hoare Logic.\n \n \n \n \n\n\n \n Barthe, G.; Gaboardi, M.; Arias, E. J. G.; Hsu, J.; Kunz, C.; and Strub, P.\n\n\n \n\n\n\n In IEEE 27th Computer Security Foundations Symposium, CSF 2014, Vienna, Austria, 19-22 July, 2014, pages 411–424, 2014. IEEE Computer Society\n \n\n\n\n
\n\n\n\n \n \n \"ProvingPaper\n  \n \n\n \n \n doi\n  \n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{DBLP:conf/csfw/BartheGAHKS14,\n  author = {Gilles Barthe and Marco Gaboardi and\nEmilio Jes{\\'{u}}s Gallego Arias and Justin Hsu and\nC{\\'{e}}sar Kunz and Pierre{-}Yves Strub},\n  bibsource = {dblp computer science bibliography, https://dblp.org},\n  biburl = {https://dblp.org/rec/conf/csfw/BartheGAHKS14.bib},\n  booktitle = {{IEEE} 27th Computer Security Foundations Symposium,\n{CSF} 2014, Vienna, Austria, 19-22 July, 2014},\n  doi = {10.1109/CSF.2014.36},\n  isbn = {978-1-4799-4290-9},\n  pages = {411--424},\n  publisher = {{IEEE} Computer Society},\n  timestamp = {Sat, 19 Oct 2019 01:00:00 +0200},\n  title = {Proving Differential Privacy in Hoare Logic},\n  url = {https://doi.org/10.1109/CSF.2014.36},\n  year = {2014}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n A Formal Library for Elliptic Curves in the Coq Proof Assistant.\n \n \n \n \n\n\n \n Bartzia, E.; and Strub, P.\n\n\n \n\n\n\n In Klein, G.; and Gamboa, R., editor(s), Interactive Theorem Proving - 5th International Conference, ITP 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 14-17, 2014. Proceedings, volume 8558, of Lecture Notes in Computer Science, pages 77–92, 2014. Springer\n \n\n\n\n
\n\n\n\n \n \n \"APaper\n  \n \n\n \n \n doi\n  \n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{DBLP:conf/itp/BartziaS14,\n  author = {Evmorfia{-}Iro Bartzia and Pierre{-}Yves Strub},\n  bibsource = {dblp computer science bibliography, https://dblp.org},\n  biburl = {https://dblp.org/rec/conf/itp/BartziaS14.bib},\n  booktitle = {Interactive Theorem Proving - 5th International\nConference, {ITP} 2014, Held as Part of the Vienna\nSummer of Logic, {VSL} 2014, Vienna, Austria, July\n14-17, 2014. Proceedings},\n  doi = {10.1007/978-3-319-08970-6\\_6},\n  editor = {Gerwin Klein and Ruben Gamboa},\n  isbn = {978-3-319-08969-0},\n  pages = {77--92},\n  publisher = {Springer},\n  series = {Lecture Notes in Computer Science},\n  timestamp = {Tue, 14 May 2019 10:00:37 +0200},\n  title = {A Formal Library for Elliptic Curves in the Coq Proof\nAssistant},\n  url = {https://doi.org/10.1007/978-3-319-08970-6\\_6},\n  volume = {8558},\n  year = {2014}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Probabilistic relational verification for cryptographic implementations.\n \n \n \n \n\n\n \n Barthe, G.; Fournet, C.; Grégoire, B.; Strub, P.; Swamy, N.; and Béguelin, S. Z.\n\n\n \n\n\n\n In Jagannathan, S.; and Sewell, P., editor(s), The 41st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL '14, San Diego, CA, USA, January 20-21, 2014, pages 193–206, 2014. ACM\n \n\n\n\n
\n\n\n\n \n \n \"ProbabilisticPaper\n  \n \n\n \n \n doi\n  \n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{DBLP:conf/popl/BartheFGSSB14,\n  author = {Gilles Barthe and C{\\'{e}}dric Fournet and\nBenjamin Gr{\\'{e}}goire and Pierre{-}Yves Strub and\nNikhil Swamy and Santiago Zanella B{\\'{e}}guelin},\n  bibsource = {dblp computer science bibliography, https://dblp.org},\n  biburl = {https://dblp.org/rec/conf/popl/BartheFGSSB14.bib},\n  booktitle = {The 41st Annual {ACM} {SIGPLAN-SIGACT} Symposium on\nPrinciples of Programming Languages, {POPL} '14, San\nDiego, CA, USA, January 20-21, 2014},\n  doi = {10.1145/2535838.2535847},\n  editor = {Suresh Jagannathan and Peter Sewell},\n  isbn = {978-1-4503-2544-8},\n  pages = {193--206},\n  publisher = {{ACM}},\n  timestamp = {Thu, 24 Jun 2021 16:19:31 +0200},\n  title = {Probabilistic relational verification for\ncryptographic implementations},\n  url = {https://doi.org/10.1145/2535838.2535847},\n  year = {2014}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Gradual typing embedded securely in JavaScript.\n \n \n \n \n\n\n \n Swamy, N.; Fournet, C.; Rastogi, A.; Bhargavan, K.; Chen, J.; Strub, P.; and Bierman, G. M.\n\n\n \n\n\n\n In Jagannathan, S.; and Sewell, P., editor(s), The 41st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL '14, San Diego, CA, USA, January 20-21, 2014, pages 425–438, 2014. ACM\n \n\n\n\n
\n\n\n\n \n \n \"GradualPaper\n  \n \n\n \n \n doi\n  \n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{DBLP:conf/popl/SwamyFRBCSB14,\n  author = {Nikhil Swamy and C{\\'{e}}dric Fournet and\nAseem Rastogi and Karthikeyan Bhargavan and Juan Chen and\nPierre{-}Yves Strub and Gavin M. Bierman},\n  bibsource = {dblp computer science bibliography, https://dblp.org},\n  biburl = {https://dblp.org/rec/conf/popl/SwamyFRBCSB14.bib},\n  booktitle = {The 41st Annual {ACM} {SIGPLAN-SIGACT} Symposium on\nPrinciples of Programming Languages, {POPL} '14, San\nDiego, CA, USA, January 20-21, 2014},\n  doi = {10.1145/2535838.2535889},\n  editor = {Suresh Jagannathan and Peter Sewell},\n  isbn = {978-1-4503-2544-8},\n  pages = {425--438},\n  publisher = {{ACM}},\n  timestamp = {Thu, 24 Jun 2021 01:00:00 +0200},\n  title = {Gradual typing embedded securely in JavaScript},\n  url = {https://doi.org/10.1145/2535838.2535889},\n  year = {2014}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Triple Handshakes and Cookie Cutters: Breaking and Fixing Authentication over TLS.\n \n \n \n \n\n\n \n Bhargavan, K.; Delignat-Lavaud, A.; Fournet, C.; Pironti, A.; and Strub, P.\n\n\n \n\n\n\n In 2014 IEEE Symposium on Security and Privacy, SP 2014, Berkeley, CA, USA, May 18-21, 2014, pages 98–113, 2014. IEEE Computer Society\n \n\n\n\n
\n\n\n\n \n \n \"TriplePaper\n  \n \n\n \n \n doi\n  \n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{DBLP:conf/sp/BhargavanDFPS14,\n  author = {Karthikeyan Bhargavan and Antoine Delignat{-}Lavaud and\nC{\\'{e}}dric Fournet and Alfredo Pironti and\nPierre{-}Yves Strub},\n  bibsource = {dblp computer science bibliography, https://dblp.org},\n  biburl = {https://dblp.org/rec/conf/sp/BhargavanDFPS14.bib},\n  booktitle = {2014 {IEEE} Symposium on Security and Privacy, {SP}\n2014, Berkeley, CA, USA, May 18-21, 2014},\n  doi = {10.1109/SP.2014.14},\n  isbn = {978-1-4799-4686-0},\n  pages = {98--113},\n  publisher = {{IEEE} Computer Society},\n  timestamp = {Wed, 16 Oct 2019 14:14:51 +0200},\n  title = {Triple Handshakes and Cookie Cutters: Breaking and\nFixing Authentication over {TLS}},\n  url = {https://doi.org/10.1109/SP.2014.14},\n  year = {2014}\n}\n\n
\n
\n\n\n\n
\n\n\n\n\n\n
\n
\n\n
\n
\n  \n 2013\n \n \n (4)\n \n \n
\n
\n \n \n
\n \n\n \n \n \n \n \n \n EasyCrypt: A Tutorial.\n \n \n \n \n\n\n \n Barthe, G.; Dupressoir, F.; Grégoire, B.; Kunz, C.; Schmidt, B.; and Strub, P.\n\n\n \n\n\n\n In Aldini, A.; López, J.; and Martinelli, F., editor(s), Foundations of Security Analysis and Design VII - FOSAD 2012/2013 Tutorial Lectures, volume 8604, of Lecture Notes in Computer Science, pages 146–166, 2013. Springer\n \n\n\n\n
\n\n\n\n \n \n \"EasyCrypt:Paper\n  \n \n\n \n \n doi\n  \n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{DBLP:conf/fosad/BartheDGKSS13,\n  author = {Gilles Barthe and Fran{\\c{c}}ois Dupressoir and\nBenjamin Gr{\\'{e}}goire and C{\\'{e}}sar Kunz and\nBenedikt Schmidt and Pierre{-}Yves Strub},\n  bibsource = {dblp computer science bibliography, https://dblp.org},\n  biburl = {https://dblp.org/rec/conf/fosad/BartheDGKSS13.bib},\n  booktitle = {Foundations of Security Analysis and Design {VII} -\n{FOSAD} 2012/2013 Tutorial Lectures},\n  doi = {10.1007/978-3-319-10082-1\\_6},\n  editor = {Alessandro Aldini and Javier L{\\'{o}}pez and\nFabio Martinelli},\n  isbn = {978-3-319-10081-4},\n  pages = {146--166},\n  publisher = {Springer},\n  series = {Lecture Notes in Computer Science},\n  timestamp = {Thu, 29 Aug 2019 08:10:01 +0200},\n  title = {EasyCrypt: {A} Tutorial},\n  url = {https://doi.org/10.1007/978-3-319-10082-1\\_6},\n  volume = {8604},\n  year = {2013}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Fully abstract compilation to JavaScript.\n \n \n \n \n\n\n \n Fournet, C.; Swamy, N.; Chen, J.; Dagand, P.; Strub, P.; and Livshits, B.\n\n\n \n\n\n\n In Giacobazzi, R.; and Cousot, R., editor(s), The 40th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL '13, Rome, Italy - January 23 - 25, 2013, pages 371–384, 2013. ACM\n \n\n\n\n
\n\n\n\n \n \n \"FullyPaper\n  \n \n\n \n \n doi\n  \n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n  \n \n 1 download\n \n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{DBLP:conf/popl/FournetSCDSL13,\n  author = {C{\\'{e}}dric Fournet and Nikhil Swamy and Juan Chen and\nPierre{-}{\\'{E}}variste Dagand and\nPierre{-}Yves Strub and Benjamin Livshits},\n  bibsource = {dblp computer science bibliography, https://dblp.org},\n  biburl = {https://dblp.org/rec/conf/popl/FournetSCDSL13.bib},\n  booktitle = {The 40th Annual {ACM} {SIGPLAN-SIGACT} Symposium on\nPrinciples of Programming Languages, {POPL} '13,\nRome, Italy - January 23 - 25, 2013},\n  doi = {10.1145/2429069.2429114},\n  editor = {Roberto Giacobazzi and Radhia Cousot},\n  isbn = {978-1-4503-1832-7},\n  pages = {371--384},\n  publisher = {{ACM}},\n  timestamp = {Thu, 24 Jun 2021 16:19:31 +0200},\n  title = {Fully abstract compilation to JavaScript},\n  url = {https://doi.org/10.1145/2429069.2429114},\n  year = {2013}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Implementing TLS with Verified Cryptographic Security.\n \n \n \n \n\n\n \n Bhargavan, K.; Fournet, C.; Kohlweiss, M.; Pironti, A.; and Strub, P.\n\n\n \n\n\n\n In 2013 IEEE Symposium on Security and Privacy, SP 2013, Berkeley, CA, USA, May 19-22, 2013, pages 445–459, 2013. IEEE Computer Society\n \n\n\n\n
\n\n\n\n \n \n \"ImplementingPaper\n  \n \n\n \n \n doi\n  \n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{DBLP:conf/sp/BhargavanFKPS13,\n  author = {Karthikeyan Bhargavan and C{\\'{e}}dric Fournet and\nMarkulf Kohlweiss and Alfredo Pironti and\nPierre{-}Yves Strub},\n  bibsource = {dblp computer science bibliography, https://dblp.org},\n  biburl = {https://dblp.org/rec/conf/sp/BhargavanFKPS13.bib},\n  booktitle = {2013 {IEEE} Symposium on Security and Privacy, {SP}\n2013, Berkeley, CA, USA, May 19-22, 2013},\n  doi = {10.1109/SP.2013.37},\n  isbn = {978-1-4673-6166-8},\n  pages = {445--459},\n  publisher = {{IEEE} Computer Society},\n  timestamp = {Wed, 16 Oct 2019 14:14:51 +0200},\n  title = {Implementing {TLS} with Verified Cryptographic\nSecurity},\n  url = {https://doi.org/10.1109/SP.2013.37},\n  year = {2013}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Secure distributed programming with value-dependent types.\n \n \n \n \n\n\n \n Swamy, N.; Chen, J.; Fournet, C.; Strub, P.; Bhargavan, K.; and Yang, J.\n\n\n \n\n\n\n J. Funct. Program., 23(4): 402–451. 2013.\n \n\n\n\n
\n\n\n\n \n \n \"SecurePaper\n  \n \n\n \n \n doi\n  \n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n  \n \n 2 downloads\n \n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@article{DBLP:journals/jfp/SwamyCFSBY13,\n  author = {Nikhil Swamy and Juan Chen and C{\\'{e}}dric Fournet and\nPierre{-}Yves Strub and Karthikeyan Bhargavan and\nJean Yang},\n  bibsource = {dblp computer science bibliography, https://dblp.org},\n  biburl = {https://dblp.org/rec/journals/jfp/SwamyCFSBY13.bib},\n  doi = {10.1017/S0956796813000142},\n  journal = {J. Funct. Program.},\n  number = {4},\n  pages = {402--451},\n  timestamp = {Thu, 03 Sep 2020 01:00:00 +0200},\n  title = {Secure distributed programming with value-dependent\ntypes},\n  url = {https://doi.org/10.1017/S0956796813000142},\n  volume = {23},\n  year = {2013}\n}\n\n
\n
\n\n\n\n
\n\n\n\n\n\n
\n
\n\n
\n
\n  \n 2012\n \n \n (1)\n \n \n
\n
\n \n \n
\n \n\n \n \n \n \n \n \n Self-certification: bootstrapping certified typecheckers in F* with Coq.\n \n \n \n \n\n\n \n Strub, P.; Swamy, N.; Fournet, C.; and Chen, J.\n\n\n \n\n\n\n In Field, J.; and Hicks, M., editor(s), Proceedings of the 39th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2012, Philadelphia, Pennsylvania, USA, January 22-28, 2012, pages 571–584, 2012. ACM\n \n\n\n\n
\n\n\n\n \n \n \"Self-certification:Paper\n  \n \n\n \n \n doi\n  \n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n  \n \n 2 downloads\n \n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{DBLP:conf/popl/StrubSFC12,\n  author = {Pierre{-}Yves Strub and Nikhil Swamy and\nC{\\'{e}}dric Fournet and Juan Chen},\n  bibsource = {dblp computer science bibliography, https://dblp.org},\n  biburl = {https://dblp.org/rec/conf/popl/StrubSFC12.bib},\n  booktitle = {Proceedings of the 39th {ACM} {SIGPLAN-SIGACT}\nSymposium on Principles of Programming Languages,\n{POPL} 2012, Philadelphia, Pennsylvania, USA, January\n22-28, 2012},\n  doi = {10.1145/2103656.2103723},\n  editor = {John Field and Michael Hicks},\n  isbn = {978-1-4503-1083-3},\n  pages = {571--584},\n  publisher = {{ACM}},\n  timestamp = {Thu, 24 Jun 2021 16:19:31 +0200},\n  title = {Self-certification: bootstrapping certified\ntypecheckers in F* with Coq},\n  url = {https://doi.org/10.1145/2103656.2103723},\n  year = {2012}\n}\n\n
\n
\n\n\n\n
\n\n\n\n\n\n
\n
\n\n
\n
\n  \n 2011\n \n \n (3)\n \n \n
\n
\n \n \n
\n \n\n \n \n \n \n \n \n Modular code-based cryptographic verification.\n \n \n \n \n\n\n \n Fournet, C.; Kohlweiss, M.; and Strub, P.\n\n\n \n\n\n\n In Chen, Y.; Danezis, G.; and Shmatikov, V., editor(s), Proceedings of the 18th ACM Conference on Computer and Communications Security, CCS 2011, Chicago, Illinois, USA, October 17-21, 2011, pages 341–350, 2011. ACM\n \n\n\n\n
\n\n\n\n \n \n \"ModularPaper\n  \n \n\n \n \n doi\n  \n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n  \n \n 1 download\n \n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{DBLP:conf/ccs/FournetKS11,\n  author = {C{\\'{e}}dric Fournet and Markulf Kohlweiss and\nPierre{-}Yves Strub},\n  bibsource = {dblp computer science bibliography, https://dblp.org},\n  biburl = {https://dblp.org/rec/conf/ccs/FournetKS11.bib},\n  booktitle = {Proceedings of the 18th {ACM} Conference on Computer\nand Communications Security, {CCS} 2011, Chicago,\nIllinois, USA, October 17-21, 2011},\n  doi = {10.1145/2046707.2046746},\n  editor = {Yan Chen and George Danezis and Vitaly Shmatikov},\n  isbn = {978-1-4503-0948-6},\n  pages = {341--350},\n  publisher = {{ACM}},\n  timestamp = {Tue, 10 Nov 2020 19:56:39 +0100},\n  title = {Modular code-based cryptographic verification},\n  url = {https://doi.org/10.1145/2046707.2046746},\n  year = {2011}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Secure distributed programming with value-dependent types.\n \n \n \n \n\n\n \n Swamy, N.; Chen, J.; Fournet, C.; Strub, P.; Bhargavan, K.; and Yang, J.\n\n\n \n\n\n\n In Chakravarty, M. M. T.; Hu, Z.; and Danvy, O., editor(s), Proceeding of the 16th ACM SIGPLAN international conference on Functional Programming, ICFP 2011, Tokyo, Japan, September 19-21, 2011, pages 266–278, 2011. ACM\n \n\n\n\n
\n\n\n\n \n \n \"SecurePaper\n  \n \n\n \n \n doi\n  \n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n  \n \n 1 download\n \n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{DBLP:conf/icfp/SwamyCFSBY11,\n  author = {Nikhil Swamy and Juan Chen and C{\\'{e}}dric Fournet and\nPierre{-}Yves Strub and Karthikeyan Bhargavan and\nJean Yang},\n  bibsource = {dblp computer science bibliography, https://dblp.org},\n  biburl = {https://dblp.org/rec/conf/icfp/SwamyCFSBY11.bib},\n  booktitle = {Proceeding of the 16th {ACM} {SIGPLAN} international\nconference on Functional Programming, {ICFP} 2011,\nTokyo, Japan, September 19-21, 2011},\n  doi = {10.1145/2034773.2034811},\n  editor = {Manuel M. T. Chakravarty and Zhenjiang Hu and\nOlivier Danvy},\n  isbn = {978-1-4503-0865-6},\n  pages = {266--278},\n  publisher = {{ACM}},\n  timestamp = {Thu, 24 Jun 2021 16:19:30 +0200},\n  title = {Secure distributed programming with value-dependent\ntypes},\n  url = {https://doi.org/10.1145/2034773.2034811},\n  year = {2011}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n CoQMTU: A Higher-Order Type Theory with a Predicative Hierarchy of Universes Parametrized by a Decidable First-Order Theory.\n \n \n \n \n\n\n \n Barras, B.; Jouannaud, J.; Strub, P.; and Wang, Q.\n\n\n \n\n\n\n In Proceedings of the 26th Annual IEEE Symposium on Logic in Computer Science, LICS 2011, June 21-24, 2011, Toronto, Ontario, Canada, pages 143–151, 2011. IEEE Computer Society\n \n\n\n\n
\n\n\n\n \n \n \"CoQMTU:Paper\n  \n \n\n \n \n doi\n  \n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{DBLP:conf/lics/BarrasJSW11,\n  author = {Bruno Barras and Jean{-}Pierre Jouannaud and\nPierre{-}Yves Strub and Qian Wang},\n  bibsource = {dblp computer science bibliography, https://dblp.org},\n  biburl = {https://dblp.org/rec/conf/lics/BarrasJSW11.bib},\n  booktitle = {Proceedings of the 26th Annual {IEEE} Symposium on\nLogic in Computer Science, {LICS} 2011, June 21-24,\n2011, Toronto, Ontario, Canada},\n  doi = {10.1109/LICS.2011.37},\n  isbn = {978-0-7695-4412-0},\n  pages = {143--151},\n  publisher = {{IEEE} Computer Society},\n  timestamp = {Wed, 16 Oct 2019 14:14:54 +0200},\n  title = {CoQMTU: {A} Higher-Order Type Theory with a\nPredicative Hierarchy of Universes Parametrized by a\nDecidable First-Order Theory},\n  url = {https://doi.org/10.1109/LICS.2011.37},\n  year = {2011}\n}\n\n
\n
\n\n\n\n
\n\n\n\n\n\n
\n
\n\n
\n
\n  \n 2010\n \n \n (1)\n \n \n
\n
\n \n \n
\n \n\n \n \n \n \n \n \n Coq Modulo Theory.\n \n \n \n \n\n\n \n Strub, P.\n\n\n \n\n\n\n In Dawar, A.; and Veith, H., editor(s), Computer Science Logic, 24th International Workshop, CSL 2010, 19th Annual Conference of the EACSL, Brno, Czech Republic, August 23-27, 2010. Proceedings, volume 6247, of Lecture Notes in Computer Science, pages 529–543, 2010. Springer\n \n\n\n\n
\n\n\n\n \n \n \"CoqPaper\n  \n \n\n \n \n doi\n  \n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n  \n \n 1 download\n \n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{DBLP:conf/csl/Strub10,\n  author = {Pierre{-}Yves Strub},\n  bibsource = {dblp computer science bibliography, https://dblp.org},\n  biburl = {https://dblp.org/rec/conf/csl/Strub10.bib},\n  booktitle = {Computer Science Logic, 24th International Workshop,\n{CSL} 2010, 19th Annual Conference of the EACSL,\nBrno, Czech Republic, August 23-27, 2010.\nProceedings},\n  doi = {10.1007/978-3-642-15205-4\\_40},\n  editor = {Anuj Dawar and Helmut Veith},\n  isbn = {978-3-642-15204-7},\n  pages = {529--543},\n  publisher = {Springer},\n  series = {Lecture Notes in Computer Science},\n  timestamp = {Tue, 14 May 2019 10:00:42 +0200},\n  title = {Coq Modulo Theory},\n  url = {https://doi.org/10.1007/978-3-642-15205-4\\_40},\n  volume = {6247},\n  year = {2010}\n}\n\n
\n
\n\n\n\n
\n\n\n\n\n\n
\n
\n\n
\n
\n  \n 2008\n \n \n (1)\n \n \n
\n
\n \n \n
\n \n\n \n \n \n \n \n \n From Formal Proofs to Mathematical Proofs: A Safe, Incremental Way for Building in First-order Decision Procedures.\n \n \n \n \n\n\n \n Blanqui, F.; Jouannaud, J.; and Strub, P.\n\n\n \n\n\n\n In Ausiello, G.; Karhumäki, J.; Mauri, G.; and Ong, C. L., editor(s), Fifth IFIP International Conference On Theoretical Computer Science - TCS 2008, IFIP 20th World Computer Congress, TC 1, Foundations of Computer Science, September 7-10, 2008, Milano, Italy, volume 273, of IFIP, pages 349–365, 2008. Springer\n \n\n\n\n
\n\n\n\n \n \n \"FromPaper\n  \n \n\n \n \n doi\n  \n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n  \n \n 1 download\n \n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{DBLP:conf/ifipTCS/BlanquiJS08,\n  author = {Fr{\\'{e}}d{\\'{e}}ric Blanqui and\nJean{-}Pierre Jouannaud and Pierre{-}Yves Strub},\n  bibsource = {dblp computer science bibliography, https://dblp.org},\n  biburl = {https://dblp.org/rec/conf/ifipTCS/BlanquiJS08.bib},\n  booktitle = {Fifth {IFIP} International Conference On Theoretical\nComputer Science - {TCS} 2008, {IFIP} 20th World\nComputer Congress, {TC} 1, Foundations of Computer\nScience, September 7-10, 2008, Milano, Italy},\n  doi = {10.1007/978-0-387-09680-3\\_24},\n  editor = {Giorgio Ausiello and Juhani Karhum{\\"{a}}ki and\nGiancarlo Mauri and C.{-}H. Luke Ong},\n  isbn = {978-0-387-09679-7},\n  pages = {349--365},\n  publisher = {Springer},\n  series = {{IFIP}},\n  timestamp = {Sun, 02 Oct 2022 01:00:00 +0200},\n  title = {From Formal Proofs to Mathematical Proofs: {A} Safe,\nIncremental Way for Building in First-order Decision\nProcedures},\n  url = {https://doi.org/10.1007/978-0-387-09680-3\\_24},\n  volume = {273},\n  year = {2008}\n}\n\n
\n
\n\n\n\n
\n\n\n\n\n\n
\n
\n\n
\n
\n  \n 2007\n \n \n (1)\n \n \n
\n
\n \n \n
\n \n\n \n \n \n \n \n \n Building Decision Procedures in the Calculus of Inductive Constructions.\n \n \n \n \n\n\n \n Blanqui, F.; Jouannaud, J.; and Strub, P.\n\n\n \n\n\n\n In Duparc, J.; and Henzinger, T. A., editor(s), Computer Science Logic, 21st International Workshop, CSL 2007, 16th Annual Conference of the EACSL, Lausanne, Switzerland, September 11-15, 2007, Proceedings, volume 4646, of Lecture Notes in Computer Science, pages 328–342, 2007. Springer\n \n\n\n\n
\n\n\n\n \n \n \"BuildingPaper\n  \n \n\n \n \n doi\n  \n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{DBLP:conf/csl/BlanquiJS07,\n  author = {Fr{\\'{e}}d{\\'{e}}ric Blanqui and\nJean{-}Pierre Jouannaud and Pierre{-}Yves Strub},\n  bibsource = {dblp computer science bibliography, https://dblp.org},\n  biburl = {https://dblp.org/rec/conf/csl/BlanquiJS07.bib},\n  booktitle = {Computer Science Logic, 21st International Workshop,\n{CSL} 2007, 16th Annual Conference of the EACSL,\nLausanne, Switzerland, September 11-15, 2007,\nProceedings},\n  doi = {10.1007/978-3-540-74915-8\\_26},\n  editor = {Jacques Duparc and Thomas A. Henzinger},\n  isbn = {978-3-540-74914-1},\n  pages = {328--342},\n  publisher = {Springer},\n  series = {Lecture Notes in Computer Science},\n  timestamp = {Sun, 02 Oct 2022 01:00:00 +0200},\n  title = {Building Decision Procedures in the Calculus of\nInductive Constructions},\n  url = {https://doi.org/10.1007/978-3-540-74915-8\\_26},\n  volume = {4646},\n  year = {2007}\n}\n\n
\n
\n\n\n\n
\n\n\n\n\n\n
\n
\n\n
\n
\n  \n 2001\n \n \n (1)\n \n \n
\n
\n \n \n
\n \n\n \n \n \n \n \n \n Color image segmentation based on automatic morphological clustering.\n \n \n \n \n\n\n \n Géraud, T.; Strub, P.; and Darbon, J.\n\n\n \n\n\n\n In Proceedings of the 2001 International Conference on Image Processing, ICIP 2001, Thessaloniki, Greece, October 7-10, 2001, pages 70–73, 2001. IEEE\n \n\n\n\n
\n\n\n\n \n \n \"ColorPaper\n  \n \n\n \n \n doi\n  \n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n  \n \n 2 downloads\n \n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{DBLP:conf/icip/GeraudSD01,\n  author = {Thierry G{\\'{e}}raud and Pierre{-}Yves Strub and\nJ{\\'{e}}r{\\^{o}}me Darbon},\n  bibsource = {dblp computer science bibliography, https://dblp.org},\n  biburl = {https://dblp.org/rec/conf/icip/GeraudSD01.bib},\n  booktitle = {Proceedings of the 2001 International Conference on\nImage Processing, {ICIP} 2001, Thessaloniki, Greece,\nOctober 7-10, 2001},\n  doi = {10.1109/ICIP.2001.958053},\n  isbn = {0-7803-6725-1},\n  pages = {70--73},\n  publisher = {{IEEE}},\n  timestamp = {Wed, 16 Oct 2019 14:14:52 +0200},\n  title = {Color image segmentation based on automatic\nmorphological clustering},\n  url = {https://doi.org/10.1109/ICIP.2001.958053},\n  year = {2001}\n}\n\n
\n
\n\n\n\n
\n\n\n\n\n\n
\n
\n\n\n\n\n
\n\n\n \n\n \n \n \n \n\n
\n"}; document.write(bibbase_data.data);