Jonathan Protzenko

I am now a post-doc researcher in the RiSE group at Microsoft Research Redmond. I spent most of 2015 working with the BBC on the micro:bit, a cool device that will hopefully get more kids into programming. These days, my main area of interest is F*, the new language of the future, in particular its application to the miTLS project.

Previously, I spent a bunch of time at INRIA, where I worked with François designing Mezzo, the (old) language of the future.

My permanent address is My GPG key is available here. Alternatively, gpg --recv 4F7509A0 will do the trick.


🌲 F* / TLS

  • Danel Ahman, Cătălin Hriţcu, Guido Martínez, Gordon Plotkin, Jonathan Protzenko, Aseem Rastogi, Nikhil Swamy. Dijkstra Monads for Free. To appear 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 ]

🌲 Current

  • Sebastian Burckhardt, Jonathan Protzenko. Abstract Specifications for Weakly Consistent Data. IEEE Data Eng. Bull. 39 (1), 45-51, 2016. [ PDF ]
  • Jonathan Protzenko. Functional Pearl: the Proof Search Monad. In Proceedings of the 11th Workshop on the Implementation of Logics (IWIL), 2015 [ 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 homepagetry 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. 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:,,,,,, ]

🌲 Selected talks

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


🌲 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


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