Jonathan Protzenko

64 papers A* 12A 3B 2Misc 1Journal 34Unranked 10
YearRankTypeTitle / Venue / Authors
2025 — conf
Charon: An Analysis Framework for Rust.
CAV (4)
Son Ho, Guillaume Boisseau, Lucas Franceschino, Yoann Prak, Aymeric Fromherz, Jonathan Protzenko
2025 A* conf
TreeKEM: A Modular Machine-Checked Symbolic Security Analysis of Group Key Agreement in Messaging Layer Security.
SP
Théophile Wallez, Jonathan Protzenko, Karthikeyan Bhargavan
2025 J jnl
TreeKEM: A Modular Machine-Checked Symbolic Security Analysis of Group Key Agreement in Messaging Layer Security.
IACR Cryptol. ePrint Arch.
Théophile Wallez, Jonathan Protzenko, Karthikeyan Bhargavan
2025 — ed.
Verified Software. Theories, Tools and Experiments - 16th International Conference, VSTTE 2024, Prague, Czech Republic, October 14-15, 2024, Revised Selected Papers
VSTTE
Jonathan Protzenko, Azalea Raad
2024 J jnl
Charon: An Analysis Framework for Rust.
CoRR
Son Ho, Guillaume Boisseau, Lucas Franceschino, Yoann Prak, Aymeric Fromherz, Jonathan Protzenko
2024 J jnl
Compiling C to Safe Rust, Formalized.
CoRR
Aymeric Fromherz, Jonathan Protzenko
2024 J jnl
Sound Borrow-Checking for Rust via Symbolic Semantics.
CoRR
Son Ho, Aymeric Fromherz, Jonathan Protzenko
2024 J jnl
Sound Borrow-Checking for Rust via Symbolic Semantics.
Proc. ACM Program. Lang.
Son Ho, Aymeric Fromherz, Jonathan Protzenko
2024 J jnl
StarMalloc: A Formally Verified, Concurrent, Performant, and Security-Oriented Memory Allocator.
CoRR
Antonin Reitz, Aymeric Fromherz, Jonathan Protzenko
2024 J jnl
StarMalloc: Verifying a Modern, Hardened Memory Allocator.
Proc. ACM Program. Lang.
Antonin Reitz, Aymeric Fromherz, Jonathan Protzenko
2023 A* conf
Comparse: Provably Secure Formats for Cryptographic Protocols.
CCS
Théophile Wallez, Jonathan Protzenko, Karthikeyan Bhargavan
2023 J jnl
Comparse: Provably Secure Formats for Cryptographic Protocols.
IACR Cryptol. ePrint Arch.
Théophile Wallez, Jonathan Protzenko, Karthikeyan Bhargavan
2023 J jnl
Foundations of WebAssembly (Dagstuhl Seminar 23101).
Dagstuhl Reports
Karthikeyan Bhargavan, Jonathan Protzenko, Andreas Rossberg, Deian Stefan
2023 J jnl
Modularity, Code Specialization, and Zero-Cost Abstractions for Program Verification.
Proc. ACM Program. Lang.
Son Ho, Aymeric Fromherz, Jonathan Protzenko
2023 A* conf
TreeSync: Authenticated Group Management for Messaging Layer Security.
USENIX Security Symposium
Théophile Wallez, Jonathan Protzenko, Benjamin Beurdouche, Karthikeyan Bhargavan
2022 J jnl
Aeneas: Rust Verification by Functional Translation.
CoRR
Son Ho, Jonathan Protzenko
2022 J jnl
Aeneas: Rust verification by functional translation.
Proc. ACM Program. Lang.
Son Ho, Jonathan Protzenko
2022 J jnl
Noise*: A Library of Verified High-Performance Secure Channel Protocol Implementations (Long Version).
IACR Cryptol. ePrint Arch.
Son Ho, Jonathan Protzenko, Abhishek Bichhawat, Karthikeyan Bhargavan
2022 A* conf
Noise*: A Library of Verified High-Performance Secure Channel Protocol Implementations.
SP
Son Ho, Jonathan Protzenko, Abhishek Bichhawat, Karthikeyan Bhargavan
2022 J jnl
TreeSync: Authenticated Group Management for Messaging Layer Security.
IACR Cryptol. ePrint Arch.
Théophile Wallez, Jonathan Protzenko, Benjamin Beurdouche, Karthikeyan Bhargavan
2021 A* conf
A Security Model and Fully Verified Implementation for the IETF QUIC Record Layer.
SP
Antoine Delignat-Lavaud, Cédric Fournet, Bryan Parno, Jonathan Protzenko, Tahina Ramananandro, Jay Bosamiya, Joseph Lallemand, Itsaka Rakotonirina, Yi Zhou
2021 B conf
A modern compiler for the French tax code.
CC
Denis Merigoux, Raphaël Monat, Jonathan Protzenko
2021 J jnl
Catala: A Programming Language for the Law.
CoRR
Denis Merigoux, Nicolas Chataing, Jonathan Protzenko
2021 J jnl
Catala: a programming language for the law.
Proc. ACM Program. Lang.
Denis Merigoux, Nicolas Chataing, Jonathan Protzenko
2021 — conf
FastVer: Making Data Integrity a Commodity.
SIGMOD Conference
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
2021 J jnl
Zero-cost meta-programmed stateful functors in F.
CoRR
Jonathan Protzenko, Son Ho
2020 J jnl
A Modern Compiler for the French Tax Code.
CoRR
Denis Merigoux, Raphaël Monat, Jonathan Protzenko
2020 J jnl
A Security Model and Fully Verified Implementation for the IETF QUIC Record Layer.
IACR Cryptol. ePrint Arch.
Antoine Delignat-Lavaud, Cédric Fournet, Bryan Parno, Jonathan Protzenko, Tahina Ramananandro, Jay Bosamiya, Joseph Lallemand, Itsaka Rakotonirina, Yi Zhou
2020 A* conf
EverCrypt: A Fast, Verified, Cross-Platform Cryptographic Provider.
SP
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
2020 A* conf
HACLxN: Verified Generic SIMD Crypto (for all your favourite platforms).
CCS
Marina Polubelova, Karthikeyan Bhargavan, Jonathan Protzenko, Benjamin Beurdouche, Aymeric Fromherz, Natalia Kulatova, Santiago Zanella-Béguelin
2020 J jnl
HACL×N: Verified Generic SIMD Crypto (for all your favorite platforms).
IACR Cryptol. ePrint Arch.
Marina Polubelova, Karthikeyan Bhargavan, Jonathan Protzenko, Benjamin Beurdouche, Aymeric Fromherz, Natalia Kulatova, Santiago Zanella-Béguelin
2019 J jnl
EverCrypt: A Fast, Verified, Cross-Platform Cryptographic Provider.
IACR Cryptol. ePrint Arch.
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
2019 A* conf
EverParse: Verified Secure Zero-Copy Parsers for Authenticated Message Formats.
USENIX Security Symposium
Tahina Ramananandro, Antoine Delignat-Lavaud, Cédric Fournet, Nikhil Swamy, Tej Chajed, Nadim Kobeissi, Jonathan Protzenko
2019 A* conf
Formally Verified Cryptographic Web Applications in WebAssembly.
IEEE Symposium on Security and Privacy
Jonathan Protzenko, Benjamin Beurdouche, Denis Merigoux, Karthikeyan Bhargavan
2019 J jnl
Formally Verified Cryptographic Web Applications in WebAssembly.
IACR Cryptol. ePrint Arch.
Jonathan Protzenko, Benjamin Beurdouche, Denis Merigoux, Karthikeyan Bhargavan
2019 A conf
Meta-F ^\star : Proof Automation with SMT, Tactics, and Metaprograms.
ESOP
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
2018 B conf
A monadic framework for relational verification: applied to information security, program equivalence, and optimizations.
CPP
Niklas Grimm, Kenji Maillard, Cédric Fournet, Catalin Hritcu, Matteo Maffei, Jonathan Protzenko, Tahina Ramananandro, Aseem Rastogi, Nikhil Swamy, Santiago Zanella-Béguelin
2018 J jnl
Meta-F*: Metaprogramming and Tactics in an Effectful Program Verifier.
CoRR
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
2017 J jnl
A Monadic Framework for Relational Verification (Functional Pearl).
CoRR
Niklas Grimm, Kenji Maillard, Cédric Fournet, Catalin Hritcu, Matteo Maffei, Jonathan Protzenko, Aseem Rastogi, Nikhil Swamy, Santiago Zanella-Béguelin
2017 A* conf
Dijkstra monads for free.
POPL
Danel Ahman, Catalin Hritcu, Kenji Maillard, Guido Martínez, Gordon D. Plotkin, Jonathan Protzenko, Aseem Rastogi, Nikhil Swamy
2017 — conf
Everest: Towards a Verified, Drop-in Replacement of HTTPS.
SNAPL
Karthikeyan Bhargavan, Barry Bond, Antoine Delignat-Lavaud, Cédric Fournet, Chris Hawblitzel, Catalin Hritcu, Samin Ishtiaq, Markulf Kohlweiss, K. Rustan M. 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
2017 A* conf
HACL*: A Verified Modern Cryptographic Library.
CCS
Jean Karim Zinzindohoué, Karthikeyan Bhargavan, Jonathan Protzenko, Benjamin Beurdouche
2017 J jnl
HACL*: A Verified Modern Cryptographic Library.
IACR Cryptol. ePrint Arch.
Jean Karim Zinzindohoué, Karthikeyan Bhargavan, Jonathan Protzenko, Benjamin Beurdouche
2017 A* conf
Implementing and Proving the TLS 1.3 Record Layer.
IEEE Symposium on Security and Privacy
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
2017 J jnl
Verified Low-Level Programming Embedded in F
CoRR
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
2017 J jnl
Verified low-level programming embedded in F.
Proc. ACM Program. Lang.
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
2016 J jnl
Abstract Specifications for Weakly Consistent Data.
IEEE Data Eng. Bull.
Sebastian Burckhardt, Jonathan Protzenko
2016 J jnl
Dijkstra Monads for Free.
CoRR
Danel Ahman, Catalin Hritcu, Guido Martínez, Gordon D. Plotkin, Jonathan Protzenko, Aseem Rastogi, Nikhil Swamy
2016 J jnl
Implementing and Proving the TLS 1.3 Record Layer.
IACR Cryptol. ePrint Arch.
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
2016 — conf
Microsoft touch develop and the BBC micro: bit.
ICSE (Companion Volume)
Thomas Ball, Jonathan Protzenko, Judith Bishop, Michal Moskal, Jonathan de Halleux, Michael Braun, Steve Hodges, Clare Riley
2016 J jnl
The Design and Formalization of Mezzo, a Permission-Based Programming Language.
ACM Trans. Program. Lang. Syst.
Thibaut Balabonski, François Pottier, Jonathan Protzenko
2015 — conf
A Few Lessons from the Mezzo Project.
SNAPL
François Pottier, Jonathan Protzenko
2015 — conf
Beyond Open Source: The Touch Develop Cloud-Based Integrated Development Environment.
MOBILESoft
Thomas Ball, Sebastian Burckhardt, Jonathan de Halleux, Michal Moskal, Jonathan Protzenko, Nikolai Tillmann
2015 — conf
Functional Pearl: the Proof Search Monad.
IWIL@LPAR
Jonathan Protzenko
2015 A conf
Global Sequence Protocol: A Robust Abstraction for Replicated Shared State.
ECOOP
Sebastian Burckhardt, Daan Leijen, Jonathan Protzenko, Manuel Fähndrich
2015 — conf
Implementing real-time collaboration in TouchDevelop using AST merges.
MobileDeLi
Jonathan Protzenko, Sebastian Burckhardt, Michal Moskal, Jedidiah McClurg
2014 — —
Mezzo: a typed language for safe effectful concurrent programs. (Mezzo: un langage typé pour programmer de manière concurrent et sure en présence d'effets).
Jonathan Protzenko
2014 Misc conf
Type Soundness and Race Freedom for Mezzo.
FLOPS
Thibaut Balabonski, François Pottier, Jonathan Protzenko
2013 — conf
Illustrating the Mezzo programming language.
FSFMA
Jonathan Protzenko
2013 J jnl
Illustrating the Mezzo programming language.
CoRR
Jonathan Protzenko
2013 J jnl
Programming with Permissions in Mezzo.
CoRR
Jonathan Protzenko, François Pottier
2013 A conf
Programming with permissions in Mezzo.
ICFP
François Pottier, Jonathan Protzenko
2013 — conf
The implementation of the Mezzo type-checker.
IFL
Jonathan Protzenko
2013 J jnl
The ins and outs of iteration in Mezzo.
CoRR
Armaël Guéneau, François Pottier, Jonathan Protzenko