See also: DBLP, Google Scholar

Conference, workshop & journal papers

2024:

  • Jonathan Protzenko, Bas Spitters. Modernizing FIPS for safe languages and verified libraries (FMCP@NIST). PDF

  • Antonin Reitz, Aymeric Fromherz, Jonathan Protzenko. StarMalloc: A Formally Verified, Concurrent, Performant, and Security-Oriented Memory Allocator (OOPSLA’24). arXiv

  • Son Ho, Aymeric Fromherz, Jonathan Protzenko. Sound Borrow-Checking for Rust via Symbolic Semantics (ICFP’24). arXiv

2023:

  • Théophile Wallez, Jonathan Protzenko, Karthikeyan Bhargavan. Comparse: Provably Secure Formats for Cryptographic Protocols (CCS’23). ePrint

  • Théophile Wallez, Jonathan Protzenko, Benjamin Beurdouche, Karthikeyan Bhargavan. TreeSync: Authenticated Group Management for Messaging Layer Security (Usenix Security’23). Internet Defense Prize, Distinguished Paper Award. ePrint

  • Son Ho, Aymeric Fromherz, Jonathan Protzenko. Modularity, Code Specialization, and Zero-Cost Abstractions for Program Verification (ICFP’23). arXiv

2022:

  • Son Ho, Jonathan Protzenko. Aeneas: Rust Verification by Functional Translation (ICFP’22). arXiv (long), PDF (short)

  • Son Ho, Jonathan Protzenko, Abhishek Bichhawat, Karthikeyan Bhargavan. Noise*: A Library of Verified High-Performance Secure Channel Protocol Implementations (S&P’22). ePrint

2021:

  • Denis Merigoux, Raphaël Monat, Jonathan Protzenko. A Modern Compiler for the French Tax Code (CC’21). arXiv

  • 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 (S&P’21). ePrint

  • Arvind Arasu, Badrish Chandramouli, Johannes Gehrke, Esha Ghosh, Donald Kossmann, Jonathan Protzenko, Ravi Ramamurthy, Tahina Ramananandro, Aseem Rastogi, Srinath Setty, Nikhil Swamy, Alexander van Renen, Min Xu. FastVer: Making Data Integrity a Commodity (SIGMOD’21). PDF

  • Denis Merigoux, Nicolas Chataing, Jonathan Protzenko. Catala: A Programming Language for the Law (ICFP’21). arXiv

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) (CCS’20). ePrint

  • Jonathan Protzenko, Bryan Parno, Aymeric Fromherz, Chris Hawblitzel, Marina Polubelova, Karthikeyan Bhargavan, Benjamin Beurdouche, Joonwon Choi, Antoine Delignat-Lavaud, Cedric Fournet, Natalia Kulatova, Tahina Ramananandro, Aseem Rastogi, Nikhil Swamy, Christoph Wintersteiger, Santiago Zanella-Beguelin. EverCrypt: A Fast, Verified, Cross-Platform Cryptographic Provider (S&P’20). ePrint

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’19). PDF

  • Jonathan Protzenko, Benjamin Beurdouche, Denis Merigoux, Karthikeyan Bhargavan. Formally Verified Cryptographic Web Applications in WebAssembly (S&P’19). PDF.

  • Guido Martinez, 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. (ESOP 2019). arXiv

2018:

  • 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. (CPP’18). arXiv

  • Guido Martínez, Danel Ahman, Victor Dumitrescu, Nick Giannarakis, Chris Hawblitzel, Cătălin Hriţcu, Monal Narasimhamurthy, Zoe Paraskevopoulou, Clément Pit-Claudel, Jonathan Protzenko, Tahina Ramananandro, Nikhil Swamy. ML as a Tactic Language, Again. (ML’18) PDF

2017:

  • Jean-Karim Zinzindohoué, Karthikeyan Bhargavan, Jonathan Protzenko, Benjamin Beurdouche. HACL*: A Verified Modern Cryptographic Library. In ACM Conference on Computer and Communications Security (CCS), 2017. eprint

  • Jonathan Protzenko, Jean-Karim Zinzindohoué, Aseem Rastogi, Tahina Ramananandro, Peng Wang, Santiago Zanella-Béguelin, Antoine Delignat-Lavaud, Cătălin Hriţcu, Karthikeyan Bhargavan, Cédric Fournet, and Nikhil Swamy. Verified Low-Level Programming Embedded in F*. In Proceedings of the ACM on Programming Languages 1 (ICFP), 2017. arXiv

  • Karthikeyan Bhargavan, Barry Bond, Antoine Delignat-Lavaud, Cédric Fournet, Chris Hawblitzel, Cătălin Hriţcu, Samin Ishtiaq, Markulf Kohlweiss, Rustan Leino, Jay Lorch, Kenji Maillard, Jianyang Pang, Bryan Parno, Jonathan Protzenko, Tahina Ramananandro, Ashay Rane, Aseem Rastogi, Nikhil Swamy, Laure Thompson, Peng Wang, Santiago Zanella-Béguelin, and Jean-Karim Zinzindohoué. Everest: Towards a Verified, Drop-in Replacement of HTTPS In Summit oN Advances in Programming Languages (SNAPL), May 2017. PDF

  • Karthikeyan Bhargavan, Antoine Delignat-Lavaud, Cedric Fournet, Markulf Kohlweiss, Jianyang Pan, Jonathan Protzenko, Aseem Rastogi, Nikhil Swamy, Santiago Zanella-Beguelin, Jean-Karim Zinzindohoue. Implementing and Proving the TLS 1.3 Record Layer. In Proceedings of the 38th IEEE Symposium on Security and Privacy (S&P’17), San Jose, USA. PDF

  • Danel Ahman, Cătălin Hriţcu, Guido Martínez, Gordon Plotkin, Jonathan Protzenko, Aseem Rastogi, Nikhil Swamy. Dijkstra Monads for Free. In Proceedings of the 44th ACM Symposium on Principles of Programming Languages (POPL’17), Paris, France. PDF

