关注
Jonathan Protzenko
Jonathan Protzenko
Microsoft Research
在 ens-lyon.org 的电子邮件经过验证 - 首页
标题
引用次数
引用次数
年份
HACL*: A verified modern cryptographic library
JK Zinzindohoué, K Bhargavan, J Protzenko, B Beurdouche
Proceedings of the 2017 ACM SIGSAC Conference on Computer and Communications …, 2017
2942017
Verified low-level programming embedded in F*
J Protzenko, JK Zinzindohoué, A Rastogi, T Ramananandro, P Wang, ...
Proc. {ACM} Program. Lang., 2017
1622017
Implementing and proving the TLS 1.3 record layer
K Bhargavan, A Delignat-Lavaud, C Fournet, M Kohlweiss, J Pan, ...
SP 2017-38th IEEE Symposium on Security and Privacy, 463-482, 2017
141*2017
Evercrypt: A fast, verified, cross-platform cryptographic provider
J Protzenko, B Parno, A Fromherz, C Hawblitzel, M Polubelova, ...
2020 IEEE Symposium on Security and Privacy (SP), 983-1002, 2020
1192020
Everest: Towards a verified, drop-in replacement of HTTPS
K Bhargavan, B Bond, A Delignat-Lavaud, C Fournet, C Hawblitzel, ...
2nd Summit on Advances in Programming Languages, 2017
932017
Microsoft touch develop and the bbc micro: bit
T Ball, J Protzenko, J Bishop, M Moskal, J De Halleux, M Braun, S Hodges, ...
Proceedings of the 38th International Conference on Software Engineering …, 2016
83*2016
Dijkstra monads for free
D Ahman, C Hriţcu, K Maillard, G Martínez, G Plotkin, J Protzenko, ...
Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming …, 2017
802017
{EverParse}: Verified secure {Zero-Copy} parsers for authenticated message formats
T Ramananandro, A Delignat-Lavaud, C Fournet, N Swamy, T Chajed, ...
28th USENIX Security Symposium (USENIX Security 19), 1465-1482, 2019
782019
Global sequence protocol: A robust abstraction for replicated shared state
S Burckhardt, D Leijen, J Protzenko, M Fähndrich
29th European Conference on Object-Oriented Programming (ECOOP 2015), 2015
702015
Catala: a programming language for the law
D Merigoux, N Chataing, J Protzenko
Proceedings of the ACM on Programming Languages 5 (ICFP), 1-29, 2021
692021
Meta-F: Proof Automation with SMT, Tactics, and Metaprograms
G Martínez, D Ahman, V Dumitrescu, N Giannarakis, C Hawblitzel, ...
European Symposium on Programming, 30-59, 2019
552019
Formally verified cryptographic web applications in WebAssembly
J Protzenko, B Beurdouche, D Merigoux, K Bhargavan
542019
Programming with permissions in Mezzo
F Pottier, J Protzenko
ACM SIGPLAN Notices 48 (9), 173-184, 2013
532013
The design and formalization of Mezzo, a permission-based programming language
T Balabonski, F Pottier, J Protzenko
ACM Transactions on Programming Languages and Systems (TOPLAS) 38 (4), 1-94, 2016
372016
Aeneas: Rust verification by functional translation
S Ho, J Protzenko
Proceedings of the ACM on Programming Languages 6 (ICFP), 711-741, 2022
352022
A security model and fully verified implementation for the IETF QUIC record layer
A Delignat-Lavaud, C Fournet, B Parno, J Protzenko, T Ramananandro, ...
2021 IEEE Symposium on Security and Privacy (SP), 1162-1178, 2021
292021
Beyond open source: the touch develop cloud-based integrated development environment
T Ball, S Burckhardt, J de Halleux, M Moskal, J Protzenko, N Tillmann
2015 2nd ACM International Conference on Mobile Software Engineering and …, 2015
252015
Haclxn: Verified generic SIMD crypto (for all your favourite platforms)
M Polubelova, K Bhargavan, J Protzenko, B Beurdouche, A Fromherz, ...
Proceedings of the 2020 ACM SIGSAC Conference on Computer and Communications …, 2020
232020
A monadic framework for relational verification: applied to information security, program equivalence, and optimizations
N Grimm, K Maillard, C Fournet, C Hriţcu, M Maffei, J Protzenko, ...
Proceedings of the 7th ACM SIGPLAN International Conference on Certified …, 2018
232018
A modern compiler for the french tax code
D Merigoux, R Monat, J Protzenko
Proceedings of the 30th ACM SIGPLAN International Conference on Compiler …, 2021
202021
系统目前无法执行此操作,请稍后再试。
文章 1–20