


Остановите войну!
for scientists:
BibTeX records: Pierre-Yves Strub
@article{DBLP:journals/lmcs/AllamigeonKS22, author = {Xavier Allamigeon and Ricardo D. Katz and Pierre{-}Yves Strub}, title = {Formalizing the Face Lattice of Polyhedra}, journal = {Log. Methods Comput. Sci.}, volume = {18}, number = {2}, year = {2022}, url = {https://doi.org/10.46298/lmcs-18(2:10)2022}, doi = {10.46298/lmcs-18(2:10)2022}, timestamp = {Thu, 09 Jun 2022 01:00:00 +0200}, biburl = {https://dblp.org/rec/journals/lmcs/AllamigeonKS22.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:conf/cpp/DonatoSW22, author = {Pablo Donato and Pierre{-}Yves Strub and Benjamin Werner}, editor = {Andrei Popescu and Steve Zdancewic}, title = {A drag-and-drop proof tactic}, booktitle = {{CPP} '22: 11th {ACM} {SIGPLAN} International Conference on Certified Programs and Proofs, Philadelphia, PA, USA, January 17 - 18, 2022}, pages = {197--209}, publisher = {{ACM}}, year = {2022}, url = {https://doi.org/10.1145/3497775.3503692}, doi = {10.1145/3497775.3503692}, timestamp = {Mon, 17 Jan 2022 09:44:17 +0100}, biburl = {https://dblp.org/rec/conf/cpp/DonatoSW22.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@article{DBLP:journals/corr/abs-2207-11350, author = {Li Zhou and Gilles Barthe and Pierre{-}Yves Strub and Junyi Liu and Mingsheng Ying}, title = {CoqQ: Foundational Verification of Quantum Programs}, journal = {CoRR}, volume = {abs/2207.11350}, year = {2022}, url = {https://doi.org/10.48550/arXiv.2207.11350}, doi = {10.48550/arXiv.2207.11350}, eprinttype = {arXiv}, eprint = {2207.11350}, timestamp = {Mon, 01 Aug 2022 01:00:00 +0200}, biburl = {https://dblp.org/rec/journals/corr/abs-2207-11350.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@article{DBLP:journals/iacr/HulsingMS22, author = {Andreas H{\"{u}}lsing and Matthias Meijers and Pierre{-}Yves Strub}, title = {Formal Verification of Saber's Public-Key Encryption Scheme in EasyCrypt}, journal = {{IACR} Cryptol. ePrint Arch.}, pages = {351}, year = {2022}, url = {https://eprint.iacr.org/2022/351}, timestamp = {Thu, 21 Apr 2022 01:00:00 +0200}, biburl = {https://dblp.org/rec/journals/iacr/HulsingMS22.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:conf/ccs/BarbosaBGKS21, author = {Manuel Barbosa and Gilles Barthe and Benjamin Gr{\'{e}}goire and Adrien Koutsos and Pierre{-}Yves Strub}, editor = {Yongdae Kim and Jong Kim and Giovanni Vigna and Elaine Shi}, title = {Mechanized Proofs of Adversarial Complexity and Application to Universal Composability}, booktitle = {{CCS} '21: 2021 {ACM} {SIGSAC} Conference on Computer and Communications Security, Virtual Event, Republic of Korea, November 15 - 19, 2021}, pages = {2541--2563}, publisher = {{ACM}}, year = {2021}, url = {https://doi.org/10.1145/3460120.3484548}, doi = {10.1145/3460120.3484548}, timestamp = {Thu, 23 Jun 2022 01:00:00 +0200}, biburl = {https://dblp.org/rec/conf/ccs/BarbosaBGKS21.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:conf/ccs/BarbosaBFGHKSWZ21, author = {Manuel Barbosa and Gilles Barthe and Xiong Fan and Benjamin Gr{\'{e}}goire and Shih{-}Han Hung and Jonathan Katz and Pierre{-}Yves Strub and Xiaodi Wu and Li Zhou}, editor = {Yongdae Kim and Jong Kim and Giovanni Vigna and Elaine Shi}, title = {EasyPQC: Verifying Post-Quantum Cryptography}, booktitle = {{CCS} '21: 2021 {ACM} {SIGSAC} Conference on Computer and Communications Security, Virtual Event, Republic of Korea, November 15 - 19, 2021}, pages = {2564--2586}, publisher = {{ACM}}, year = {2021}, url = {https://doi.org/10.1145/3460120.3484567}, doi = {10.1145/3460120.3484567}, timestamp = {Mon, 03 Jan 2022 00:00:00 +0100}, biburl = {https://dblp.org/rec/conf/ccs/BarbosaBFGHKSWZ21.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:conf/itp/BernardCMS21, author = {Sophie Bernard and Cyril Cohen and Assia Mahboubi and Pierre{-}Yves Strub}, editor = {Liron Cohen and Cezary Kaliszyk}, title = {Unsolvability of the Quintic Formalized in Dependent Type Theory}, booktitle = {12th International Conference on Interactive Theorem Proving, {ITP} 2021, June 29 to July 1, 2021, Rome, Italy (Virtual Conference)}, series = {LIPIcs}, volume = {193}, pages = {8:1--8:18}, publisher = {Schloss Dagstuhl - Leibniz-Zentrum f{\"{u}}r Informatik}, year = {2021}, url = {https://doi.org/10.4230/LIPIcs.ITP.2021.8}, doi = {10.4230/LIPIcs.ITP.2021.8}, timestamp = {Mon, 21 Jun 2021 14:45:49 +0200}, biburl = {https://dblp.org/rec/conf/itp/BernardCMS21.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@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}, url = {https://arxiv.org/abs/2104.15021}, eprinttype = {arXiv}, eprint = {2104.15021}, timestamp = {Tue, 04 May 2021 01:00:00 +0200}, biburl = {https://dblp.org/rec/journals/corr/abs-2104-15021.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@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}, url = {https://eprint.iacr.org/2021/156}, timestamp = {Tue, 02 Mar 2021 00:00:00 +0100}, biburl = {https://dblp.org/rec/journals/iacr/BarbosaBGKS21.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@article{DBLP:journals/iacr/BarbosaBFGHKSWZ21, author = {Manuel Barbosa and Gilles Barthe and Xiong Fan and Benjamin Gr{\'{e}}goire and Shih{-}Han Hung and Jonathan Katz and Pierre{-}Yves Strub and Xiaodi Wu and Li Zhou}, title = {EasyPQC: Verifying Post-Quantum Cryptography}, journal = {{IACR} Cryptol. ePrint Arch.}, pages = {1253}, year = {2021}, url = {https://eprint.iacr.org/2021/1253}, timestamp = {Mon, 25 Oct 2021 01:00:00 +0200}, biburl = {https://dblp.org/rec/journals/iacr/BarbosaBFGHKSWZ21.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@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}, url = {https://doi.org/10.1007/s13389-018-00202-2}, doi = {10.1007/s13389-018-00202-2}, timestamp = {Thu, 14 Oct 2021 01:00:00 +0200}, biburl = {https://dblp.org/rec/journals/jce/BartheBDFGSS20.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:conf/cade/AllamigeonKS20, author = {Xavier Allamigeon and Ricardo D. Katz and Pierre{-}Yves Strub}, editor = {Nicolas Peltier and Viorica Sofronie{-}Stokkermans}, title = {Formalizing the Face Lattice of Polyhedra}, booktitle = {Automated Reasoning - 10th International Joint Conference, {IJCAR} 2020, Paris, France, July 1-4, 2020, Proceedings, Part {II}}, series = {Lecture Notes in Computer Science}, volume = {12167}, pages = {185--203}, publisher = {Springer}, year = {2020}, url = {https://doi.org/10.1007/978-3-030-51054-1\_11}, doi = {10.1007/978-3-030-51054-1\_11}, timestamp = {Fri, 03 Jul 2020 13:56:19 +0200}, biburl = {https://dblp.org/rec/conf/cade/AllamigeonKS20.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@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 = {2020 {IEEE} Symposium on Security and Privacy, {SP} 2020, San Francisco, CA, USA, May 18-21, 2020}, pages = {965--982}, publisher = {{IEEE}}, year = {2020}, url = {https://doi.org/10.1109/SP40000.2020.00028}, doi = {10.1109/SP40000.2020.00028}, timestamp = {Tue, 29 Dec 2020 00:00:00 +0100}, biburl = {https://dblp.org/rec/conf/sp/AlmeidaBBGKL0S20.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@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}, url = {https://doi.org/10.1017/S0956796819000145}, doi = {10.1017/S0956796819000145}, timestamp = {Tue, 16 Jun 2020 01:00:00 +0200}, biburl = {https://dblp.org/rec/journals/jfp/AguirreBGGS19.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@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}, url = {https://doi.org/10.23638/LMCS-15(4:18)2019}, doi = {10.23638/LMCS-15(4:18)2019}, timestamp = {Thu, 14 Oct 2021 01:00:00 +0200}, biburl = {https://dblp.org/rec/journals/lmcs/BartheEHSS19.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@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}, editor = {Lorenzo Cavallaro and Johannes Kinder and XiaoFeng Wang and Jonathan Katz}, title = {A Machine-Checked Proof of Security for {AWS} Key Management Service}, booktitle = {Proceedings of the 2019 {ACM} {SIGSAC} Conference on Computer and Communications Security, {CCS} 2019, London, UK, November 11-15, 2019}, pages = {63--78}, publisher = {{ACM}}, year = {2019}, url = {https://doi.org/10.1145/3319535.3354228}, doi = {10.1145/3319535.3354228}, timestamp = {Fri, 29 Apr 2022 01:00:00 +0200}, biburl = {https://dblp.org/rec/conf/ccs/AlmeidaBBCCGPPS19.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@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}, editor = {Lorenzo Cavallaro and Johannes Kinder and XiaoFeng Wang and Jonathan Katz}, title = {Machine-Checked Proofs for Cryptographic Standards: Indifferentiability of Sponge and Secure High-Assurance Implementations of {SHA-3}}, booktitle = {Proceedings of the 2019 {ACM} {SIGSAC} Conference on Computer and Communications Security, {CCS} 2019, London, UK, November 11-15, 2019}, pages = {1607--1622}, publisher = {{ACM}}, year = {2019}, url = {https://doi.org/10.1145/3319535.3363211}, doi = {10.1145/3319535.3363211}, timestamp = {Mon, 29 Mar 2021 01:00:00 +0200}, biburl = {https://dblp.org/rec/conf/ccs/AlmeidaBBBDGL0S19.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@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 = {32nd {IEEE} Computer Security Foundations Symposium, {CSF} 2019, Hoboken, NJ, USA, June 25-28, 2019}, pages = {136--151}, publisher = {{IEEE}}, year = {2019}, url = {https://doi.org/10.1109/CSF.2019.00017}, doi = {10.1109/CSF.2019.00017}, timestamp = {Wed, 16 Oct 2019 14:14:49 +0200}, biburl = {https://dblp.org/rec/conf/csfw/BartheGJKS19.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@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}, url = {http://arxiv.org/abs/1904.04606}, eprinttype = {arXiv}, eprint = {1904.04606}, timestamp = {Sat, 23 Jan 2021 00:00:00 +0100}, biburl = {https://dblp.org/rec/journals/corr/abs-1904-04606.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@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}, url = {https://eprint.iacr.org/2019/1042}, timestamp = {Fri, 29 Apr 2022 01:00:00 +0200}, biburl = {https://dblp.org/rec/journals/iacr/AlmeidaBBCCGPPS19.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@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}, url = {https://eprint.iacr.org/2019/1155}, timestamp = {Mon, 29 Mar 2021 01:00:00 +0200}, biburl = {https://dblp.org/rec/journals/iacr/AlmeidaBBBDGLOS19.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@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}, url = {https://doi.org/10.1145/3158145}, doi = {10.1145/3158145}, timestamp = {Wed, 17 Feb 2021 00:00:00 +0100}, biburl = {https://dblp.org/rec/journals/pacmpl/BartheEGHS18.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@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 = {31st {IEEE} Computer Security Foundations Symposium, {CSF} 2018, Oxford, United Kingdom, July 9-12, 2018}, pages = {119--131}, publisher = {{IEEE} Computer Society}, year = {2018}, url = {https://doi.org/10.1109/CSF.2018.00016}, doi = {10.1109/CSF.2018.00016}, timestamp = {Thu, 14 Oct 2021 01:00:00 +0200}, biburl = {https://dblp.org/rec/conf/csfw/HaaghKOSS18.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@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}, editor = {Amal Ahmed}, title = {An Assertion-Based Program Logic for Probabilistic Programs}, booktitle = {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}, series = {Lecture Notes in Computer Science}, volume = {10801}, pages = {117--144}, publisher = {Springer}, year = {2018}, url = {https://doi.org/10.1007/978-3-319-89884-1\_5}, doi = {10.1007/978-3-319-89884-1\_5}, timestamp = {Tue, 05 Jul 2022 08:30:25 +0200}, biburl = {https://dblp.org/rec/conf/esop/BartheEGGHS18.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:conf/secsr/BhargavanKS18, author = {Karthikeyan Bhargavan and Franziskus Kiefer and Pierre{-}Yves Strub}, editor = {Cas Cremers and Anja Lehmann}, title = {hacspec: Towards Verifiable Crypto Standards}, booktitle = {Security Standardisation Research - 4th International Conference, {SSR} 2018, Darmstadt, Germany, November 26-27, 2018, Proceedings}, series = {Lecture Notes in Computer Science}, volume = {11322}, pages = {1--20}, publisher = {Springer}, year = {2018}, url = {https://doi.org/10.1007/978-3-030-04762-7\_1}, doi = {10.1007/978-3-030-04762-7\_1}, timestamp = {Tue, 14 May 2019 10:00:40 +0200}, biburl = {https://dblp.org/rec/conf/secsr/BhargavanKS18.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@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}, url = {http://arxiv.org/abs/1803.05535}, eprinttype = {arXiv}, eprint = {1803.05535}, timestamp = {Mon, 13 Aug 2018 01:00:00 +0200}, biburl = {https://dblp.org/rec/journals/corr/abs-1803-05535.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@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}, url = {http://arxiv.org/abs/1806.07197}, eprinttype = {arXiv}, eprint = {1806.07197}, timestamp = {Sat, 23 Jan 2021 00:00:00 +0100}, biburl = {https://dblp.org/rec/journals/corr/abs-1806-07197.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@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}, url = {https://eprint.iacr.org/2018/502}, timestamp = {Mon, 11 May 2020 01:00:00 +0200}, biburl = {https://dblp.org/rec/journals/iacr/HaaghKOSS18.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@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}, url = {https://eprint.iacr.org/2018/505}, timestamp = {Thu, 21 Jan 2021 00:00:00 +0100}, biburl = {https://dblp.org/rec/journals/iacr/BartheBDFGSS18.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@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}, url = {https://doi.org/10.1145/3023357}, doi = {10.1145/3023357}, timestamp = {Tue, 06 Nov 2018 00:00:00 +0100}, biburl = {https://dblp.org/rec/journals/cacm/BeurdoucheBDFKP17.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@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}, url = {https://doi.org/10.1145/3110265}, doi = {10.1145/3110265}, timestamp = {Wed, 17 Feb 2021 00:00:00 +0100}, biburl = {https://dblp.org/rec/journals/pacmpl/AguirreBG0S17.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@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}, editor = {Bhavani Thuraisingham and David Evans and Tal Malkin and Dongyan Xu}, title = {Jasmin: High-Assurance and High-Speed Cryptography}, booktitle = {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}, publisher = {{ACM}}, year = {2017}, url = {https://doi.org/10.1145/3133956.3134078}, doi = {10.1145/3133956.3134078}, timestamp = {Wed, 29 Jun 2022 15:37:41 +0200}, biburl = {https://dblp.org/rec/conf/ccs/AlmeidaBBBGLOPS17.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@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}, editor = {Jean{-}S{\'{e}}bastien Coron and Jesper Buus Nielsen}, title = {Parallel Implementations of Masking Schemes and the Bounded Moment Leakage Model}, booktitle = {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}}, series = {Lecture Notes in Computer Science}, volume = {10210}, pages = {535--566}, year = {2017}, url = {https://doi.org/10.1007/978-3-319-56620-7\_19}, doi = {10.1007/978-3-319-56620-7\_19}, timestamp = {Thu, 14 Oct 2021 01:00:00 +0200}, biburl = {https://dblp.org/rec/conf/eurocrypt/BartheDFGSS17.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:conf/icalp/BartheEHSS17, author = {Gilles Barthe and Thomas Espitau and Justin Hsu and Tetsuya Sato and Pierre{-}Yves Strub}, editor = {Ioannis Chatzigiannakis and Piotr Indyk and Fabian Kuhn and Anca Muscholl}, title = {*-Liftings for Differential Privacy}, booktitle = {44th International Colloquium on Automata, Languages, and Programming, {ICALP} 2017, July 10-14, 2017, Warsaw, Poland}, series = {LIPIcs}, volume = {80}, pages = {102:1--102:12}, publisher = {Schloss Dagstuhl - Leibniz-Zentrum f{\"{u}}r Informatik}, year = {2017}, url = {https://doi.org/10.4230/LIPIcs.ICALP.2017.102}, doi = {10.4230/LIPIcs.ICALP.2017.102}, timestamp = {Mon, 11 Oct 2021 01:00:00 +0200}, biburl = {https://dblp.org/rec/conf/icalp/BartheEHSS17.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:conf/lpar/BartheEGHS17, author = {Gilles Barthe and Thomas Espitau and Benjamin Gr{\'{e}}goire and Justin Hsu and Pierre{-}Yves Strub}, editor = {Thomas Eiter and David Sands}, title = {Proving uniformity and independence by self-composition and coupling}, booktitle = {LPAR-21, 21st International Conference on Logic for Programming, Artificial Intelligence and Reasoning, Maun, Botswana, May 7-12, 2017}, series = {EPiC Series in Computing}, volume = {46}, pages = {385--403}, publisher = {EasyChair}, year = {2017}, url = {https://doi.org/10.29007/vz48}, doi = {10.29007/vz48}, timestamp = {Thu, 14 Oct 2021 01:00:00 +0200}, biburl = {https://dblp.org/rec/conf/lpar/BartheEGHS17.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:conf/lpar/JouannaudS17, author = {Jean{-}Pierre Jouannaud and Pierre{-}Yves Strub}, editor = {Thomas Eiter and David Sands}, title = {Coq without Type Casts: {A} Complete Proof of Coq Modulo Theory}, booktitle = {LPAR-21, 21st International Conference on Logic for Programming, Artificial Intelligence and Reasoning, Maun, Botswana, May 7-12, 2017}, series = {EPiC Series in Computing}, volume = {46}, pages = {474--489}, publisher = {EasyChair}, year = {2017}, url = {https://doi.org/10.29007/bjpg}, doi = {10.29007/bjpg}, timestamp = {Sun, 15 Aug 2021 01:00:00 +0200}, biburl = {https://dblp.org/rec/conf/lpar/JouannaudS17.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:conf/popl/BartheGHS17, author = {Gilles Barthe and Benjamin Gr{\'{e}}goire and Justin Hsu and Pierre{-}Yves Strub}, editor = {Giuseppe Castagna and Andrew D. Gordon}, title = {Coupling proofs are probabilistic product programs}, booktitle = {Proceedings of the 44th {ACM} {SIGPLAN} Symposium on Principles of Programming Languages, {POPL} 2017, Paris, France, January 18-20, 2017}, pages = {161--174}, publisher = {{ACM}}, year = {2017}, url = {https://doi.org/10.1145/3009837.3009896}, doi = {10.1145/3009837.3009896}, timestamp = {Mon, 14 Feb 2022 09:20:26 +0100}, biburl = {https://dblp.org/rec/conf/popl/BartheGHS17.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@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 = {2017 {IEEE} Symposium on Security and Privacy, {SP} 2017, San Jose, CA, USA, May 22-26, 2017}, pages = {993--1008}, publisher = {{IEEE} Computer Society}, year = {2017}, url = {https://doi.org/10.1109/SP.2017.28}, doi = {10.1109/SP.2017.28}, timestamp = {Sat, 19 Oct 2019 01:00:00 +0200}, biburl = {https://dblp.org/rec/conf/sp/CortierDDSSW17.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@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}, url = {http://arxiv.org/abs/1701.06477}, eprinttype = {arXiv}, eprint = {1701.06477}, timestamp = {Mon, 13 Aug 2018 01:00:00 +0200}, biburl = {https://dblp.org/rec/journals/corr/BartheEGHS17.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@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}, url = {http://arxiv.org/abs/1703.05042}, eprinttype = {arXiv}, eprint = {1703.05042}, timestamp = {Mon, 13 Aug 2018 01:00:00 +0200}, biburl = {https://dblp.org/rec/journals/corr/AguirreBG0S17.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@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}, url = {http://arxiv.org/abs/1705.00133}, eprinttype = {arXiv}, eprint = {1705.00133}, timestamp = {Mon, 11 Oct 2021 01:00:00 +0200}, biburl = {https://dblp.org/rec/journals/corr/BartheEHSS17.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@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}, url = {http://arxiv.org/abs/1708.02537}, eprinttype = {arXiv}, eprint = {1708.02537}, timestamp = {Mon, 13 Aug 2018 01:00:00 +0200}, biburl = {https://dblp.org/rec/journals/corr/abs-1708-02537.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@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}, editor = {Edgar R. Weippl and Stefan Katzenbeisser and Christopher Kruegel and Andrew C. Myers and Shai Halevi}, title = {Advanced Probabilistic Couplings for Differential Privacy}, booktitle = {Proceedings of the 2016 {ACM} {SIGSAC} Conference on Computer and Communications Security, Vienna, Austria, October 24-28, 2016}, pages = {55--67}, publisher = {{ACM}}, year = {2016}, url = {https://doi.org/10.1145/2976749.2978391}, doi = {10.1145/2976749.2978391}, timestamp = {Tue, 10 Nov 2020 20:00:49 +0100}, biburl = {https://dblp.org/rec/conf/ccs/BartheFGGHS16.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@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}, editor = {Edgar R. Weippl and Stefan Katzenbeisser and Christopher Kruegel and Andrew C. Myers and Shai Halevi}, title = {Differentially Private Bayesian Programming}, booktitle = {Proceedings of the 2016 {ACM} {SIGSAC} Conference on Computer and Communications Security, Vienna, Austria, October 24-28, 2016}, pages = {68--79}, publisher = {{ACM}}, year = {2016}, url = {https://doi.org/10.1145/2976749.2978371}, doi = {10.1145/2976749.2978371}, timestamp = {Mon, 14 Feb 2022 00:00:00 +0100}, biburl = {https://dblp.org/rec/conf/ccs/BartheFGAGHS16.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@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}, editor = {Edgar R. Weippl and Stefan Katzenbeisser and Christopher Kruegel and Andrew C. Myers and Shai Halevi}, title = {Strong Non-Interference and Type-Directed Higher-Order Masking}, booktitle = {Proceedings of the 2016 {ACM} {SIGSAC} Conference on Computer and Communications Security, Vienna, Austria, October 24-28, 2016}, pages = {116--129}, publisher = {{ACM}}, year = {2016}, url = {https://doi.org/10.1145/2976749.2978427}, doi = {10.1145/2976749.2978427}, timestamp = {Tue, 10 Nov 2020 00:00:00 +0100}, biburl = {https://dblp.org/rec/conf/ccs/BartheBDFGSZ16.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:conf/cpp/BernardBRS16, author = {Sophie Bernard and Yves Bertot and Laurence Rideau and Pierre{-}Yves Strub}, editor = {Jeremy Avigad and Adam Chlipala}, title = {Formal proofs of transcendence for e and pi as an application of multivariate and symmetric polynomials}, booktitle = {Proceedings of the 5th {ACM} {SIGPLAN} Conference on Certified Programs and Proofs, Saint Petersburg, FL, USA, January 20-22, 2016}, pages = {76--87}, publisher = {{ACM}}, year = {2016}, url = {https://doi.org/10.1145/2854065.2854072}, doi = {10.1145/2854065.2854072}, timestamp = {Tue, 06 Nov 2018 00:00:00 +0100}, biburl = {https://dblp.org/rec/conf/cpp/BernardBRS16.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:conf/icalp/BartheGGHS16, author = {Gilles Barthe and Marco Gaboardi and Benjamin Gr{\'{e}}goire and Justin Hsu and Pierre{-}Yves Strub}, editor = {Ioannis Chatzigiannakis and Michael Mitzenmacher and Yuval Rabani and Davide Sangiorgi}, title = {A Program Logic for Union Bounds}, booktitle = {43rd International Colloquium on Automata, Languages, and Programming, {ICALP} 2016, July 11-15, 2016, Rome, Italy}, series = {LIPIcs}, volume = {55}, pages = {107:1--107:15}, publisher = {Schloss Dagstuhl - Leibniz-Zentrum f{\"{u}}r Informatik}, year = {2016}, url = {https://doi.org/10.4230/LIPIcs.ICALP.2016.107}, doi = {10.4230/LIPIcs.ICALP.2016.107}, timestamp = {Mon, 15 Jun 2020 01:00:00 +0200}, biburl = {https://dblp.org/rec/conf/icalp/BartheGGHS16.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:conf/lics/BartheGGHS16, author = {Gilles Barthe and Marco Gaboardi and Benjamin Gr{\'{e}}goire and Justin Hsu and Pierre{-}Yves Strub}, editor = {Martin Grohe and Eric Koskinen and Natarajan Shankar}, title = {Proving Differential Privacy via Probabilistic Couplings}, booktitle = {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}, publisher = {{ACM}}, year = {2016}, url = {https://doi.org/10.1145/2933575.2934554}, doi = {10.1145/2933575.2934554}, timestamp = {Wed, 11 Aug 2021 01:00:00 +0200}, biburl = {https://dblp.org/rec/conf/lics/BartheGGHS16.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@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}, editor = {Rastislav Bod{\'{\i}}k and Rupak Majumdar}, title = {Dependent types and multi-monadic effects in {F}}, booktitle = {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}, publisher = {{ACM}}, year = {2016}, url = {https://doi.org/10.1145/2837614.2837655}, doi = {10.1145/2837614.2837655}, timestamp = {Wed, 23 Jun 2021 15:34:31 +0200}, biburl = {https://dblp.org/rec/conf/popl/SwamyHKRDFBFSKZ16.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@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}, editor = {Yang Cai and Adrian Vetta}, title = {Computer-Aided Verification for Mechanism Design}, booktitle = {Web and Internet Economics - 12th International Conference, {WINE} 2016, Montreal, Canada, December 11-14, 2016, Proceedings}, series = {Lecture Notes in Computer Science}, volume = {10123}, pages = {279--293}, publisher = {Springer}, year = {2016}, url = {https://doi.org/10.1007/978-3-662-54110-4\_20}, doi = {10.1007/978-3-662-54110-4\_20}, timestamp = {Sat, 09 Apr 2022 12:47:11 +0200}, biburl = {https://dblp.org/rec/conf/wine/BartheGAHRS16.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@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}, url = {http://arxiv.org/abs/1601.05047}, eprinttype = {arXiv}, eprint = {1601.05047}, timestamp = {Mon, 13 Aug 2018 01:00:00 +0200}, biburl = {https://dblp.org/rec/journals/corr/BartheGGHS16.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@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}, url = {http://arxiv.org/abs/1602.05681}, eprinttype = {arXiv}, eprint = {1602.05681}, timestamp = {Mon, 13 Aug 2018 01:00:00 +0200}, biburl = {https://dblp.org/rec/journals/corr/BartheGGHS16a.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@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}, url = {http://arxiv.org/abs/1605.00283}, eprinttype = {arXiv}, eprint = {1605.00283}, timestamp = {Mon, 14 Feb 2022 00:00:00 +0100}, biburl = {https://dblp.org/rec/journals/corr/BartheFGAGHS16.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@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}, url = {http://arxiv.org/abs/1606.07143}, eprinttype = {arXiv}, eprint = {1606.07143}, timestamp = {Mon, 13 Aug 2018 01:00:00 +0200}, biburl = {https://dblp.org/rec/journals/corr/BartheGGHS16b.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@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}, url = {http://arxiv.org/abs/1607.03455}, eprinttype = {arXiv}, eprint = {1607.03455}, timestamp = {Mon, 13 Aug 2018 01:00:00 +0200}, biburl = {https://dblp.org/rec/journals/corr/BartheGHS16.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@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}, url = {http://eprint.iacr.org/2016/912}, timestamp = {Mon, 11 May 2020 01:00:00 +0200}, biburl = {https://dblp.org/rec/journals/iacr/BartheDFGSS16.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@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}, editor = {Elisabeth Oswald and Marc Fischlin}, title = {Verified Proofs of Higher-Order Masking}, booktitle = {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}}, series = {Lecture Notes in Computer Science}, volume = {9056}, pages = {457--485}, publisher = {Springer}, year = {2015}, url = {https://doi.org/10.1007/978-3-662-46800-5\_18}, doi = {10.1007/978-3-662-46800-5\_18}, timestamp = {Thu, 14 Oct 2021 09:58:16 +0200}, biburl = {https://dblp.org/rec/conf/eurocrypt/BartheBDFGS15.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@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}, editor = {Martin Davis and Ansgar Fehnker and Annabelle McIver and Andrei Voronkov}, title = {Relational Reasoning via Probabilistic Coupling}, booktitle = {Logic for Programming, Artificial Intelligence, and Reasoning - 20th International Conference, {LPAR-20} 2015, Suva, Fiji, November 24-28, 2015, Proceedings}, series = {Lecture Notes in Computer Science}, volume = {9450}, pages = {387--401}, publisher = {Springer}, year = {2015}, url = {https://doi.org/10.1007/978-3-662-48899-7\_27}, doi = {10.1007/978-3-662-48899-7\_27}, timestamp = {Mon, 03 Jan 2022 22:31:30 +0100}, biburl = {https://dblp.org/rec/conf/lpar/BartheEGHSS15.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@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}, editor = {Sriram K. Rajamani and David Walker}, title = {Higher-Order Approximate Relational Refinement Types for Mechanism Design and Differential Privacy}, booktitle = {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}, publisher = {{ACM}}, year = {2015}, url = {https://doi.org/10.1145/2676726.2677000}, doi = {10.1145/2676726.2677000}, timestamp = {Wed, 23 Jun 2021 17:06:05 +0200}, biburl = {https://dblp.org/rec/conf/popl/BartheGAHRS15.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@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 = {2015 {IEEE} Symposium on Security and Privacy, {SP} 2015, San Jose, CA, USA, May 17-21, 2015}, pages = {535--552}, publisher = {{IEEE} Computer Society}, year = {2015}, url = {https://doi.org/10.1109/SP.2015.39}, doi = {10.1109/SP.2015.39}, timestamp = {Wed, 16 Oct 2019 14:14:51 +0200}, biburl = {https://dblp.org/rec/conf/sp/BeurdoucheBDFKP15.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@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}, url = {http://arxiv.org/abs/1502.04052}, eprinttype = {arXiv}, eprint = {1502.04052}, timestamp = {Tue, 08 Oct 2019 01:00:00 +0200}, biburl = {https://dblp.org/rec/journals/corr/BartheGAHRS15.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@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}, url = {http://arxiv.org/abs/1509.03476}, eprinttype = {arXiv}, eprint = {1509.03476}, timestamp = {Mon, 13 Aug 2018 01:00:00 +0200}, biburl = {https://dblp.org/rec/journals/corr/BartheEGHSS15.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@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}, url = {http://arxiv.org/abs/1512.02791}, eprinttype = {arXiv}, eprint = {1512.02791}, timestamp = {Mon, 13 Aug 2018 01:00:00 +0200}, biburl = {https://dblp.org/rec/journals/corr/BernardBRS15.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@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}, url = {http://eprint.iacr.org/2015/060}, timestamp = {Mon, 11 May 2020 01:00:00 +0200}, biburl = {https://dblp.org/rec/journals/iacr/BartheBDFGS15.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@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}, editor = {Juan A. Garay and Rosario Gennaro}, title = {Proving the {TLS} Handshake Secure (As It Is)}, booktitle = {Advances in Cryptology - {CRYPTO} 2014 - 34th Annual Cryptology Conference, Santa Barbara, CA, USA, August 17-21, 2014, Proceedings, Part {II}}, series = {Lecture Notes in Computer Science}, volume = {8617}, pages = {235--255}, publisher = {Springer}, year = {2014}, url = {https://doi.org/10.1007/978-3-662-44381-1\_14}, doi = {10.1007/978-3-662-44381-1\_14}, timestamp = {Sun, 25 Oct 2020 01:00:00 +0200}, biburl = {https://dblp.org/rec/conf/crypto/BhargavanFKPSB14.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@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 = {{IEEE} 27th Computer Security Foundations Symposium, {CSF} 2014, Vienna, Austria, 19-22 July, 2014}, pages = {153--165}, publisher = {{IEEE} Computer Society}, year = {2014}, url = {https://doi.org/10.1109/CSF.2014.19}, doi = {10.1109/CSF.2014.19}, timestamp = {Sat, 19 Oct 2019 01:00:00 +0200}, biburl = {https://dblp.org/rec/conf/csfw/AkinyeleBGSS14.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@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 = {{IEEE} 27th Computer Security Foundations Symposium, {CSF} 2014, Vienna, Austria, 19-22 July, 2014}, pages = {411--424}, publisher = {{IEEE} Computer Society}, year = {2014}, url = {https://doi.org/10.1109/CSF.2014.36}, doi = {10.1109/CSF.2014.36}, timestamp = {Sat, 19 Oct 2019 01:00:00 +0200}, biburl = {https://dblp.org/rec/conf/csfw/BartheGAHKS14.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:conf/itp/BartziaS14, author = {Evmorfia{-}Iro Bartzia and Pierre{-}Yves Strub}, editor = {Gerwin Klein and Ruben Gamboa}, title = {A Formal Library for Elliptic Curves in the Coq Proof Assistant}, booktitle = {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}, series = {Lecture Notes in Computer Science}, volume = {8558}, pages = {77--92}, publisher = {Springer}, year = {2014}, url = {https://doi.org/10.1007/978-3-319-08970-6\_6}, doi = {10.1007/978-3-319-08970-6\_6}, timestamp = {Tue, 14 May 2019 10:00:37 +0200}, biburl = {https://dblp.org/rec/conf/itp/BartziaS14.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@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}, editor = {Suresh Jagannathan and Peter Sewell}, title = {Probabilistic relational verification for cryptographic implementations}, booktitle = {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}, publisher = {{ACM}}, year = {2014}, url = {https://doi.org/10.1145/2535838.2535847}, doi = {10.1145/2535838.2535847}, timestamp = {Thu, 24 Jun 2021 16:19:31 +0200}, biburl = {https://dblp.org/rec/conf/popl/BartheFGSSB14.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@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}, editor = {Suresh Jagannathan and Peter Sewell}, title = {Gradual typing embedded securely in JavaScript}, booktitle = {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}, publisher = {{ACM}}, year = {2014}, url = {https://doi.org/10.1145/2535838.2535889}, doi = {10.1145/2535838.2535889}, timestamp = {Thu, 24 Jun 2021 01:00:00 +0200}, biburl = {https://dblp.org/rec/conf/popl/SwamyFRBCSB14.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@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 = {2014 {IEEE} Symposium on Security and Privacy, {SP} 2014, Berkeley, CA, USA, May 18-21, 2014}, pages = {98--113}, publisher = {{IEEE} Computer Society}, year = {2014}, url = {https://doi.org/10.1109/SP.2014.14}, doi = {10.1109/SP.2014.14}, timestamp = {Wed, 16 Oct 2019 14:14:51 +0200}, biburl = {https://dblp.org/rec/conf/sp/BhargavanDFPS14.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@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}, url = {http://arxiv.org/abs/1407.2988}, eprinttype = {arXiv}, eprint = {1407.2988}, timestamp = {Mon, 13 Aug 2018 01:00:00 +0200}, biburl = {https://dblp.org/rec/journals/corr/BartheGAHKS14.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@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}, url = {http://arxiv.org/abs/1407.6845}, eprinttype = {arXiv}, eprint = {1407.6845}, timestamp = {Tue, 08 Oct 2019 01:00:00 +0200}, biburl = {https://dblp.org/rec/journals/corr/BartheGAHRS14.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@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}, url = {http://eprint.iacr.org/2014/182}, timestamp = {Mon, 11 May 2020 01:00:00 +0200}, biburl = {https://dblp.org/rec/journals/iacr/BhargavanFKPSB14.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@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}, url = {http://eprint.iacr.org/2014/456}, timestamp = {Mon, 11 May 2020 01:00:00 +0200}, biburl = {https://dblp.org/rec/journals/iacr/AlmeidaBBDDGS14.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@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}, url = {https://doi.org/10.1017/S0956796813000142}, doi = {10.1017/S0956796813000142}, timestamp = {Thu, 03 Sep 2020 01:00:00 +0200}, biburl = {https://dblp.org/rec/journals/jfp/SwamyCFSBY13.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@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}, editor = {Alessandro Aldini and Javier L{\'{o}}pez and Fabio Martinelli}, title = {EasyCrypt: {A} Tutorial}, booktitle = {Foundations of Security Analysis and Design {VII} - {FOSAD} 2012/2013 Tutorial Lectures}, series = {Lecture Notes in Computer Science}, volume = {8604}, pages = {146--166}, publisher = {Springer}, year = {2013}, url = {https://doi.org/10.1007/978-3-319-10082-1\_6}, doi = {10.1007/978-3-319-10082-1\_6}, timestamp = {Thu, 29 Aug 2019 08:10:01 +0200}, biburl = {https://dblp.org/rec/conf/fosad/BartheDGKSS13.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@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}, editor = {Roberto Giacobazzi and Radhia Cousot}, title = {Fully abstract compilation to JavaScript}, booktitle = {The 40th Annual {ACM} {SIGPLAN-SIGACT} Symposium on Principles of Programming Languages, {POPL} '13, Rome, Italy - January 23 - 25, 2013}, pages = {371--384}, publisher = {{ACM}}, year = {2013}, url = {https://doi.org/10.1145/2429069.2429114}, doi = {10.1145/2429069.2429114}, timestamp = {Thu, 24 Jun 2021 16:19:31 +0200}, biburl = {https://dblp.org/rec/conf/popl/FournetSCDSL13.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@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 = {2013 {IEEE} Symposium on Security and Privacy, {SP} 2013, Berkeley, CA, USA, May 19-22, 2013}, pages = {445--459}, publisher = {{IEEE} Computer Society}, year = {2013}, url = {https://doi.org/10.1109/SP.2013.37}, doi = {10.1109/SP.2013.37}, timestamp = {Wed, 16 Oct 2019 14:14:51 +0200}, biburl = {https://dblp.org/rec/conf/sp/BhargavanFKPS13.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:conf/popl/StrubSFC12, author = {Pierre{-}Yves Strub and Nikhil Swamy and C{\'{e}}dric Fournet and Juan Chen}, editor = {John Field and Michael Hicks}, title = {Self-certification: bootstrapping certified typecheckers in F* with Coq}, booktitle = {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}, publisher = {{ACM}}, year = {2012}, url = {https://doi.org/10.1145/2103656.2103723}, doi = {10.1145/2103656.2103723}, timestamp = {Thu, 24 Jun 2021 16:19:31 +0200}, biburl = {https://dblp.org/rec/conf/popl/StrubSFC12.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:conf/ccs/FournetKS11, author = {C{\'{e}}dric Fournet and Markulf Kohlweiss and Pierre{-}Yves Strub}, editor = {Yan Chen and George Danezis and Vitaly Shmatikov}, title = {Modular code-based cryptographic verification}, booktitle = {Proceedings of the 18th {ACM} Conference on Computer and Communications Security, {CCS} 2011, Chicago, Illinois, USA, October 17-21, 2011}, pages = {341--350}, publisher = {{ACM}}, year = {2011}, url = {https://doi.org/10.1145/2046707.2046746}, doi = {10.1145/2046707.2046746}, timestamp = {Tue, 10 Nov 2020 19:56:39 +0100}, biburl = {https://dblp.org/rec/conf/ccs/FournetKS11.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@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}, editor = {Manuel M. T. Chakravarty and Zhenjiang Hu and Olivier Danvy}, title = {Secure distributed programming with value-dependent types}, booktitle = {Proceeding of the 16th {ACM} {SIGPLAN} international conference on Functional Programming, {ICFP} 2011, Tokyo, Japan, September 19-21, 2011}, pages = {266--278}, publisher = {{ACM}}, year = {2011}, url = {https://doi.org/10.1145/2034773.2034811}, doi = {10.1145/2034773.2034811}, timestamp = {Thu, 24 Jun 2021 16:19:30 +0200}, biburl = {https://dblp.org/rec/conf/icfp/SwamyCFSBY11.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@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 = {Proceedings of the 26th Annual {IEEE} Symposium on Logic in Computer Science, {LICS} 2011, June 21-24, 2011, Toronto, Ontario, Canada}, pages = {143--151}, publisher = {{IEEE} Computer Society}, year = {2011}, url = {https://doi.org/10.1109/LICS.2011.37}, doi = {10.1109/LICS.2011.37}, timestamp = {Wed, 16 Oct 2019 14:14:54 +0200}, biburl = {https://dblp.org/rec/conf/lics/BarrasJSW11.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:conf/csl/Strub10, author = {Pierre{-}Yves Strub}, editor = {Anuj Dawar and Helmut Veith}, title = {Coq Modulo Theory}, booktitle = {Computer Science Logic, 24th International Workshop, {CSL} 2010, 19th Annual Conference of the EACSL, Brno, Czech Republic, August 23-27, 2010. Proceedings}, series = {Lecture Notes in Computer Science}, volume = {6247}, pages = {529--543}, publisher = {Springer}, year = {2010}, url = {https://doi.org/10.1007/978-3-642-15205-4\_40}, doi = {10.1007/978-3-642-15205-4\_40}, timestamp = {Tue, 14 May 2019 10:00:42 +0200}, biburl = {https://dblp.org/rec/conf/csl/Strub10.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@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}, url = {https://tel.archives-ouvertes.fr/tel-00351837}, timestamp = {Tue, 21 Jul 2020 01:00:00 +0200}, biburl = {https://dblp.org/rec/phd/hal/Strub08.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:conf/ifipTCS/BlanquiJS08, author = {Fr{\'{e}}d{\'{e}}ric Blanqui and Jean{-}Pierre Jouannaud and Pierre{-}Yves Strub}, editor = {Giorgio Ausiello and Juhani Karhum{\"{a}}ki and Giancarlo Mauri and C.{-}H. Luke Ong}, title = {From Formal Proofs to Mathematical Proofs: {A} Safe, Incremental Way for Building in First-order Decision Procedures}, booktitle = {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}, series = {{IFIP}}, volume = {273}, pages = {349--365}, publisher = {Springer}, year = {2008}, url = {https://doi.org/10.1007/978-0-387-09680-3\_24}, doi = {10.1007/978-0-387-09680-3\_24}, timestamp = {Fri, 27 Sep 2019 10:35:17 +0200}, biburl = {https://dblp.org/rec/conf/ifipTCS/BlanquiJS08.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@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}, url = {http://arxiv.org/abs/0804.3762}, eprinttype = {arXiv}, eprint = {0804.3762}, timestamp = {Mon, 13 Aug 2018 01:00:00 +0200}, biburl = {https://dblp.org/rec/journals/corr/abs-0804-3762.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:conf/csl/BlanquiJS07, author = {Fr{\'{e}}d{\'{e}}ric Blanqui and Jean{-}Pierre Jouannaud and Pierre{-}Yves Strub}, editor = {Jacques Duparc and Thomas A. Henzinger}, title = {Building Decision Procedures in the Calculus of Inductive Constructions}, booktitle = {Computer Science Logic, 21st International Workshop, {CSL} 2007, 16th Annual Conference of the EACSL, Lausanne, Switzerland, September 11-15, 2007, Proceedings}, series = {Lecture Notes in Computer Science}, volume = {4646}, pages = {328--342}, publisher = {Springer}, year = {2007}, url = {https://doi.org/10.1007/978-3-540-74915-8\_26}, doi = {10.1007/978-3-540-74915-8\_26}, timestamp = {Tue, 14 May 2019 10:00:42 +0200}, biburl = {https://dblp.org/rec/conf/csl/BlanquiJS07.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@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}, url = {http://arxiv.org/abs/0707.1266}, eprinttype = {arXiv}, eprint = {0707.1266}, timestamp = {Mon, 13 Aug 2018 01:00:00 +0200}, biburl = {https://dblp.org/rec/journals/corr/abs-0707-1266.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@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 = {Proceedings of the 2001 International Conference on Image Processing, {ICIP} 2001, Thessaloniki, Greece, October 7-10, 2001}, pages = {70--73}, publisher = {{IEEE}}, year = {2001}, url = {https://doi.org/10.1109/ICIP.2001.958053}, doi = {10.1109/ICIP.2001.958053}, timestamp = {Wed, 16 Oct 2019 14:14:52 +0200}, biburl = {https://dblp.org/rec/conf/icip/GeraudSD01.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }

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