Jonathan Protzenko
Publication record assembled from the DBLP archive of ranked conferences.
Papers indexed
22
Venues
14
Active years
2013–2025
Best venue rank
A*
Where they publish
Papers
22 indexed papers, newest first.
| Year | Venue | Title | Authors |
|---|---|---|---|
| 2025 | CAV | Charon: An Analysis Framework for Rust. | Son Ho, Guillaume Boisseau, Lucas Franceschino, Yoann Prak, Aymeric Fromherz, Jonathan Protzenko |
| 2025 | SP | TreeKEM: A Modular Machine-Checked Symbolic Security Analysis of Group Key Agreement in Messaging Layer Security. | Thophile Wallez, Jonathan Protzenko, Karthikeyan Bhargavan |
| 2023 | CCS | Comparse: Provably Secure Formats for Cryptographic Protocols. | Thophile Wallez, Jonathan Protzenko, Karthikeyan Bhargavan |
| 2022 | SP | Noise*: A Library of Verified High-Performance Secure Channel Protocol Implementations. | Son Ho, Jonathan Protzenko, Abhishek Bichhawat, Karthikeyan Bhargavan |
| 2021 | CC | A modern compiler for the French tax code. | Denis Merigoux, Raphal Monat, Jonathan Protzenko |
| 2021 | SIGMOD | 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 |
| 2021 | SP | A Security Model and Fully Verified Implementation for the IETF QUIC Record Layer. | Antoine Delignat-Lavaud, Cdric Fournet, Bryan Parno, Jonathan Protzenko, Tahina Ramananandro, Jay Bosamiya, Joseph Lallemand, Itsaka Rakotonirina, Yi Zhou |
| 2020 | CCS | HACLxN: Verified Generic SIMD Crypto (for all your favourite platforms). | Marina Polubelova, Karthikeyan Bhargavan, Jonathan Protzenko, Benjamin Beurdouche, Aymeric Fromherz, Natalia Kulatova, Santiago Zanella-Bguelin |
| 2020 | SP | 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, Cdric Fournet, Natalia Kulatova, Tahina Ramananandro, Aseem Rastogi, Nikhil Swamy, Christoph M. Wintersteiger, Santiago Zanella-Bguelin |
| 2019 | ESOP | Meta-F ^\star : Proof Automation with SMT, Tactics, and Metaprograms. | Guido Martnez, Danel Ahman, Victor Dumitrescu, Nick Giannarakis, Chris Hawblitzel, Catalin Hritcu, Monal Narasimhamurthy, Zoe Paraskevopoulou, Clment Pit-Claudel, Jonathan Protzenko, Tahina Ramananandro, Aseem Rastogi, Nikhil Swamy |
| 2019 | SP | Formally Verified Cryptographic Web Applications in WebAssembly. | Jonathan Protzenko, Benjamin Beurdouche, Denis Merigoux, Karthikeyan Bhargavan |
| 2018 | CPP | A monadic framework for relational verification: applied to information security, program equivalence, and optimizations. | Niklas Grimm, Kenji Maillard, Cdric Fournet, Catalin Hritcu, Matteo Maffei, Jonathan Protzenko, Tahina Ramananandro, Aseem Rastogi, Nikhil Swamy, Santiago Zanella-Bguelin |
| 2017 | CCS | HACL*: A Verified Modern Cryptographic Library. | Jean Karim Zinzindohou, Karthikeyan Bhargavan, Jonathan Protzenko, Benjamin Beurdouche |
| 2017 | POPL | Dijkstra monads for free. | Danel Ahman, Catalin Hritcu, Kenji Maillard, Guido Martnez, Gordon D. Plotkin, Jonathan Protzenko, Aseem Rastogi, Nikhil Swamy |
| 2017 | SP | Implementing and Proving the TLS 1.3 Record Layer. | Antoine Delignat-Lavaud, Cdric Fournet, Markulf Kohlweiss, Jonathan Protzenko, Aseem Rastogi, Nikhil Swamy, Santiago Zanella-Bguelin, Karthikeyan Bhargavan, Jianyang Pan, Jean Karim Zinzindohoue |
| 2016 | ICSE | 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 |
| 2015 | ECOOP | Global Sequence Protocol: A Robust Abstraction for Replicated Shared State. | Sebastian Burckhardt, Daan Leijen, Jonathan Protzenko, Manuel Fhndrich |
| 2015 | ICSE | Beyond Open Source: The Touch Develop Cloud-Based Integrated Development Environment. | Thomas Ball, Sebastian Burckhardt, Jonathan de Halleux, Michal Moskal, Jonathan Protzenko, Nikolai Tillmann |
| 2015 | LPAR | Functional Pearl: the Proof Search Monad. | Jonathan Protzenko |
| 2015 | OOPSLA | Implementing real-time collaboration in TouchDevelop using AST merges. | Jonathan Protzenko, Sebastian Burckhardt, Michal Moskal, Jedidiah McClurg |
| 2014 | FLOPS | Type Soundness and Race Freedom for Mezzo. | Thibaut Balabonski, Franois Pottier, Jonathan Protzenko |
| 2013 | ICFP | Programming with permissions in Mezzo. | Franois Pottier, Jonathan Protzenko |