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.
To appear at CPP'18.
[ arXiv ]
-
Jean-Karim Zinzindohoué, Karthikeyan Bhargavan, Jonathan
Protzenko, Benjamin Beurdouche.
HACL*: A Verified Modern Cryptographic Library.
In ACM Conference on Computer and Communications Security
(CCS), 2017.
[ eprint ]
-
Jonathan Protzenko, Jean-Karim Zinzindohoué, Aseem Rastogi, Tahina
Ramananandro, Peng Wang, Santiago Zanella-Béguelin, Antoine
Delignat-Lavaud, Cătălin Hriţcu, Karthikeyan Bhargavan, Cédric
Fournet, and Nikhil Swamy.
Verified Low-Level Programming Embedded in F*.
In Proceedings of the ACM on Programming Languages 1
(ICFP), 2017.
[ 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.
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
- Jonathan Protzenko. Functional Pearl: the Proof Search
Monad. In Proceedings of the 11th Workshop on the
Implementation of Logics (IWIL), 2015 [ PDF ]
This is a neat trick used in the implementation
of the Mezzo type-checker that I extracted and presented in a
standalone manner.
-
Thibaut Balabonski, François Pottier, and Jonathan Protzenko.
Type soundness and race freedom for
Mezzo
In Proceedings of the 12th International Symposium on Functional
and Logic Programming (FLOPS 2014), volume 8475, pages 253-269, June 2014.
[ PDF ]
The submitted journal paper contains more
information about the proof of soundness.
- Jonathan Protzenko. An introduction to Mezzo.
[ Part
1, Part
2 ]
An informal, tutorial-style introduction to
Mezzo on the team's blog.
-
Jonathan Protzenko
The implementation of the Mezzo type-checker.
IFL'13.
[ PDF ]
My PhD dissertation contains better,
more up-to-date information about the implementation.
-
Jonathan Protzenko
Illustrating the Mezzo programming language.
FSFMA'13.
[ PDF ]
-
Jonathan Protzenko and François Pottier.
Programming with permissions: the Mezzo language
(extended abstract).
ML'12.
[ PDF ]
🌲 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
- Verified Embedded Low-Level Programming in
F*, ICFP'17. [ PDF ]
- 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 ]