Semantics-Directed Code Generation. - Andrew W. Appel (POPL, 1985)

A Standard ML compiler. - Andrew W. Appel; David B. MacQueen (FPCA, 1987)

Garbage Collection can be Faster than Stack Allocation. - Andrew W. Appel (Inf. Process. Lett., 1987)

Generalization of the Sethi-Ullman Algorithm for Register Allocation. - Andrew W. Appel; Kenneth J. Supowit (Softw. Pract. Exp., 1987)

Real-time concurrent collection on stock multiprocessors (with retrospective) - Andrew W. Appel (Best of PLDI, 1988)

Real-Time Concurrent Collection on Stock Multiprocessors. - Andrew W. Appel; John R. Ellis; Kai Li 001 (PLDI, 1988)

The World's Fastest Scrabble Program. - Andrew W. Appel; Guy J. Jacobson (Commun. ACM, 1988)

Simulating digital circuits with one bit per wire. - Andrew W. Appel (IEEE Trans. Comput. Aided Des. Integr. Circuits Syst., 1988)

Continuation-Passing, Closure-Passing Style. - Andrew W. Appel; Trevor Jim (POPL, 1989)

Runtime Tags Aren't Necessary. - Andrew W. Appel (LISP Symb. Comput., 1989)

Simple Generational Garbage Collection and Fast Allocation. - Andrew W. Appel (Softw. Pract. Exp., 1989)

Allocation without Locking. - Andrew W. Appel (Softw. Pract. Exp., 1989)

Vectorized garbage collection. - Andrew W. Appel; Aage Bendiksen (J. Supercomput., 1989)

Debugging Standard ML Without Reverse Engineering. - Andrew P. Tolmach; Andrew W. Appel (LISP and Functional Programming, 1990)

An Advisor for Flexible Working Sets. - Rafael Alonso; Andrew W. Appel (SIGMETRICS, 1990)

A Runtime System. - Andrew W. Appel (LISP Symb. Comput., 1990)

Virtual Memory Primitives for User Programs. - Andrew W. Appel; Kai Li 001 (ASPLOS, 1991)

Debuggable Concurrency Extensions for Standard ML. - Andrew P. Tolmach; Andrew W. Appel (Workshop on Parallel and Distributed Debugging, 1991)

Standard ML of New Jersey. - Andrew W. Appel; David B. MacQueen (PLILP, 1991)

Compiling with Continuations - Andrew W. Appel (Cambridge University Press, 1992)

Callee-Save Registers in Continuation-Passing Style. - Andrew W. Appel; Zhong Shao 001 (LISP Symb. Comput., 1992)

Is POPL mathematics or science? - Andrew W. Appel (ACM SIGPLAN Notices, 1992)

Smartest Recompilation. - Zhong Shao 001; Andrew W. Appel (POPL, 1993)

A Critique of Standard ML. - Andrew W. Appel (J. Funct. Program., 1993)

Space-Efficient Closure Representations. - Zhong Shao 001; Andrew W. Appel (LISP and Functional Programming, 1994)

Unrolling Lists. - Zhong Shao 001; John H. Reppy; Andrew W. Appel (LISP and Functional Programming, 1994)

Separate Compilation for Standard ML. - Andrew W. Appel; David B. MacQueen (PLDI, 1994)

Loop Headers in Lambda-Calculus or CPS. - Andrew W. Appel (LISP Symb. Comput., 1994)

Axiomatic Bootstrapping: A Guide for Compiler Hackers. - Andrew W. Appel (ACM Trans. Program. Lang. Syst., 1994)

Cache Performance of Fast-Allocating Programs. - Marcelo J. R. Gonçalves; Andrew W. Appel (FPCA, 1995)

A Type-Based Compiler for Standard ML. - Zhong Shao 001; Andrew W. Appel (PLDI, 1995)

A Debugger for Standard ML. - Andrew P. Tolmach; Andrew W. Appel (J. Funct. Program., 1995)

Empirical and Analytic Study of Stack Versus Heap Cost for Languages with Closures. - Andrew W. Appel; Zhong Shao 001 (J. Funct. Program., 1996)

Intensional Equality ;=) for Continuations. - Andrew W. Appel (ACM SIGPLAN Notices, 1996)

Iterated Register Coalescing. - Lal George; Andrew W. Appel (ACM Trans. Program. Lang. Syst., 1996)

Modern Compiler Implementation in Java: Basic Techniques - Andrew W. Appel (Cambridge University Press, 1997)

Modern Compiler Implementation in C: Basic Techniques - Andrew W. Appel (Cambridge University Press, 1997)

Modern Compiler Implementation in ML: Basic Techniques - Andrew W. Appel (Cambridge University Press, 1997)

The Zephyr Abstract Syntax Description Language. - Daniel C. Wang; Andrew W. Appel; Jeffrey L. Korn; Christopher S. Serra (DSL, 1997)

