Andrew Appel -

Registered user since Fri 12 Jun 2020

Name:Andrew Appel

Affiliation:Princeton

Personal website:http://www.cs.Princeton.EDU/~appel

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
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
ICFP 2021	Author of Compositional Optimizations for CertiCoq 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
POPL 2020	Committee Member in Program Committee within the Research Papers-track Session Chair of Verified & Secure Compilation (part of Research Papers)
DeepSpec 2018	Author of The Science of Deep Specification within the DeepSpec 2018-track
FMS 2018	Author of Modular Verification of Deep Specifications of Security-Critical Components within the FMS 2018-track
ICFP 2019	Author of Closure Conversion is Safe for Space within the Research Papers-track
CoqPL 2018	Committee Member in Program Committee within the -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
SPLASH 2017	Author of A Verified Messaging System within the OOPSLA-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