Andrew Appel
Research
Interests: Software verification, computer security, programming languages, compilers
ACM Fellow, 1998; SIGPLAN Distinguished Service Award, 2002
Research Areas:
Short Bio
Andrew Appel is Eugene Higgins Professor Computer Science, and served from 2009-2015 as Chair of Princeton's CS department. 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.