Lambda-Splitting: A Higher-Order Approach to Cross-Module Optimizations. - Matthias Blume; Andrew W. Appel (ICFP, 1997)

Shrinking lambda Expressions in Linear Time. - Andrew W. Appel; Trevor Jim (J. Funct. Program., 1997)

Modern Compiler Implementation in Java - Andrew W. Appel (Cambridge University Press, 1998)

Modern Compiler Implementation in C - Andrew W. Appel (Cambridge University Press, 1998)

Modern Compiler Implementation in ML - Andrew W. Appel (Cambridge University Press, 1998)

Traversal-Based Visualization of Data Structures. - Jeffrey L. Korn; Andrew W. Appel (INFOVIS, 1998)

SSA is Functional Programming. - Andrew W. Appel (ACM SIGPLAN Notices, 1998)

Proof-Carrying Authentication. - Andrew W. Appel; Edward W. Felten (CCS, 1999)

Lightweight Lemmas in lambda-Prolog. - Andrew W. Appel; Amy P. Felty (ICLP, 1999)

Hierarchical modularity. - Matthias Blume; Andrew W. Appel (ACM Trans. Program. Lang. Syst., 1999)

Machine Instruction Syntax and Semantics in Higher Order Logic. - Neophytos G. Michael; Andrew W. Appel (CADE, 2000)

A Semantic Model of Types and Machine Instructions for Proof-Carrying Code. - Andrew W. Appel; Amy P. Felty (POPL, 2000)

Technological access control interferes with noninfringing scholarship. - Andrew W. Appel; Edward W. Felten (Commun. ACM, 2000)

Efficient and safe-for-space closure conversion. - Zhong Shao 001; Andrew W. Appel (ACM Trans. Program. Lang. Syst., 2000)

SAFKASI: a security mechanism for language-based systems. - Dan S. Wallach; Andrew W. Appel; Edward W. Felten (ACM Trans. Softw. Eng. Methodol., 2000)

Foundational Proof-Carrying Code. - Andrew W. Appel (LICS, 2001)

Optimal Spilling for CISC Machines with Few Registers. - Andrew W. Appel; Lal George (PLDI, 2001)

Type-preserving garbage collectors. - Daniel C. Wang; Andrew W. Appel (POPL, 2001)

An indexed model of recursive types for foundational proof-carrying code. - Andrew W. Appel; David A. McAllester (ACM Trans. Program. Lang. Syst., 2001)

Modern Compiler Implementation in Java, 2nd edition. - Andrew W. Appel; Jens Palsberg (Cambridge University Press, 2002)

A Stratified Semantics of General References A Stratified Semantics of General References. - Amal J. Ahmed 001; Andrew W. Appel; Roberto Virga (LICS, 2002)

Creating and preserving locality of java applications at allocation and garbage collection times. - Yefim Shuf; Manish Gupta 002; Hubertus Franke; Andrew W. Appel; Jaswinder Pal Singh (OOPSLA, 2002)

Access Control on the Web Using Proof-carrying Authorization. - Lujo Bauer; Michael A. Schneider; Edward W. Felten; Andrew W. Appel (DISCEX (2), 2003)

A provably sound TAL for back-end optimization. - Juan Chen; Dinghao Wu; Andrew W. Appel; Hai Fang (PLDI, 2003)

Foundational proof checkers with small witnesses. - Dinghao Wu; Andrew W. Appel; Aaron Stump (PPDP, 2003)

Policy-enforced linking of untrusted components. - Eunyoung Lee; Andrew W. Appel (ESEC / SIGSOFT FSE, 2003)

Using Memory Errors to Attack a Virtual Machine. - Sudhakar Govindavajhala; Andrew W. Appel (S&P, 2003)

A Trustworthy Proof Checker. - Andrew W. Appel; Neophytos G. Michael; Aaron Stump; Roberto Virga (J. Autom. Reason., 2003)

Mechanisms for secure modular programming in Java. - Lujo Bauer; Andrew W. Appel; Edward W. Felten (Softw. Pract. Exp., 2003)

Social processes and proofs of theorems and programs, revisited. - Andrew W. Appel (PLDI, 2004)

Construction of a Semantic Model for a Typed Assembly Language. - Gang Tan; Andrew W. Appel; Kedar N. Swadi; Dinghao Wu (VMCAI, 2004)

Dependent types ensure partial correctness of theorem provers. - Andrew W. Appel; Amy P. Felty (J. Funct. Program., 2004)

Polymorphic Lemmas and Definitions in lambda-Prolog and Twelf. - Andrew W. Appel; Amy P. Felty (Theory Pract. Log. Program., 2004)

MulVAL: A Logic-based Network Security Analyzer. - Xinming Ou; Sudhakar Govindavajhala; Andrew W. Appel (USENIX Security Symposium, 2005)