2016:

  • Peng Wang, Karthikeyan Bhargavan, Jean-Karim Zinzindohoué, Abhishek Anand, Cédric Fournet, Bryan Parno, Jonathan Protzenko, Aseem Rastogi, Nikhil Swamy. Extracting from F* to C: a progress report. ACM SIGPLAN Workshop on ML, 2016 PDF

  • Benjamin Beurdouche, Karthikeyan Bhargavan, Antoine Delignat-Lavaud, Cédric Fournet, Samin Ishtiaq, Markulf Kohlweiss, Jonathan Protzenko, Nikhil Swamy, Santiago Zanella-Béguelin, Jean Karim Zinzindohoué. Towards a Provably Secure Implementation of TLS 1.3, TLS, Ready Or Not? (TRON) Workshop, 2016. PDF

  • Sebastian Burckhardt, Jonathan Protzenko. Abstract Specifications for Weakly Consistent Data. IEEE Data Eng. Bull. 39 (1), 45-51, 2016. PDF

2015:

  • Sebastian Burckhardt, Daan Leijen, Jonathan Protzenko and Manuel Fähndrich. Global Sequence Protocol: A Robust Abstraction for Replicated Shared State. In Proceedings of the 29th European Conference on Object-Oriented Programming, ECOOP, vol. 15. 2015. PDF

  • Thomas Ball, Jonathan Protzenko, Judith Bishop, Michał Moskal, Jonathan de Halleux, and Michael Braun. The BBC micro:bit Coded by Microsoft Touch Develop. In ICSE 2016 Companion, ACM, May 2016. PDF

  • Thomas Ball, Sebastian Burckhardt, Jonathan de Halleux, Michal Moskal, Jonathan Protzenko, Nikolai Tillmann. Beyond Open Source: The Touch Develop Cloud-Based Integrated Development Environment. In proceedings of the 2nd ACM International Conference on Mobile Software Engineering and Systems (MOBILESoft) 2015 PDF

  • Sebastian Burckhardt, Jedidiah McClurg, Michal Moskal, Jonathan Protzenko. Real-time collaboration in TouchDevelop using AST merges. In Proceedings of the Third International Workshop on Mobile Development Lifecycle (MobileDeLi), 2015 PDF

  • Jonathan Protzenko. Pushing Blocks all the way to C++. In Proceedings of the 1st Blocks and Beyond Workshop, 2015 PDF

  • Thibaut Balabonski, François Pottier, and Jonathan Protzenko. The design and formalization of Mezzo, a permission-based programming language. ACM Transactions on Programming Languages and Systems (TOPLAS), November 2015. PDF

  • François Pottier and Jonathan Protzenko. A few lessons from the Mezzo project. In Summit oN Advances in Programming Languages (SNAPL), May 2015. PDF

2014:

  • Thibaut Balabonski, François Pottier, and Jonathan Protzenko. Type soundness and race freedom for Mezzo In Proceedings of the 12th International Symposium on Functional and Logic Programming (FLOPS 2014), volume 8475, pages 253-269, June 2014. PDF

  • Thomas Braibant, Jonathan Protzenko, Gabriel Scherer. ArtiCheck: well-typed generic fuzzing for module interfaces. ML’14. PDF

2013:

  • François Pottier and Jonathan Protzenko Programming with permissions in Mezzo. ICFP’13. PDF

  • Armaël Guéneau, François Pottier, and Jonathan Protzenko. The ins and outs of iteration in Mezzo. HOPE’13. PDF

  • Jonathan Protzenko The implementation of the Mezzo type-checker. IFL’13. PDF

  • Jonathan Protzenko Illustrating the Mezzo programming language. FSFMA’13. PDF

2012:

  • Jonathan Protzenko and François Pottier. Programming with permissions: the Mezzo language (extended abstract). ML’12. PDF

Theses

  • Jonathan Protzenko. Mezzo, the language of the future. PhD Dissertation, INRIA, September 2014. PDF

  • Jonathan Protzenko. Translating a subset of OCaml into System F. Master’s thesis, 2010. PDF source code

  • Jonathan Protzenko. Communities and modularity, a study on complex networks. Undergrad’s thesis, 2008. PDF

Books

  • Jonathan Protzenko, with contributions by Benoît Picaud. Les Cahiers du programmeur XUL, Eyrolles, 2005. the book’s website

  • Jonathan Protzenko. XUL: Entwicklung von Rich Clients mit der Mozilla XML User Interface Language, Open Source Press, 2007.

Informal

  • Jonathan Protzenko, Gabriel Scherer. A toy type language Part 1, Part 2, Part 3

  • Jonathan Protzenko. An introduction to Mezzo. Part 1, Part 2

  • Jonathan Protzenko, A survey of Itanium, course assignment, 2008. PDF

  • Jonathan Protzenko, A survey of register allocation, course assignment, 2009. PDF

  • Jonathan Protzenko, Cours de Mathématiques supérieures, a condensed summary of undergrad-level math (French) PDF

Mistakes of my youth

I wrote, while in high school, a series of six articles for the French magazine Direction|PHP. Topics I covered included glorious technologies such as SOAP, WSDL, XUL and PHP-GTk. Fortunately, there seems to be no trace left of those on the internet.