Jonathan Protzenko

Registered user since Tue 2 Jun 2015

Name: Jonathan Protzenko

Country: United States

Affiliation: Microsoft Research, Redmond

Personal website:

Research interests: Type systems, programming languages, software verification


ML 2020Committee Member in Program Committee within the ML 2020-track
PriSC 2020Committee Member in Steering Committee within the Principles of Secure Compilation 2020-track
Session Chair of Compartmentalization, memory safety, and isolation (part of Principles of Secure Compilation 2020)
Committee Member in Program Committee within the Principles of Secure Compilation 2020-track
HASE 2020Chair of Working Sessions I within the HASE 2020-track
Committee Member in Organizing Committee within the HASE 2020-track
ICFP 2020Committee Member in Program Committee within the Research Papers-track
PLDI 2020Presenter of Verified Programming with Project Everest within the Sponsors-track
ESOP 2019Author of Meta-F*: Proof Automation with SMT, Tactics, and Metaprograms within the ESOP 2019-track
POPL 2019Committee Member in Artifact Evaluation Committee within the Artifact Evaluation-track
ML 2018Author of ML as a Tactic Language, Again within the ML 2018-track
OCaml 2018Committee Member in Program Committee within the OCaml 2018-track
ICFP 2019Committee Member in External Review Committee within the Research Papers-track
Session Chair of Lambda-Calculus & Teaching (part of Research Papers)
PriSC 2018Author of Short Talk: Secure compilation from F* to WebAssembly within the PriSC 2018-track
CPP 2018Author of A Monadic Framework for Relational Verification: Applied to Information Security, Program Equivalence, and Optimizations within the CPP 2018-track
PLDI 2018Presenter of Verified Low-Level Programming in F* within the PLDI Tutorials-track
SCM 2017Presenter of Security preserving compilation of low-level programs embedded in F* within the SCM-track
ICFP 2017Author of Verified Low-Level Programming Embedded in F* within the Research Papers-track
PLMWCommittee Member in Speaker within the PLMW-track
Author of Young Researcher Panel Session within the PLMW-track
Mobile! 2016Committee Member in Program Committee within the Mobile!-track
ML 2016Author of Extracting from F* to C: a progress report within the ML-track
POPL 2017Author of Dijkstra Monads for Free within the POPL-track
PROMOTO 2015Author of PROMOTO Keynote: The BBC micro:bit within the PROMOTO-track
MobileDeLi 2015Author of Implementing real-time collaboration in TouchDevelop using AST merges within the MobileDeLi-track
PLOOC 2015Presenter of Touchdevelop on the BBC’s microbit Going from a blocks programming language to 16kB of RAM within the PLOOC 2015-track
ECOOP 2015Author of Global Sequence Protocol: A Robust Abstraction for Replicated Shared State within the Research Track-track