Compiling with Continuations (corr. version). - Andrew W. Appel (Cambridge University Press, 2006)

Safe Java Native Interface. - Gang Tan; Andrew W. Appel; Srimat Chakradhar; Anand Raghunathan; Srivaths Ravi 001; Daniel C. Wang (ISSSE, 2006)

A Compositional Logic for Control Flow. - Gang Tan; Andrew W. Appel (VMCAI, 2006)

A List-machine Benchmark for Mechanized Metatheory: (Extended Abstract). - Andrew W. Appel; Xavier Leroy (LFMTP@FLoC, 2006)

A very modal model of a modern, major, general type system. - Andrew W. Appel; Paul-André Melliès; Christopher D. Richards; Jérôme Vouillon (POPL, 2007)

Separation Logic for Small-Step cminor. - Andrew W. Appel; Sandrine Blazy (TPHOLs, 2007)

Oracle Semantics for Concurrent Separation Logic. - Aquinas Hobor; Andrew W. Appel; Francesco Zappa Nardelli (ESOP, 2008)

Multimodal Separation Logic for Reasoning About Operational Semantics. - Robert Dockins; Andrew W. Appel; Aquinas Hobor (MFPS, 2008)

A Fresh Look at Separation Algebras and Share Accounting. - Robert Dockins; Aquinas Hobor; Andrew W. Appel (APLAS, 2009)

The New Jersey Voting-machine Lawsuit and the AVC Advantage DRE Voting Machine. - Andrew W. Appel; Maia Ginsburg; Harri Hursti; Brian W. Kernighan; Christopher D. Richards; Gang Tan; Penny Venetis (EVT/WOTE, 2009)

A Logical Mix of Approximation and Separation. - Aquinas Hobor; Robert Dockins; Andrew W. Appel (APLAS, 2010)

Formal Verification of Coalescing Graph-Coloring Register Allocation. - Sandrine Blazy; Benoît Robillard; Andrew W. Appel (ESOP, 2010)

A theory of indirection via approximation. - Aquinas Hobor; Robert Dockins; Andrew W. Appel (POPL, 2010)

Concurrent Separation Logic for Pipelined Parallelization. - Christian J. Bell; Andrew W. Appel; David Walker 001 (SAS, 2010)

Semantic foundations for typed assembly languages. - Amal Ahmed 001; Andrew W. Appel; Christopher D. Richards; Kedar N. Swadi; Gang Tan; Daniel C. Wang (ACM Trans. Program. Lang. Syst., 2010)

VeriSmall: Verified Smallfoot Shape Analysis. - Andrew W. Appel (CPP, 2011)

Verified Software Toolchain - (Invited Talk). - Andrew W. Appel (ESOP, 2011)

Local actions for a curry-style operational semantics. - Gordon Stewart 001; Andrew W. Appel (PLPV, 2011)

Security Seals on Voting Machines: A Case Study. - Andrew W. Appel (ACM Trans. Inf. Syst. Secur., 2011)

Verified heap theorem prover by paramodulation. - Gordon Stewart 001; Lennart Beringer; Andrew W. Appel (ICFP, 2012)

Verified Software Toolchain. - Andrew W. Appel (NASA Formal Methods, 2012)

A Certificate Infrastructure for Machine-Checked Proofs of Conditional Information Flow. - Torben Amtoft; Josiah Dodds; Zhi Zhang; Andrew W. Appel; Lennart Beringer; John Hatcliff; Xinming Ou; Andrew Cousino (POST, 2012)

A List-Machine Benchmark for Mechanized Metatheory. - Andrew W. Appel; Robert Dockins; Xavier Leroy (J. Autom. Reason., 2012)

Mostly Sound Type System Improves a Foundational Program Verifier. - Josiah Dodds; Andrew W. Appel (CPP, 2013)

Program Logics - for Certified Compilers. - Andrew W. Appel (Cambridge University Press, 2014)

Portable Software Fault Isolation. - Joshua A. Kroll; Gordon Stewart 001; Andrew W. Appel (CSF, 2014)

Verified Compilation for Shared-Memory C. - Lennart Beringer; Gordon Stewart 001; Robert Dockins; Andrew W. Appel (ESOP, 2014)

Verification of a cryptographic primitive: SHA-256 (abstract). - Andrew W. Appel (PLDI, 2015)

Compositional CompCert. - Gordon Stewart 001; Lennart Beringer; Santiago Cuéllar; Andrew W. Appel (POPL, 2015)

Verified Correctness and Security of OpenSSL HMAC. - Lennart Beringer; Adam Petcher; Katherine Q. Ye; Andrew W. Appel (USENIX Security Symposium, 2015)

Verification of a Cryptographic Primitive: SHA-256. - Andrew W. Appel (ACM Trans. Program. Lang. Syst., 2015)

