Jonathan Protzenko

Registered user since Tue 2 Jun 2015

Name:Jonathan Protzenko
Country:United States
Affiliation:Microsoft Research, Redmond
Research interests:Type systems, programming languages, software verification

Contributions

PriSC 2022 Session Chair of Attacks and defenses (part of PriSC 2022)
Session Chair of Keynote I (part of PriSC 2022)
Co-chair in Program Committee within the PriSC 2022-track
Committee Member in Steering Committee within the PriSC 2022-track
ProLaLa 2022 Session Chair of Long talks #4 (part of ProLaLa Programming Languages and the Law)
Session Chair of Short talks (part of ProLaLa Programming Languages and the Law)
Session Chair of Industry keynote (part of ProLaLa Programming Languages and the Law)
Session Chair of Long talks #3 (part of ProLaLa Programming Languages and the Law)
Program Co-Chair in Program Committee within the ProLaLa Programming Languages and the Law-track
Session Chair of Long talks #1 (part of ProLaLa Programming Languages and the Law)
Session Chair of Long talks #2 (part of ProLaLa Programming Languages and the Law)
Session Chair of Long talks #5 (part of ProLaLa Programming Languages and the Law)
Session Chair of Research keynote (part of ProLaLa Programming Languages and the Law)
ML 2021 PC Chair in Organizing Committee within the ML 2021-track
OCaml 2021 Committee Member in Program Committee within the OCaml 2021-track
POPL 2022 Session Chair of Verification 2 (part of POPL)
PriSC 2021 Committee Member in Program Committee within the PriSC 2021-track
Session Chair of Formal analysis & proof techniques (part of PriSC 2021)
Committee Member in Steering Committee within the PriSC 2021-track
CC 2021 Author of A Modern Compiler for the French Tax Code within the CC Research Papers-track
ML 2020 Committee Member in Program Committee within the ML 2020-track
ICFP 2021 Author of Catala: A Programming Language for the Law within the Research Papers-track
PriSC 2020 Committee 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 2020 Chair of Working Sessions I within the HASE 2020-track
Committee Member in Organizing Committee within the HASE 2020-track
ICFP 2020 Committee Member in Program Committee within the ICFP Program-track
PLDI 2020 Presenter of Verified Programming with Project Everest within the Sponsors-track
ESOP 2019 Author of Meta-F*: Proof Automation with SMT, Tactics, and Metaprograms within the ESOP 2019-track
POPL 2019 Committee Member in Artifact Evaluation Committee within the Artifact Evaluation-track
ML 2018 Author of ML as a Tactic Language, Again within the ML 2018-track
OCaml 2018 Committee Member in Program Committee within the OCaml 2018-track
ICFP 2019 Committee Member in External Review Committee within the Research Papers-track
Session Chair of Lambda-Calculus & Teaching (part of Research Papers)
PriSC 2018 Author of Short Talk: Secure compilation from F* to WebAssembly within the PriSC 2018-track
CPP 2018 Author of A Monadic Framework for Relational Verification: Applied to Information Security, Program Equivalence, and Optimizations within the CPP 2018-track
PLDI 2018 Presenter of Verified Low-Level Programming in F* within the PLDI Tutorials-track
SCM 2017 Presenter of Security preserving compilation of low-level programs embedded in F* within the SCM-track
ICFP 2017 Author of Verified Low-Level Programming Embedded in F* within the Research Papers-track
PLMW Committee Member in Speaker within the PLMW-track
Author of Young Researcher Panel Session within the PLMW-track
Mobile! 2016 Committee Member in Program Committee within the Mobile!-track
ML 2016 Author of Extracting from F* to C: a progress report within the ML-track
POPL 2017 Author of Dijkstra Monads for Free within the POPL-track
PROMOTO 2015 Author of PROMOTO Keynote: The BBC micro:bit within the PROMOTO-track
MobileDeLi 2015 Author of Implementing real-time collaboration in TouchDevelop using AST merges within the MobileDeLi-track
PLOOC 2015 Presenter of Touchdevelop on the BBC’s microbit Going from a blocks programming language to 16kB of RAM within the PLOOC 2015-track
ECOOP 2015 Author of Global Sequence Protocol: A Robust Abstraction for Replicated Shared State within the Research Track-track