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 jonathan.protzenko@ens-lyon.org. My GPG key is available here. Alternatively, gpg --recv 4F7509A0 will do the trick.

Research

🌲 F* / TLS

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

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

Teaching

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