12th International Conference on Interactive Theorem Proving (ITP 2021) MO Myreen, N Polikarpova, A Popescu, T Bauereiss, P Lammich, ... Schloss Dagstuhl-Leibniz-Zentrum für Informatik GmbH, 2021 | | 2021 |
A calculus of congruent constructions F Blanqui, JP Jouannaud, PY Strub Unpublished draft, 2005 | 8 | 2005 |
A drag-and-drop proof tactic P Donato, PY Strub, B Werner Proceedings of the 11th ACM SIGPLAN International Conference on Certified …, 2022 | 15 | 2022 |
A formal disproof of hirsch conjecture X Allamigeon, Q Canu, PY Strub Proceedings of the 12th ACM SIGPLAN International Conference on Certified …, 2023 | 4 | 2023 |
A formal library for elliptic curves in the Coq proof assistant EI Bartzia, PY Strub International Conference on Interactive Theorem Proving, 77-92, 2014 | 22 | 2014 |
A Formalization of the Proof of Correctness of a Number-Theoretic Transform in the Context of the Hakyber Cryptographic Primitive A Séré, PY Strub Journées 2022 du GT” Méthodes Formelles pour la Sécurité”, GdR Sécurité …, 2022 | | 2022 |
A machine-checked proof of security for AWS key management service JB Almeida, M Barbosa, G Barthe, M Campagna, E Cohen, B Gregoire, ... Proceedings of the 2019 ACM SIGSAC Conference on Computer and Communications …, 2019 | 26 | 2019 |
A messy state of the union B Beurdouche, A Delignat-Lavaud, C Fournet, M Kohlweiss, A Pironti, ... | 1 | |
A messy state of the union: taming the composite state machines of TLS K Bhargavan, B Beurdouche, A Delignat-Lavaud, C Fournet, M Kohlweiss, ... Communications of the ACM 60 (2), 99-107, 2017 | | 2017 |
A messy state of the union: Taming the composite state machines of TLS B Beurdouche, K Bhargavan, A Delignat-Lavaud, C Fournet, M Kohlweiss, ... Communications of the ACM 60 (2), 99-107, 2017 | 404 | 2017 |
A program logic for probabilistic programs G Barthe, T Espitau, M Gaboardi, B Grégoire, J Hsu, PY Strub Available at justinh. su/files/papers/ellora. pdf, 2016 | 8 | 2016 |
A program logic for union bounds G Barthe, M Gaboardi, B Grégoire, J Hsu, PY Strub arXiv preprint arXiv:1602.05681, 2016 | 34 | 2016 |
A relational logic for higher-order programs A Aguirre, G Barthe, M Gaboardi, D Garg, PY Strub Proceedings of the ACM on Programming Languages 1 (ICFP), 1-29, 2017 | 68 | 2017 |
A Relational Logic for Higher-Order Programs (Additional material) A AGUIRRE, G BARTHE, M GABOARDI, D GARG, PY STRUB | | 2017 |
A Tight Security Proof for , Formally Verified M Barbosa, F Dupressoir, A Hülsing, M Meijers, PY Strub Cryptology ePrint Archive, 2024 | | 2024 |
Actema: une interface graphique et gestuelle pour preuves formelles (démonstration) P Donato, PY Strub, B Werner 33èmes Journées Francophones des Langages Applicatifs, 267-268, 2022 | | 2022 |
Advanced probabilistic couplings for differential privacy G Barthe, N Fong, M Gaboardi, B Grégoire, J Hsu, PY Strub Proceedings of the 2016 ACM SIGSAC Conference on Computer and Communications …, 2016 | 63 | 2016 |
An assertion-based program logic for probabilistic programs G Barthe, T Espitau, M Gaboardi, B Grégoire, J Hsu, PY Strub Programming Languages and Systems: 27th European Symposium on Programming …, 2018 | 30 | 2018 |
An implementation of TLS 1.2 with verified cryptographic security C Fournet, K Bhargavan, M Kohlweiss, A Pironti, PY Strub Proceedings of the Second international conference on Principles of Security …, 2013 | 1 | 2013 |
Building decision procedures in the calculus of inductive constructions F Blanqui, JP Jouannaud, PY Strub Computer Science Logic: 21st International Workshop, CSL 2007, 16th Annual …, 2007 | 24 | 2007 |