Andrew Appel

Registered user since Fri 12 Jun 2020

Name:Andrew Appel
Affiliation:Princeton

Contributions

CPP 2022 Invited Speaker of Coq’s vibrant ecosystem for verification engineering within the CPP 2022-track
SPLASH 2021 Author of Compositional Optimizations for CertiCoq within the SIGPLAN Papers-track
ICFP 2021 Author of Compositional Optimizations for CertiCoq within the Research Papers-track
CoqPL 2021 Author of The B+-tree Index as a Verified Software Unit within the CoqPL-track
PriSC 2021 Committee Member in Program Committee within the PriSC 2021-track
REMS-DeepSpec 2020 Author of Verified Software Toolchain: a powerful and practical tool within the REMS-DeepSpec 2020-track
ISMM 2020 Author of Verified Sequential Malloc/Free within the ISMM 2020-track
POPL 2020 Committee Member in Program Committee within the Research Papers-track
Session Chair of Verified & Secure Compilation (part of Research Papers)
ICFP 2019 Author of Closure Conversion is Safe for Space within the Research Papers-track
DeepSpec 2019 Presenter of Closure Conversion is Safe for Space within the DeepSpec 2019-track
Session Chair of Interaction Trees and Algebraic Effects I (part of DeepSpec 2019)
Presenter of Abstraction, Subsumption, and Linking in VST within the DeepSpec 2019-track
Presenter of Project Updates from Participating Sites within the DeepSpec 2019-track
FMS 2018 Author of Modular Verification of Deep Specifications of Security-Critical Components within the FMS 2018-track
DeepSpec 2018 Author of The Science of Deep Specification within the DeepSpec 2018-track
CoqPL 2018 Committee Member in Program Committee within the -track
SPLASH 2017 Author of A Verified Messaging System within the OOPSLA-track
DSW 2017 Author of Verifying concurrent C programs with the Verified Software Toolchain within the DSW 2017-track
Session Chair of Intro & industry perspective on crypto (part of DSW 2017)
CoqPL 2017 Author of CertiCoq: A verified compiler for Coq within the CoqPL 2017-track
CoqPL 2016 Author of The Science of Deep Specification within the CoqPL-track
PLDI 2015 Author of Verification of a Cryptographic Primitive: SHA-256 within the Research Papers-track