Title/Position
Eugene Higgins Professor

Degree
Ph.D., Carnegie-Mellon University, 1985

appel(@cs.princeton.edu) (609) 258-4627 209 Computer Science

Homepage
https://www.cs.princeton.edu/~appel

Other Affiliations
CITP

Research

Interests: Software verification, computer security, programming languages, compilers.
ACM Fellow, 1998. SIGPLAN Distinguished Service Award, 2002.
Research Areas: Policy
Programming Languages / Compilers
Security & Privacy

Active Research Projects: CertiCoq: Principled Optimizing Compilation of Dependently Typed Programs
Verified Software Toolchain

Previous Research Projects: Concurrent C Minor
Foundational Proof-Carrying Code
Proof-Carrying Authorization
Standard ML of New Jersey

Short Bio

Andrew Appel is Eugene Higgins Professor Computer Science, and served from 2009-2015 as Chair of Princeton's CSdepartment. His research is in software verification, computer security, programming languages and compilers, and technology policy. He received his A.B. summa cum laude in physics from Princeton in 1981, and his Ph.D. in computer science from Carnegie Mellon University in 1985. Professor Appel has been editor in chief of ACM Transactions on Programming Languages and Systems and is a fellow of the ACM (Association for Computing Machinery). He has worked on fast N-body algorithms (1980s), Standard ML of New Jersey (1990s), Foundational Proof-Carrying Code (2000s), and the Verified Software Toolchain (2010-present).

Selected Publications

“VST-Floyd: A separation logic tool to verify correctness of C programs”, by Qinxiang Cao, Lennart Beringer, Samuel Gruetter, Josiah Dodds, and Andrew W. Appel. Journal of Automated Reasoning 61(1), pp. 367-422, 2018.
Program Logics for Certified Compilers. Andrew W. Appel et al. Cambridge University Press, 2014.
“Verified Software Toolchain.” Andrew W. Appel. In ESOP 2011: 20th European Symposium on Programming, LNCS 6602, pp. 1-17, March 2011.
“An Indexed Model of Recursive Types for Foundational Proof-Carrying Code.” Andrew W. Appel and David McAllester. ACM Transactions on Programming Languages and Systems 23 (5) 657-683, September 2001.
Modern Compiler Implementation in Java. Andrew W. Appel. Cambridge University Press, 1998.
Compiling with Continuations. Andrew W. Appel. Cambridge University Press, 1992.