Jonathan Protzenko

ORCID

Publication Activity (10 Years)

Years Active: 2013-2024
Publications (10 Years): 43

Top Venues

CoRR

IACR Cryptol. ePrint Arch.

IEEE Symposium on Security and Privacy

Proc. ACM Program. Lang.

Paris Diderot University, France (PHD)

Education History

Paris Diderot University, France

PHD

Publications

Son Ho, Aymeric Fromherz, Jonathan Protzenko
Sound Borrow-Checking for Rust via Symbolic Semantics. CoRR (2024)
Antonin Reitz, Aymeric Fromherz, Jonathan Protzenko
StarMalloc: A Formally Verified, Concurrent, Performant, and Security-Oriented Memory Allocator. CoRR (2024)
Théophile Wallez, Jonathan Protzenko, Karthikeyan Bhargavan
Comparse: Provably Secure Formats for Cryptographic Protocols. IACR Cryptol. ePrint Arch. 2023 (2023)
Karthikeyan Bhargavan, Jonathan Protzenko, Andreas Rossberg, Deian Stefan
Foundations of WebAssembly (Dagstuhl Seminar 23101). Dagstuhl Reports 13 (3) (2023)
Son Ho, Aymeric Fromherz, Jonathan Protzenko
Modularity, Code Specialization, and Zero-Cost Abstractions for Program Verification. Proc. ACM Program. Lang. 7 (ICFP) (2023)
Théophile Wallez, Jonathan Protzenko, Karthikeyan Bhargavan
Comparse: Provably Secure Formats for Cryptographic Protocols. CCS (2023)
Théophile Wallez, Jonathan Protzenko, Benjamin Beurdouche, Karthikeyan Bhargavan
TreeSync: Authenticated Group Management for Messaging Layer Security. USENIX Security Symposium (2023)
Son Ho, Jonathan Protzenko
Aeneas: Rust Verification by Functional Translation. CoRR (2022)
Son Ho, Jonathan Protzenko, Abhishek Bichhawat, Karthikeyan Bhargavan
Noise*: A Library of Verified High-Performance Secure Channel Protocol Implementations. IEEE Symposium on Security and Privacy (2022)
Son Ho, Jonathan Protzenko
Aeneas: Rust verification by functional translation. Proc. ACM Program. Lang. 6 (ICFP) (2022)
Théophile Wallez, Jonathan Protzenko, Benjamin Beurdouche, Karthikeyan Bhargavan
TreeSync: Authenticated Group Management for Messaging Layer Security. IACR Cryptol. ePrint Arch. 2022 (2022)
Son Ho, Jonathan Protzenko, Abhishek Bichhawat, Karthikeyan Bhargavan
Noise*: A Library of Verified High-Performance Secure Channel Protocol Implementations (Long Version). IACR Cryptol. ePrint Arch. 2022 (2022)
Arvind Arasu, Badrish Chandramouli, Johannes Gehrke, Esha Ghosh, Donald Kossmann, Jonathan Protzenko, Ravi Ramamurthy, Tahina Ramananandro, Aseem Rastogi, Srinath T. V. Setty, Nikhil Swamy, Alexander van Renen, Min Xu
FastVer: Making Data Integrity a Commodity. SIGMOD Conference (2021)
Denis Merigoux, Raphaël Monat, Jonathan Protzenko
A modern compiler for the French tax code. CC (2021)
Denis Merigoux, Nicolas Chataing, Jonathan Protzenko
Catala: A Programming Language for the Law. CoRR (2021)
Jonathan Protzenko, Son Ho
Zero-cost meta-programmed stateful functors in F. CoRR (2021)
Denis Merigoux, Nicolas Chataing, Jonathan Protzenko
Catala: a programming language for the law. Proc. ACM Program. Lang. 5 (ICFP) (2021)
Antoine Delignat-Lavaud, Cédric Fournet, Bryan Parno, Jonathan Protzenko, Tahina Ramananandro, Jay Bosamiya, Joseph Lallemand, Itsaka Rakotonirina, Yi Zhou
A Security Model and Fully Verified Implementation for the IETF QUIC Record Layer. IEEE Symposium on Security and Privacy (2021)
Marina Polubelova, Karthikeyan Bhargavan, Jonathan Protzenko, Benjamin Beurdouche, Aymeric Fromherz, Natalia Kulatova, Santiago Zanella Béguelin
HACLxN: Verified Generic SIMD Crypto (for all your favourite platforms). CCS (2020)
Jonathan Protzenko, Bryan Parno, Aymeric Fromherz, Chris Hawblitzel, Marina Polubelova, Karthikeyan Bhargavan, Benjamin Beurdouche, Joonwon Choi, Antoine Delignat-Lavaud, Cédric Fournet, Natalia Kulatova, Tahina Ramananandro, Aseem Rastogi, Nikhil Swamy, Christoph M. Wintersteiger, Santiago Zanella Béguelin
EverCrypt: A Fast, Verified, Cross-Platform Cryptographic Provider. IEEE Symposium on Security and Privacy (2020)
Denis Merigoux, Raphaël Monat, Jonathan Protzenko
A Modern Compiler for the French Tax Code. CoRR (2020)
Antoine Delignat-Lavaud, Cédric Fournet, Bryan Parno, Jonathan Protzenko, Tahina Ramananandro, Jay Bosamiya, Joseph Lallemand, Itsaka Rakotonirina, Yi Zhou
A Security Model and Fully Verified Implementation for the IETF QUIC Record Layer. IACR Cryptol. ePrint Arch. 2020 (2020)
Marina Polubelova, Karthikeyan Bhargavan, Jonathan Protzenko, Benjamin Beurdouche, Aymeric Fromherz, Natalia Kulatova, Santiago Zanella Béguelin
HACL×N: Verified Generic SIMD Crypto (for all your favorite platforms). IACR Cryptol. ePrint Arch. 2020 (2020)
Jonathan Protzenko, Bryan Parno, Aymeric Fromherz, Chris Hawblitzel, Marina Polubelova, Karthikeyan Bhargavan, Benjamin Beurdouche, Joonwon Choi, Antoine Delignat-Lavaud, Cédric Fournet, Tahina Ramananandro, Aseem Rastogi, Nikhil Swamy, Christoph M. Wintersteiger, Santiago Zanella Béguelin
EverCrypt: A Fast, Verified, Cross-Platform Cryptographic Provider. IACR Cryptol. ePrint Arch. 2019 (2019)
Jonathan Protzenko, Benjamin Beurdouche, Denis Merigoux, Karthikeyan Bhargavan
Formally Verified Cryptographic Web Applications in WebAssembly. IEEE Symposium on Security and Privacy (2019)
Jonathan Protzenko, Benjamin Beurdouche, Denis Merigoux, Karthikeyan Bhargavan
Formally Verified Cryptographic Web Applications in WebAssembly. IACR Cryptol. ePrint Arch. 2019 (2019)
Guido Martínez, Danel Ahman, Victor Dumitrescu, Nick Giannarakis, Chris Hawblitzel, Catalin Hritcu, Monal Narasimhamurthy, Zoe Paraskevopoulou, Clément Pit-Claudel, Jonathan Protzenko, Tahina Ramananandro, Aseem Rastogi, Nikhil Swamy
Meta-F ^\star : Proof Automation with SMT, Tactics, and Metaprograms. ESOP (2019)
Tahina Ramananandro, Antoine Delignat-Lavaud, Cédric Fournet, Nikhil Swamy, Tej Chajed, Nadim Kobeissi, Jonathan Protzenko
EverParse: Verified Secure Zero-Copy Parsers for Authenticated Message Formats. USENIX Security Symposium (2019)
Niklas Grimm, Kenji Maillard, Cédric Fournet, Catalin Hritcu, Matteo Maffei, Jonathan Protzenko, Tahina Ramananandro, Aseem Rastogi, Nikhil Swamy, Santiago Zanella Béguelin
A monadic framework for relational verification: applied to information security, program equivalence, and optimizations. CPP (2018)
Guido Martínez, Danel Ahman, Victor Dumitrescu, Nick Giannarakis, Chris Hawblitzel, Catalin Hritcu, Monal Narasimhamurthy, Zoe Paraskevopoulou, Clément Pit-Claudel, Jonathan Protzenko, Tahina Ramananandro, Aseem Rastogi, Nikhil Swamy
Meta-F*: Metaprogramming and Tactics in an Effectful Program Verifier. CoRR (2018)
Antoine Delignat-Lavaud, Cédric Fournet, Markulf Kohlweiss, Jonathan Protzenko, Aseem Rastogi, Nikhil Swamy, Santiago Zanella Béguelin, Karthikeyan Bhargavan, Jianyang Pan, Jean Karim Zinzindohoue
Implementing and Proving the TLS 1.3 Record Layer. IEEE Symposium on Security and Privacy (2017)
Jonathan Protzenko, Jean Karim Zinzindohoué, Aseem Rastogi, Tahina Ramananandro, Peng Wang, Santiago Zanella Béguelin, Antoine Delignat-Lavaud, Catalin Hritcu, Karthikeyan Bhargavan, Cédric Fournet, Nikhil Swamy
. CoRR (2017)
Jonathan Protzenko, Jean Karim Zinzindohoué, Aseem Rastogi, Tahina Ramananandro, Peng Wang, Santiago Zanella Béguelin, Antoine Delignat-Lavaud, Catalin Hritcu, Karthikeyan Bhargavan, Cédric Fournet, Nikhil Swamy
Verified low-level programming embedded in F. Proc. ACM Program. Lang. 1 (ICFP) (2017)
Niklas Grimm, Kenji Maillard, Cédric Fournet, Catalin Hritcu, Matteo Maffei, Jonathan Protzenko, Aseem Rastogi, Nikhil Swamy, Santiago Zanella Béguelin
A Monadic Framework for Relational Verification (Functional Pearl). CoRR (2017)
Karthikeyan Bhargavan, Barry Bond, Antoine Delignat-Lavaud, Cédric Fournet, Chris Hawblitzel, Catalin Hritcu, Samin Ishtiaq, Markulf Kohlweiss, Rustan Leino, Jay R. Lorch, Kenji Maillard, Jianyang Pan, Bryan Parno, Jonathan Protzenko, Tahina Ramananandro, Ashay Rane, Aseem Rastogi, Nikhil Swamy, Laure Thompson, Peng Wang, Santiago Zanella Béguelin, Jean Karim Zinzindohoue
Everest: Towards a Verified, Drop-in Replacement of HTTPS. SNAPL (2017)
Danel Ahman, Catalin Hritcu, Kenji Maillard, Guido Martínez, Gordon D. Plotkin, Jonathan Protzenko, Aseem Rastogi, Nikhil Swamy
Dijkstra monads for free. POPL (2017)
Jean Karim Zinzindohoué, Karthikeyan Bhargavan, Jonathan Protzenko, Benjamin Beurdouche
HACL*: A Verified Modern Cryptographic Library. CCS (2017)
Jean Karim Zinzindohoué, Karthikeyan Bhargavan, Jonathan Protzenko, Benjamin Beurdouche
HACL*: A Verified Modern Cryptographic Library. IACR Cryptol. ePrint Arch. 2017 (2017)
Thomas Ball, Jonathan Protzenko, Judith Bishop, Michal Moskal, Jonathan de Halleux, Michael Braun, Steve Hodges, Clare Riley
Microsoft touch develop and the BBC micro: bit. ICSE (Companion Volume) (2016)
Thibaut Balabonski, François Pottier, Jonathan Protzenko
The Design and Formalization of Mezzo, a Permission-Based Programming Language. ACM Trans. Program. Lang. Syst. 38 (4) (2016)
Danel Ahman, Catalin Hritcu, Guido Martínez, Gordon D. Plotkin, Jonathan Protzenko, Aseem Rastogi, Nikhil Swamy
Dijkstra Monads for Free. CoRR (2016)
Karthikeyan Bhargavan, Antoine Delignat-Lavaud, Cédric Fournet, Markulf Kohlweiss, Jianyang Pan, Jonathan Protzenko, Aseem Rastogi, Nikhil Swamy, Santiago Zanella Béguelin, Jean Karim Zinzindohoue
Implementing and Proving the TLS 1.3 Record Layer. IACR Cryptol. ePrint Arch. 2016 (2016)
Sebastian Burckhardt, Jonathan Protzenko
Abstract Specifications for Weakly Consistent Data. IEEE Data Eng. Bull. 39 (1) (2016)
François Pottier, Jonathan Protzenko
A Few Lessons from the Mezzo Project. SNAPL (2015)
Sebastian Burckhardt, Daan Leijen, Jonathan Protzenko, Manuel Fähndrich
Global Sequence Protocol: A Robust Abstraction for Replicated Shared State. ECOOP (2015)
Thomas Ball, Sebastian Burckhardt, Jonathan de Halleux, Michal Moskal, Jonathan Protzenko, Nikolai Tillmann
Beyond Open Source: The Touch Develop Cloud-Based Integrated Development Environment. MOBILESoft (2015)
Jonathan Protzenko
Functional Pearl: the Proof Search Monad. IWIL@LPAR (2015)
Jonathan Protzenko, Sebastian Burckhardt, Michal Moskal, Jedidiah McClurg
Implementing real-time collaboration in TouchDevelop using AST merges. MobileDeLi (2015)
Thibaut Balabonski, François Pottier, Jonathan Protzenko
Type Soundness and Race Freedom for Mezzo. FLOPS (2014)
Jonathan Protzenko
Illustrating the Mezzo programming language. FSFMA (2013)
Jonathan Protzenko
Illustrating the Mezzo programming language. CoRR (2013)
Armaël Guéneau, François Pottier, Jonathan Protzenko
The ins and outs of iteration in Mezzo. CoRR (2013)
Jonathan Protzenko, François Pottier
Programming with Permissions in Mezzo. CoRR (2013)
Jonathan Protzenko
The implementation of the Mezzo type-checker. IFL (2013)
François Pottier, Jonathan Protzenko
Programming with permissions in Mezzo. ICFP (2013)

Jonathan Protzenko.css-eqlu8i{font-size:small;padding-left:4px;}

Publication Activity (10 Years)

Top Topics

Top Venues

Jonathan Protzenko