Jonathan Protzenko

According to our database, Jonathan Protzenko authored at least 45 papers between 2013 and 2024.

Collaborative distances:

• Dijkstra number of three.
• Erdős number of three.

2024

Sound Borrow-Checking for Rust via Symbolic Semantics.

Son Ho, Aymeric Fromherz, Jonathan Protzenko

CoRR, 2024

StarMalloc: A Formally Verified, Concurrent, Performant, and Security-Oriented Memory Allocator.

Antonin Reitz, Aymeric Fromherz, Jonathan Protzenko

CoRR, 2024

2023

Modularity, Code Specialization, and Zero-Cost Abstractions for Program Verification.

Son Ho, Aymeric Fromherz, Jonathan Protzenko

Proc. ACM Program. Lang., August, 2023

Foundations of WebAssembly (Dagstuhl Seminar 23101).

Karthikeyan Bhargavan, Jonathan Protzenko, Andreas Rossberg, Deian Stefan

Dagstuhl Reports, March, 2023

Comparse: Provably Secure Formats for Cryptographic Protocols.

Théophile Wallez, Jonathan Protzenko, Karthikeyan Bhargavan

IACR Cryptol. ePrint Arch., 2023

2022

Aeneas: Rust verification by functional translation.

Son Ho, Jonathan Protzenko

Proc. ACM Program. Lang., 2022

TreeSync: Authenticated Group Management for Messaging Layer Security.

Théophile Wallez, Jonathan Protzenko, Benjamin Beurdouche, Karthikeyan Bhargavan

IACR Cryptol. ePrint Arch., 2022

Noise*: A Library of Verified High-Performance Secure Channel Protocol Implementations (Long Version).

Son Ho, Jonathan Protzenko, Abhishek Bichhawat, Karthikeyan Bhargavan

IACR Cryptol. ePrint Arch., 2022

Noise*: A Library of Verified High-Performance Secure Channel Protocol Implementations.

Son Ho, Jonathan Protzenko, Abhishek Bichhawat, Karthikeyan Bhargavan

Proceedings of the 43rd IEEE Symposium on Security and Privacy, 2022

2021

Catala: a programming language for the law.

Denis Merigoux, Nicolas Chataing, Jonathan Protzenko

Proc. ACM Program. Lang., 2021

Zero-cost meta-programmed stateful functors in F.

Jonathan Protzenko, Son Ho

CoRR, 2021

FastVer: Making Data Integrity a Commodity.

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

Proceedings of the SIGMOD '21: International Conference on Management of Data, 2021

A modern compiler for the French tax code.

Denis Merigoux, Raphaël Monat, Jonathan Protzenko

Proceedings of the CC '21: 30th ACM SIGPLAN International Conference on Compiler Construction, 2021

2020

HACL×N: Verified Generic SIMD Crypto (for all your favorite platforms).

Marina Polubelova, Karthikeyan Bhargavan, Jonathan Protzenko, Benjamin Beurdouche, Aymeric Fromherz, Natalia Kulatova, Santiago Zanella Béguelin

IACR Cryptol. ePrint Arch., 2020

A Security Model and Fully Verified Implementation for the IETF QUIC Record Layer.

Antoine Delignat-Lavaud, Cédric Fournet, Bryan Parno, Jonathan Protzenko, Tahina Ramananandro, Jay Bosamiya, Joseph Lallemand, Itsaka Rakotonirina, Yi Zhou

IACR Cryptol. ePrint Arch., 2020

EverCrypt: A Fast, Verified, Cross-Platform Cryptographic Provider.

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

Proceedings of the 2020 IEEE Symposium on Security and Privacy, 2020

HACLxN: Verified Generic SIMD Crypto (for all your favourite platforms).

Marina Polubelova, Karthikeyan Bhargavan, Jonathan Protzenko, Benjamin Beurdouche, Aymeric Fromherz, Natalia Kulatova, Santiago Zanella Béguelin

Proceedings of the CCS '20: 2020 ACM SIGSAC Conference on Computer and Communications Security, 2020

2019

EverCrypt: A Fast, Verified, Cross-Platform Cryptographic Provider.

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

IACR Cryptol. ePrint Arch., 2019

Formally Verified Cryptographic Web Applications in WebAssembly.

Jonathan Protzenko, Benjamin Beurdouche, Denis Merigoux, Karthikeyan Bhargavan

IACR Cryptol. ePrint Arch., 2019

EverParse: Verified Secure Zero-Copy Parsers for Authenticated Message Formats.

Tahina Ramananandro, Antoine Delignat-Lavaud, Cédric Fournet, Nikhil Swamy, Tej Chajed, Nadim Kobeissi, Jonathan Protzenko

Proceedings of the 28th USENIX Security Symposium, 2019

