Jonathan Protzenko

I am now a post-doc researcher in the RiSE group at Microsoft Research Redmond. These days, my main area of interest is F*, the new language of the future, in particular its application to the miTLS project. My new project, KreMLin, compiles a subset of F* programs into efficient, readable C code. The flagship application is HACL*, a side-channel resistant, memory-safe, functionally-correct cryptographic library.

I spent most of 2015 working with the BBC on the micro:bit, a cool device that will hopefully get more kids into programming. Previously, I spent a bunch of time at INRIA, where I worked with François designing Mezzo, the (former) language of the future.

📧 jonathan.protzenko@ens-lyon.org

Research

🌲 F* / TLS

  • 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. Submitted. [ arXiv ]
  • Karthikeyan Bhargavan, Antoine Delignat-Lavaud, Cedric Fournet, Catalin Hritcu, Jonathan Protzenko, Tahina Ramananandro, Aseem Rastogi, Nikhil Swamy, Peng Wang, Santiago Zanella-Beguelin, Jean-Karim Zinzindohoue. Verified Low-Level Programming Embedded in F*. Submitted. [ 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. To appear 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 ]
  • 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 ]

🌲 Distributed memory models

  • Sebastian Burckhardt, Jonathan Protzenko. Abstract Specifications for Weakly Consistent Data. IEEE Data Eng. Bull. 39 (1), 45-51, 2016. [ PDF ]
  • 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 ]

🌲 TouchDevelop

  • 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 ]

🌲 Mezzo

My PhD thesis was about Mezzo. Mezzo is a programming language in the tradition of ML, which tracks ownership and aliasing in an accurate manner. Thanks to a careful balance between static verification and runtime checks, we believe Mezzo enables the programmer to write more powerful programs, especially in a concurrent setting.

Quick links: source code (on GitHub) — project homepage — try Mezzo in your browser!

Selected Mezzo publications:

  • 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 ]
    This is the reference paper: starts with a gentle introduction, moves on to the core language, defines the syntax and type system. A major section of the paper describes the newer, modular proof of soundness. We also talk about the implementation.
  • François Pottier and Jonathan Protzenko. A few lessons from the Mezzo project. In Summit oN Advances in Programming Languages (SNAPL), May 2015. [ PDF ]
    A retrospective on the project, and a few things we've learned.
  • François Pottier and Jonathan Protzenko Programming with permissions in Mezzo. ICFP'13. [ PDF ]
    A gentle introduction to the Mezzo language.
  • Jonathan Protzenko. Mezzo, the language of the future. PhD Dissertation, INRIA, September 2014. [ PDF ]
    The most up-to-date document for the implementation of the Mezzo type-checker.
  • Armaël Guéneau, François Pottier, and Jonathan Protzenko. The ins and outs of iteration in Mezzo. HOPE'13. [ PDF ]
    A good illustration of the expressive power of Mezzo.

More Mezzo publications

🌲 OCaml

  • Thomas Braibant, Jonathan Protzenko, Gabriel Scherer. ArtiCheck: well-typed generic fuzzing for module interfaces. ML'14. [ PDF ]
  • Jonathan Protzenko, Gabriel Scherer. A toy type language [ Part 1, Part 2, Part 3 ]
    A three-part series. The first part is about writing a parser and a pretty-printer with a one-to-one correspondence so that the pretty-printer does "perfect parenthesizing". The second part is about variance, presented as a system of mutually recursive equations. The last part is about solving the equations using Pottier's Fix library. No groundbreaking science in there, but mostly a collection of nice tricks that didn't seem to be widely known.
  • Jonathan Protzenko. Translating a subset of OCaml into System F. Master's thesis, 2010. [ PDF ] [ source code ]

