Jonathan Protzenko

I am now a post-doc researcher in the RiSE group at Microsoft Research Redmond. I work on TouchDevelop, a.k.a. trying to get kids into programming.

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

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


🌲 Life after Mezzo

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

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

  • François Pottier and Jonathan Protzenko Programming with permissions in Mezzo. ICFP'13. [ PDF ]
    A gentle introduction to the Mezzo language.
  • 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.
  • Thibaut Balabonski, François Pottier, and Jonathan Protzenko. The design and formalization of Mezzo, a permission-based programming language. Submitted for publication, July 2014. [ PDF ]
    A comprehensive reference that covers the surface syntax of the language, the type system, and the latest version of the proof of soundness.
  • Jonathan Protzenko. Mezzo, the language of the future. PhD Dissertation. [ 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 ]

🌲 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

  • Mezzo, the language of the future PhD defense. [ PDF ]
  • The design of Mezzo, a new programming language ICFP'13. [ PDF ]
  • 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


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