Modular Verification for Computer Security. - Andrew W. Appel (CSF, 2016)

Bringing Order to the Separation Logic Jungle. - Qinxiang Cao; Santiago Cuéllar; Andrew W. Appel (APLAS, 2017)

Verified Correctness and Security of mbedTLS HMAC-DRBG. - Katherine Q. Ye; Matthew Green 001; Naphat Sanguansin; Lennart Beringer; Adam Petcher; Andrew W. Appel (CCS, 2017)

Shrink fast correctly! - Olivier Savary Bélanger; Andrew W. Appel (PPDP, 2017)

A verified messaging system. - William Mansky; Andrew W. Appel; Aleksey Nogin (Proc. ACM Program. Lang., 2017)

VST-Floyd: A Separation Logic Tool to Verify Correctness of C Programs. - Qinxiang Cao; Lennart Beringer; Samuel Gruetter; Josiah Dodds; Andrew W. Appel (J. Autom. Reason., 2018)

Technical Perspective: The scalability of CertiKOS. - Andrew W. Appel (Commun. ACM, 2019)

Proof Pearl: Magic Wand as Frame. - Qinxiang Cao; Shengyi Wang; Aquinas Hobor; Andrew W. Appel (CoRR, 2019)

Closure conversion is safe for space. - Zoe Paraskevopoulou; Andrew W. Appel (Proc. ACM Program. Lang., 2019)

Connecting Higher-Order Separation Logic to a First-Order Outside World. - William Mansky; Wolf Honoré; Andrew W. Appel (ESOP, 2020)

Verified sequential Malloc/Free. - Andrew W. Appel; David A. Naumann (ISMM, 2020)

C floating-point proofs layered with VST and Flocq. - Andrew W. Appel; Yves Bertot (J. Formaliz. Reason., 2020)

Corrigendum: C floating-point proofs layered with VST and Flocq. - Andrew W. Appel; Yves Bertot (J. Formaliz. Reason., 2020)

Abstraction and subsumption in modular verification of C programs. - Lennart Beringer; Andrew W. Appel (Formal Methods Syst. Des., 2021)

Deriving efficient program transformations from rewrite rules. - John M. Li; Andrew W. Appel (Proc. ACM Program. Lang., 2021)

Compositional optimizations for CertiCoq. - Zoe Paraskevopoulou; John M. Li; Andrew W. Appel (Proc. ACM Program. Lang., 2021)

Verified Erasure Correction in Coq with MathComp and VST. - Joshua M. Cohen; Qinshi Wang; Andrew W. Appel (CAV (2), 2022)

Verified Numerical Methods for Ordinary Differential Equations. - Ariel E. Kellison; Andrew W. Appel (NSV/FoMLAS@CAV, 2022)

Coq's vibrant ecosystem for verification engineering (invited talk). - Andrew W. Appel (CPP, 2022)

LAProof: A Library of Formal Proofs of Accuracy and Correctness for Linear Algebra Programs. - Ariel E. Kellison; Andrew W. Appel; Mohit Tekriwal; David Bindel (ARITH, 2023)

Foundational Verification of Stateful P4 Packet Processing. - Qinshi Wang; Mengying Pan; Shengyi Wang; Ryan Doenges; Lennart Beringer; Andrew W. Appel (ITP, 2023)

Verified Correctness, Accuracy, and Convergence of a Stationary Iterative Linear Solver: Jacobi Method. - Mohit Tekriwal; Andrew W. Appel; Ariel E. Kellison; David Bindel; Jean-Baptiste Jeannin (CICM, 2023)

Specifying and Verifying a Real-World Packet Error-Correction System. - Joshua M. Cohen; Andrew W. Appel (VSTTE, 2023)

A Solver for Arrays with Concatenation. - Qinshi Wang; Andrew W. Appel (J. Autom. Reason., 2023)

Efficient Extensional Binary Tries. - Andrew W. Appel; Xavier Leroy (J. Autom. Reason., 2023)

VCFloat2: Floating-Point Error Analysis in Coq. - Andrew W. Appel; Ariel Kellison (CPP, 2024)

An Internet Voting System Fatally Flawed in Creative New Ways. - Andrew W. Appel; Philip B. Stark (CoRR, 2024)

Comprehensive Verification of Packet Processing. - Shengyi Wang; Mengying Pan; Andrew W. Appel (CoRR, 2024)

VST-A: A Foundationally Sound Annotation Verifier. - Litao Zhou; Jianxing Qin; Qinshi Wang; Andrew W. Appel; Qinxiang Cao (Proc. ACM Program. Lang., 2024)

A Verified Foreign Function Interface between Coq and C. - Joomy Korkut; Kathrin Stark; Andrew W. Appel (Proc. ACM Program. Lang., 2025)