Meta-F ^\star : Proof Automation with SMT, Tactics, and Metaprograms.

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

Proceedings of the Programming Languages and Systems, 2019

2018

Meta-F*: Metaprogramming and Tactics in an Effectful Program Verifier.

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

CoRR, 2018

A monadic framework for relational verification: applied to information security, program equivalence, and optimizations.

Niklas Grimm, Kenji Maillard, Cédric Fournet, Catalin Hritcu, Matteo Maffei, Jonathan Protzenko, Tahina Ramananandro, Aseem Rastogi, Nikhil Swamy, Santiago Zanella Béguelin

Proceedings of the 7th ACM SIGPLAN International Conference on Certified Programs and Proofs, 2018

2017

Verified low-level programming embedded in F.

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

Proc. ACM Program. Lang., 2017

HACL*: A Verified Modern Cryptographic Library.

Jean Karim Zinzindohoué, Karthikeyan Bhargavan, Jonathan Protzenko, Benjamin Beurdouche

IACR Cryptol. ePrint Arch., 2017

A Monadic Framework for Relational Verification (Functional Pearl).

Niklas Grimm, Kenji Maillard, Cédric Fournet, Catalin Hritcu, Matteo Maffei, Jonathan Protzenko, Aseem Rastogi, Nikhil Swamy, Santiago Zanella Béguelin

CoRR, 2017

Verified Low-Level Programming Embedded in F^*.

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

Everest: Towards a Verified, Drop-in Replacement of HTTPS.

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

Proceedings of the 2nd Summit on Advances in Programming Languages, 2017

Dijkstra monads for free.

Danel Ahman, Catalin Hritcu, Kenji Maillard, Guido Martínez, Gordon D. Plotkin, Jonathan Protzenko, Aseem Rastogi, Nikhil Swamy

Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, 2017

2016

The Design and Formalization of Mezzo, a Permission-Based Programming Language.

Thibaut Balabonski, François Pottier, Jonathan Protzenko

ACM Trans. Program. Lang. Syst., 2016

Implementing and Proving the TLS 1.3 Record Layer.

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

IACR Cryptol. ePrint Arch., 2016

Abstract Specifications for Weakly Consistent Data.

Sebastian Burckhardt, Jonathan Protzenko

IEEE Data Eng. Bull., 2016

Dijkstra Monads for Free.

Danel Ahman, Catalin Hritcu, Guido Martínez, Gordon D. Plotkin, Jonathan Protzenko, Aseem Rastogi, Nikhil Swamy

CoRR, 2016

Microsoft touch develop and the BBC micro: bit.

Thomas Ball, Jonathan Protzenko, Judith Bishop, Michal Moskal, Jonathan de Halleux, Michael Braun, Steve Hodges, Clare Riley

Proceedings of the 38th International Conference on Software Engineering, 2016

2015

A Few Lessons from the Mezzo Project.

François Pottier, Jonathan Protzenko

Proceedings of the 1st Summit on Advances in Programming Languages, 2015

Implementing real-time collaboration in TouchDevelop using AST merges.

Jonathan Protzenko, Sebastian Burckhardt, Michal Moskal, Jedidiah McClurg

Proceedings of the 3rd International Workshop on Mobile Development Lifecycle, 2015

Functional Pearl: the Proof Search Monad.

Jonathan Protzenko

Proceedings of the IWIL@LPAR 2015, 2015

Beyond Open Source: The Touch Develop Cloud-Based Integrated Development Environment.

Thomas Ball, Sebastian Burckhardt, Jonathan de Halleux, Michal Moskal, Jonathan Protzenko, Nikolai Tillmann

Proceedings of the 2nd ACM International Conference on Mobile Software Engineering and Systems, 2015

Global Sequence Protocol: A Robust Abstraction for Replicated Shared State.

Sebastian Burckhardt, Daan Leijen, Jonathan Protzenko, Manuel Fähndrich

Proceedings of the 29th European Conference on Object-Oriented Programming, 2015

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

PhD thesis, 2014

Type Soundness and Race Freedom for Mezzo.

Thibaut Balabonski, François Pottier, Jonathan Protzenko

Proceedings of the Functional and Logic Programming - 12th International Symposium, 2014

2013

The ins and outs of iteration in Mezzo.

Armaël Guéneau, François Pottier, Jonathan Protzenko

CoRR, 2013

The implementation of the Mezzo type-checker.

Jonathan Protzenko

Proceedings of the 25th Symposium on Implementation and Application of Functional Languages, 2013

Programming with permissions in Mezzo.

François Pottier, Jonathan Protzenko

Proceedings of the ACM SIGPLAN International Conference on Functional Programming, 2013

Illustrating the Mezzo programming language.

Jonathan Protzenko

Proceedings of the 1st French Singaporean Workshop on Formal Methods and Applications, 2013