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


PriSC 2020Session 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
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