🌲 Books and other publications

  • Jonathan Protzenko, with contributions by Benoît Picaud. Les Cahiers du programmeur XUL, Eyrolles, 2005. [ the book's website ]
    I wrote a book about developing Mozilla addons. I was younger, back then.
  • Jonathan Protzenko. XUL: Entwicklung von Rich Clients mit der Mozilla XML User Interface Language, Open Source Press, 2007.
    German translation of the French book.
  • Jonathan Protzenko. Communities and modularity, a study on complex networks. Undergrad's thesis, 2008. [ PDF ] [ Subgraphs used in the paper: www.embruns.net, www.blogeee.net, www.mozilla.org, www.suez.fr, www.ixxi.fr, www.ens-lyon.fr, www.veolia.fr ]
  • Jonathan Protzenko, A survey of Itanium, course assignment, 2008.
    Itanium's a cool architecture, but no one's using it. [ PDF ]
  • Jonathan Protzenko, A survey of register allocation, course assignment, 2009.
    Register allocation is a complicated problem. [ PDF ]

🌲 Selected talks

  • Secure compilation from F* to C using the KreMLin compiler, Models and Tools for Security Analysis and Proofs (MTP), 2017. [ PDF ] This is an improved version of talk previously given at the ML Workshop (2016) and the Secure Compilation Meeting (POPL'17 workshop).
  • Young Researcher Panel Session, Programming Languages Mentoring Workshop (PLMW), 2017. [ Website ]
  • GSP: a memory model for distributed systems (invited), Journées Francophones du Logiciel Applicatif (JFLA), 2016. [ PDF ] Talk also given at Gallium (INRIA Paris) and Celtique (INRIA Rennes).
  • The BBC micro:bit and TouchDevelop (keynote), Programming for Mobile and Touch (PROMOTO) 2015. [ PPTX ] Talk also given at the Workshop on Programming Languages Technology for Massive Open Online Courses (PLOOC), 2015.
  • Translating from TouchDevelop to C++11 (short presentation), cppcon (the c++ conference), 2015. [ PPTX ]
  • Mezzo, the language of the future PhD defense, September 2014. [ PDF ]
  • The design of Mezzo, a new programming language ICFP'13. [ PDF ] I gave variations of "the Mezzo talk" at: INRIA (Rocquencourt, 2011), the PPS lab (Paris, 2012), the Proval team (Saclay, 2012), Texas A&M university (Texas, USA, 2012), Google (New York, USA, 2012), the Computer Lab (Cambridge, UK, 2013), INRIA (Rennes, Celtique Team, 2014), Microsoft Research (Redmond, USA, 2014), Microsoft C++ team (Redmond, USA, 2015), as well as all the other locations mentioned above (IFL, ICFP, ML, FSFMA, and finally my PhD defense). Dr. Pottier also gave several more Mezzo talks!
  • Why design a new programming language? FSFMA'13. [ PDF ]
  • What is type-checking? INRIA Junior Seminar, June 2013. [ PDF |  Video ]
  • An introduction to Mezzo (short). ML'12. [ PDF | YouTube ]

Teaching

🌲 Lectures

🌲 Junior Seminar

With Mathieu Feuillet and Emanuele Leoncini, I kept the Junior Seminar running at Rocquencourt for two years. The seminar is now in the good hands of Elisa Schenone, Pauline Traynard and Jacques-Henri Jourdan. [ The seminar's web page ]

🌲 Teaching assistantship

  • 2013-2014 I worked on the online algorithms course from École Polytechnique, on Coursera.
  • 2011-2013 I was a teaching assistant for INF431 (algorithms) and « Modal Web » (Web programming) at École Polytechnique
  • 2010-2011 I was a teaching assistant for INF311 (introduction to algorithms) at École Polytechnique

Hacking

🌲 The BBC micro:bit

I did a few fun hardware projects with the BBC micro:bit. Here's some cursory instructions for creating a clock / temperature display; you can also live-stream sensor data from the micro:bit to your javascript web page over usb (very rough instructions).

🌲 OCaml

When I get headaches from working on type systems, I maintain the OCaml installer for Windows. Not sure what's worse. [ download ] [ on GitHub ]

🌲 Mozilla

I'm a Mozilla contributor although I haven't had much time available lately. I maintain addons, attend MozCamps when time permits, give a few talks here and there, and occasionally lurk on IRC. I mostly hack on Thunderbird, but I've been known to fix a few bugs in Gecko and Firefox.

  • Thunderbird Conversations
    I assumed it would take me two months to write this addon, it took me two years. [ download it ] [ on GitHub ] [ development builds ]
  • Manually Sort Folders
    Another addon, because I like to have my folders tidy. [ download it ] [ on GitHub ]
  • Latex It!
    Render LaTeX formulas in your emails as images, so that the recipient sees a nice formula instead of raw LaTeX code. [ download it ] [ on GitHub ]
  • Compose for Thunderbird, abandoned
    Re-implements the composition workflow, including the UI, and the sending backend, in Javascript, by leveraging CKEditor. That's just too much work for a single person, so I abandoned the project. Plus, I'm trying to get a life. [ download it ] [ on GitHub ]
  • Thunderbird Stdlib
    A toolkit that you can build upon for your Thunderbird addons. Used heavily by Conversations and Compose. [ on GitHub ]
  • FOSDEM 2011
    I gave a talk on developing Thunderbird Addons at FOSDEM 2011, in Brussels. I don't know where the slides are. Anyway, the ones from the MozCamp are better.
  • MozCamp 2011
    I gave a talk on developing Thunderbird Addons at MozCamp 2011, in Berlin. [ demo addons ] [ the presentation ]
  • FOSDEM 2012
    I gave a talk on developing Thunderbird Addons at FOSDEM 2012, in Brussels. [ demo addons ] [ the presentation ]

🌲 Misc.

  • A stylesheet for OCamldoc.
    Because I don't like the default style. [ an OCaml module ] [ sample documentation ] [ the stylesheet ]
  • A stylesheet for LaTeX documents.
    It gives a very condensed, two-column layout for article document classes. It also adds a \part command that gives the book-like heading seen in my reports (see here for an example). The heading was initially an attempt to reproduce the style of the French LaTeX pour l'impatient book. [ the stylesheet ]
  • An IRC client written in PHP-GTk.
    When I was in high school, I would stay up all night during summer break and code like a madman. Those were the days. [ the result ]