Research papers

• A Verified Foreign Function Interface between Coq and C, by Joomy Korkut, Kathrin Stark, and Andrew W. Appel. Proc. ACM Program. Lang. 9, POPL, Article 24 (January 2025), 31 pages. [local copy]
• An Internet Voting System Fatally Flawed in Creative New Ways, by Andrew W. Appel and Philip B. Stark, arXiv:2411.11796, 10 pages, November 2024.
• VST-A: A Foundationally Sound Annotation Verifier, by Litao Zhou, Jianxing Qin, Qinshi Wang, Andrew W. Appel, and Qinxiang Cao, Proceedings of the ACM on Programming Languages volume 8, No. POPL, January 2024. [local copy]
• VCFloat2: Floating-point Error Analysis in Coq, by Andrew W. Appel and Ariel E. Kellison, in CPP'24: ACM SIGPLAN International Conference on Certified Programs and Proofs, January 2024. [local copy]
• Specifying and Verifying a Real-World Packet Error-Correction System, by Joshua M. Cohen and Andrew W. Appel, in VSTTE'23, 15th International Conference on Verified Software: Theories, Tools, and Experiments, October 23, 2023. Springer LNCS vol 14095, July 2024. [local copy]
• VSTlib: Library Components for Verified C Programs, by Andrew W. Appel, Coq Workshop 2023, July 2023.
• 24 for '24: Urgent Recommendations in Law, Media, Politics, and Tech for Fair and Legitimate 2024 U.S. Elections, by the Ad Hoc Committee for 2024 Election Fairness and Legitimacy (Appel, Azari, Cain, et al.), edited by Richard L. Hasen, UCLA Law School, September 2023.
• LAProof: a library of formal accuracy and correctness proofs for sparse linear algebra programs, by Ariel E. Kellison, Andrew W. Appel, Mohit Tekriwal, and David Bindel, 30th IEEE International Symposium on Computer Arithmetic, September 2023.
• Verified correctness, accuracy, and convergence of a stationary iterative linear solver: Jacobi method, by Mohit Tekriwal, Andrew W. Appel, Ariel E. Kellison, David Bindel, and Jean-Baptiste Jeannin. In 16th Conference on Intelligent Computer Mathematics, pp. 206-221, September 2023.
• Foundational verification of stateful P4 packet processing, by Qinshi Wang, Mengying Pan, Shengyi Wang, Ryan Doenges, Lennart Beringer and Andrew W. Appel, In ITP'23: Fourteenth International Conference on Interactive Theorem Proving, August 2023.
• A Solver for Arrays with Concatenation, by Qinshi Wang and Andrew W. Appel, Journal of Automated Reasoning vol. 67, no. 1, article 4, January 2023. (local copy)
• Efficient Extensional Binary Tries, by Andrew W. Appel and Xavier Leroy, Journal of Automated Reasoning vol. 67, no. 1, article 8, January 2023. (arXiv copy)
• Is Internet Voting Trustworthy? The Science and the Policy Battles, by Andrew W. Appel, University of New Hampshire Law Review, 21 U.N.H. L. Rev. 523 (2023). (earlier draft on SSRN)
• Verified Numerical Methods for Ordinary Differential Equations, by Ariel E. Kellison and Andrew W. Appel, in NSV'22: 15th International Workshop on Numerical Software Verification, Springer LNCS 13466, doi:10.1007/978-3-031-21222-2_9, pp. 147-163, August 2022.
• Verified Erasure Correction in Coq with MathComp and VST, by Joshua M. Cohen, Qinshi Wang, and Andrew W. Appel, in CAV'22: 34th International Conference on Computer Aided Verification, August 2022.
• Coq's Vibrant Ecosystem for Verification Engineering, by Andrew W. Appel, in CPP'22: Proceedings of the 11th ACM SIGPLAN International Conference on Certified Programs and Proofs, pages 2-11, January 2022. DOI 10.1145/3497775.3503951
• Deriving Efficient Program Transformations from Rewrite Rules, by John M. Li and Andrew W. Appel, Proc. ACM Program. Lang. Vol. 5, No. ICFP, Article 74 (29 pages), August 2021. DOI 10.1145/3473579
• Compositional Optimizations for CertiCoq, by Zoe Paraskevopoulou, John M. Li, and Andrew W. Appel, Proc. ACM Program. Lang. Vol. 5, No. ICFP, Article 86 (30 pages), August 2021. DOI 10.1145/3473591
• Verifiable C, by Andrew W. Appel, Lennart Beringer, and Qinxiang Cao, 2021. Volume 5 of Software Foundations, edited by B. C. Pierce.
• Abstraction and Subsumption in Modular Verification of C Programs, by Lennart Beringer and Andrew W. Appel, in Formal Methods in System Design, DOI 10.1007/s10703-020-00353-1, March 2021. (local copy) This is a revised and extended version of Abstraction and Subsumption in Modular Verification of C Programs, in FM2019: 23rd International Symposium on Formal Methods, October 2019.
• C-language floating-point proofs layered with VST and Flocq, by Andrew W. Appel and Yves Bertot, Journal of Formalized Reasoning 13(1), December 2020. DOI 10.6092/issn.1972-5787/11442
• Compiler Correctness for Concurrency: from concurrent separation logic to shared-memory assembly language, by Santiago Cuellar, Nick Giannarakis, Jean-Marie Madiot, William Mansky, Lennart Beringer, Qinxiang Cao, and Andrew W. Appel, Technical report TR-014-19, Department of Computer Science, Princeton University, March 2020.
• Evidence-Based Elections: Create a Meaningful Paper Trail, then Audit, by Andrew W. Appel and Philip B. Stark, Georgetown Law Technology Review, volume 4, pages 523-541, 2020.
• Fair Elections During a Crisis: Urgent Recommendations in Law, Media, Politics, and Tech to Advance the Legitimacy of, and the Public Confidence in, the November 2020 U.S. Elections,by the Ad Hoc Committee for 2020 Election Fairness and Legitimacy (Appel, Azari, Cain, et al.), edited by Richard L. Hasen, UCI Law School, April 2020.
• Verified sequential malloc/free, by Andrew W. Appel and David A. Naumann, in 2020 ACM SIGPLAN International Symposium on Memory Management, June 2020.
• Ballot-Marking Devices Cannot Assure the Will of the Voters, by Andrew W. Appel, Richard A. DeMillo, and Philip B. Stark. Election Law Journal, vol. 19 no. 3, pp. 432-450, September 2020. (Non-paywall version, differs in formatting and pagination; earlier versions appeared on SSRN.)
• Connecting Higher-Order Separation Logic to a First-Order Outside World, by William Mansky, Wolf Honoré, and Andrew W. Appel, ESOP 2020: European Symposium on Programming, April 2020.
• Certified Code Generation from CPS to C, by Olivier Savary Belanger, Matthew Z. Weaver, and Andrew W. Appel, October 2019.
• Closure Conversion is Safe for Space, by Zoe Paraskevopoulou and Andrew W. Appel. Proceedings of the ACM on Programming Languages, vol. 3, no. ICFP, article 83, 29 pages, doi 10.1145/3341687, August 2019.
• Securing the Vote: Protecting American Democracy, by National Academies of Science, Engineering, and Medicine: Lee C. Bollinger, Michael A. McRobbie, Andrew W. Appel, Josh Benaloh, Karen Cook, Dana DeBeauvoir, Moon Duchin, Juan E. Gilbert, Susan L. Graham, Neal Kelley, Kevin J. Kennedy, Nathaniel Persily, Ronald L. Rivest, Charles Stewart III. September 2018.
• Proof pearl: Magic wand as frame, by Qinxiang Cao, Shengyi Wang, Aquinas Hobor, and Andrew W. Appel, February 2018.
• 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. (Local copy)
• A verified messaging system, by William Mansky, Andrew W. Appel, and Aleksey Nogin. OOPSLA'17: ACM Conference on Object-Oriented Programming Systems, Languages, and Applications, October 2017. Proceedings of the ACM on Programming Languages (PACM/PL) volume 1, issue OOPSLA, paper 87, 2017.
• Position paper: the science of deep specification, by Andrew W. Appel, Lennart Beringer, Adam Chlipala, Benjamin C. Pierce, Zhong Shao, Stephanie Weirich and Steve Zdancewic, Philosophical Transactions of the Royal Society A 375:21060331 (24 pages), 2017.
• Bringing order to the separation logic jungle, by Qinxiang Cao, Santiago Cuellar, and Andrew W. Appel. APLAS'17: 15th Asian Symposium on Programming Languages and Systems, November 2017.
• Verified Correctness and Security of mbedTLS HMAC-DRBG by Katherine Q. Ye, Matthew Green, Naphat Sanguansin, Lennart Beringer, Adam Petcher, and Andrew W. Appel. CCS'17: ACM Conference on Computer and Communications Security, October 2017.
• Shrink Fast Correctly! by Olivier Savary Belanger and Andrew W. Appel. Proceedings of International Symposium on Principles and Practice of Declarative Programming (PPDP'17), pages 49-60, ACM Press, October 2017 (PPDP’17).
• CertiCoq: A verified compiler for Coq, by Abhishek Anand, Andrew Appel, Greg Morrisett, Zoe Paraskevopoulou, Randy Pollack, Olivier Savary Belanger, Matthieu Sozeau, and Matthew Weaver. In CoqPL'17: The Third International Workshop on Coq for Programming Languages, January 2017.
• Verified Functional Algorithms, by Andrew W. Appel, 2017. Volume 3 of Software Foundations, edited by B. C. Pierce.
• Modular Verification for Computer Security, by Andrew W. Appel. In CSF 2016: 29th IEEE Computer Security Foundations Symposium, June 2016.
• Verified Correctness and Security of OpenSSL HMAC, by Lennart Beringer, Adam Petcher, Katherine Q. Ye, and Andrew W. Appel. In 24th USENIX Security Symposium, pages 207-221, August 2015.
• Compositional CompCert, by Gordon Stewart, Lennart Beringer, Santiago Cuellar, and Andrew W. Appel. POPL 2015: The 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 275-287, January 2015. (local copy)
• Second Edition: Verification of a Cryptographic Primitive: SHA-256. This is a very minor revision (as explained in its abstract) of Verification of a Cryptographic Primitive: SHA-256, by Andrew W. Appel, ACM Transactions on Programming Languages and Systems 37(2) 7:1-7:31, April 2015.
  
• Portable Software Fault Isolation, by Joshua A. Kroll, Gordon Stewart, and Andrew W. Appel. CSF'14: Computer Security Foundations Symposium, IEEE Press, July 2014.
• Program Logics for Certified Compilers, by Andrew W. Appel with Robert Dockins, Aquinas Hobor, Lennart Beringer, Josiah Dodds, Gordon Stewart, Sandrine Blazy, and Xavier Leroy. Cambridge University Press, 2014.
• Verified Compilation for Shared-memory C, by Lennart Beringer, Gordon Stewart, Robert Dockins, and Andrew W. Appel. 23rd European Symposium on Programming (ESOP'14), April 2014.
• Mostly Sound Type System Improves a Foundational Program Verifier, by Josiah Dodds and Andrew W. Appel. 3rd International Conference on Certified Programs and Proofs (CPP 2013), December 2013.
• Research Needs for Secure, Trustworthy, and Reliable Semiconductors, by Andrew Appel, Chris Daverse, Kenneth Hines, Rafic Makki, Keith Marzullo, Celia Merzbacher, Ron Perez, Fred Schneider, Mani Soma, and Yervant Zorian. Final workshop report of the NSF/CCC/SRC workshop on Convergence of Software Assurance Methodologies and Trustworthy Semiconductor Design and Manufacture, 2013. local copy
• The CompCert Memory Model, Version 2, by Xavier Leroy, Andrew W. Appel, Sandrine Blazy, and Gordon Stewart. INRIA Research Report RR-7987, June 2012.
• A Certificate Infrastructure for Machine-Checked Proofs of Conditional Information Flow, by Torben Amtoft, Josiah Dodds, Zhi Zhang, Andrew Appel, Lennart Beringer, John Hatcliff, Xinming Ou and Andrew Cousino. First Conference on Principles of Security and Trust (POST 2012), LNCS 7215, pp. 369-389, March 2012.
• Verified Heap Theorem Prover by Paramodulation, by Gordon Stewart, Lennart Beringer, and Andrew W. Appel. In ICFP 2012: The 17th ACM SIGPLAN International Conference on Functional Programming, pp. 3-14, September 2012.
• The Birth of Computer Science at Princeton in the 1930s, by Andrew W. Appel. Introduction to Alan Turing's Systems of Logic: The Princeton Thesis, edited and introduced by Andrew W. Appel, Princeton University Press, 2012.
• Efficient Verified Red-Black Trees, by Andrew W. Appel, September 2011.
• VeriSmall: Verified Smallfoot Shape Analysis, by Andrew W. Appel. In CPP 2011: First International Conference on Certified Programs and Proofs, Springer LNCS 7086, pp. 231-246, December 2011.
• Verified Software Toolchain, by Andrew W. Appel. In ESOP 2011: 20th European Symposium on Programming, LNCS 6602, pp. 1-17, March 2011.
• A list-machine benchmark for mechanized metatheory by Andrew W. Appel, Robert Dockins, and Xavier Leroy. Journal of Automated Reasoning, 49(3):453-491, 2012. DOI 10.1007/s10817-011-9226-1 Earlier versions: A list-machine benchmark for mechanized metatheory by Andrew W. Appel and Xavier Leroy. INRIA Research Report RR-5914, May 2006. A shorter version appeared in LFMTP'06: International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice, August 2006.
• Security Seals on Voting Machines: A Case Study, by Andrew W. Appel. ACM Transactions on Information and System Security (TISSEC) 14, 2, pages 18:1--18:29, September 2011. [local copy]
• Local Actions for a Curry-style Operational Semantics by Gordon Stewart and Andrew W. Appel. In PLPV'11: 5th ACM SIGPLAN Workshop on Programming Languages meets Program Verification, January 29, 2011. [local copy]
• Concurrent Separation Logic for Pipelined Parallelization, by Christian J. Bell, Andrew W. Appel, and David Walker. In SAS 2010: 17th Annual Static Analysis Symposium, September 2010.
• A Logical Mix of Approximation and Separation by Aquinas Hobor, Robert Dockins, and Andrew W. Appel. In APLAS 2010: 8th ASIAN Symposium on Programming Languages and Systems, November 2010.
• Formal Verification of Coalescing Graph-Coloring Register Allocation, by Sandrine Blazy, Benoit Robillard, and Andrew W. Appel. In ESOP 2010: 19th European Symposium on Programming, pp. 145-164, March 2010.
• A Theory of Indirection via Approximation, by Aquinas Hobor, Robert Dockins, and Andrew W. Appel. In POPL 2010: The 37th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 171-184, January 2010. [local copy]
• A Fresh Look at Separation Algebras and Share Accounting by Robert Dockins, Aquinas Hobor, and Andrew W. Appel. In Seventh Asian Symposium on Programming Languages and Systems (APLAS 2009), December 2009.
• The New Jersey Voting-machine Lawsuit and the AVC Advantage DRE Voting Machine, by Andrew W. Appel, Maia Ginsburg, Harri Hursti, Brian W. Kernighan, Christopher D. Richards, Gang Tan, and Penny Venetis. EVT/WOTE'09, Electronic Voting Technology Workshop / Workshop on Trustworthy Elections, August 2009.
• Semantic Foundations for Typed Assembly Languages, by A. Ahmed, A. W. Appel, C. D. Richards, K. Swadi, G. Tan, and D. C. Wang. ACM Transactions on Programming Languages and Systems, 32(3):7.1-7.67, March 2010. [local copy]
• Insecurities and Inaccuracies of the Sequoia AVC Advantage 9.00H DRE Voting Machine, by Andrew W. Appel, Maia Ginsburg, Harri Hursti, Brian W. Kernighan, Christopher D. Richards, and Gang Tan. October 2008.
• Multimodal Separation Logic for Reasoning About Operational Semantics, by Robert Dockins, Andrew W. Appel, and Aquinas Hobor, in Twenty-fourth Conference on the Mathematical Foundations of Programming Semantics, May 2008; Electronic Notes in Theoretical Computer Science, vol 218, 22 October 2008, pp. 5-20.
• Foundational High-level Static Analysis, by Andrew W. Appel. In CAV 2008 Workshop on Exploiting Concurrency Efficiently and Correctly, July 2008.
• Oracle Semantics for Concurrent Separation Logic by Aquinas Hobor, Andrew W. Appel, and Francesco Zappa Nardelli. European Symposium on Programming (ESOP), April 2008. Extended version with appendix.
• Separation Logic for Small-step C minor, by Andrew W. Appel and Sandrine Blazy, in TPHOLs 2007: 20th International Conference on Theorem Proving in Higher-Order Logics, pp. 5-21, September 2007.
• Effective Audit Policy for Voter-Verified Paper Ballots, by Andrew W. Appel. Presented at 2007 Annual Meeting of the American Political Science Association, Chicago, September 1, 2007. Earlier version: Effective Audit Policy for Voter-Verified Paper Ballots in New Jersey, March 9, 2007.
• A Very Modal Model of a Modern, Major, General Type System, by Andrew W. Appel, Paul-Andre Mellies, Christopher D. Richards, and Jerome Vouillon. POPL 2007: The 34th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, January 2007. [local copy]
• Ceci n'est pas une urne: On the Internet vote for the Assemblée des Français de l'Etranger, by Andrew W. Appel, June 2006.
• Safe Java Native Interface, by Gang Tan, Andrew W. Appel, Srimat Chakradhar, Anand Raghunathan, Srivaths Ravi, and Daniel Wang. International Symposium on Secure Software Engineering, March 2006.
• Tactics for Separation Logic, by Andrew W. Appel, January 2006.
• Windows Access Control Demystified, by Sudhakar Govindavajhala and Andrew W. Appel, January 2006.
• A Compositional Logic for Control Flow by Gang Tan and Andrew W. Appel. In 7th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI), January 2006.
• MulVAL: A Logic-based Network Security Analyzer by Xinming Ou, Sudhakar Govindavajhala, and Andrew W. Appel. In 14th Usenix Security Symposium, August 2005. Older version: Network Security Management with High-level Security Policies, September 2004
• Social processes and proofs of theorems and programs, revisited. Andrew W. Appel, PLDI '04: Proceedings of the ACM SIGPLAN 2004 conference on Programming language design and implementation, 2004
• Retrospective: Real-time concurrent collection on stock multiprocessors. Andrew W. Appel, ACM SIGPLAN Notices - Best of PLDI 1979-1999, 2004
• Construction of a Semantic Model for a Typed Assembly Language, by Gang Tan, Andrew W. Appel, Kedar N. Swadi, and Dinghao Wu. In 5th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI '04),, January 2004.
• Policy-Enforced Linking of Untrusted Components (Extended Abstract), by Eunyoung Lee and Andrew W. Appel. European Software Engineering Conference and ACM SIGSOFT Symposium on the Foundations of Software Engineering, pp. 371-374, September 2003.
• Foundational Proof Checkers with Small Witnesses, by Dinghao Wu, Andrew W. Appel, and Aaron Stump. 5th ACM-SIGPLAN International Conference on Principles and Practice of Declarative Programming, pp. 264-274, August 2003. [local copy]
• A Provably Sound TAL for Back-end Optimization by Juan Chen, Dinghao Wu, Andrew W. Appel, and Hai Fang. PLDI 2003: ACM SIGPLAN Conference on Programming Language Design and Implementation, pp. 208-219, June 2003. [local copy]
• Using Memory Errors to Attack a Virtual Machine by Sudhakar Govindavajhala and Andrew W. Appel, 2003 IEEE Symposium on Security and Privacy, pp. 154-165, May 2003.
• A Kind System for Typed Machine Language, by Andrew W. Appel, Christopher D. Richards, and Kedar N. Swadi. Princeton University, October 2002.
• An Indexed Model of Impredicative Polymorphism and Mutable References, by Amal Ahmed, Andrew W. Appel, and Roberto Virga. Princeton University, January 2003.
• Secure Linking: a Framework for Trusted Software Components, by Eunyoung Lee and Andrew W. Appel. Princeton University CS TR-662-02, September 2002. Extended Version, CS TR-663-02, September 2002.
• Mechanisms for secure modular programming in Java, by Lujo Bauer, Andrew W. Appel, and Edward W. Felten. Software--Practice and Experience 33:461-480, 2003. Previous version.
• Deobfuscation is in NP, by Andrew W. Appel. Princeton University, August 2002.
• Polymorphic Lemmas and Definitions in Lambda Prolog and Twelf, by Andrew W. Appel and Amy P. Felty. Theory and Practice of Logic Programming 4 (1) 1-39, January 2004.
• Dependent Types Ensure Partial Correctness of Theorem Provers, by Andrew W. Appel and Amy P. Felty. Journal of Functional Programming 14(1):3-19, January 2004.
• Creating and Preserving Locality of Java Applications at Allocation and Garbage Collection Times, by Yefim Shuf, Manish Gupta, Hubertus Franke, Andrew W. Appel, and Jaswinder Pal Singh. 17th Annual ACM Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA 2002), SIGPLAN Notices 37(11) pp. 13-25, November 2002.
• A Stratified Semantics of General References Embeddable in Higher-Order Logic, by Amal J. Ahmed, Andrew W. Appel, and Roberto Virga. 17th Annual IEEE Symposium on Logic in Computer Science (LICS 2002), pp. 75-86, June 2002. (Preliminary version of July 2001.)
• A Trustworthy Proof Checker, by Andrew W. Appel, Neophytos G. Michael, Aaron Stump, and Roberto Virga. Journal of Automated Reasoning 31:231-260, 2003. Previous version appeared in Verification Workshop - VERIFY 2002 and (jointly) in Foundations of Computer Security - FCS 2002 Copenhagen, Denmark, July 25-26, 2002.
• JVM TCB: Measurements of the Trusted Computing Base of Java Virtual Machines, by Andrew W. Appel and Daniel C. Wang. Princeton University CS TR-647-02, April 2002.
• Typed Machine Language and its Semantics, by Kedar N. Swadi and Andrew W. Appel, preliminary version of July 2001.
• Foundational Proof-Carrying Code. Andrew W. Appel, in 16th Annual IEEE Symposium on Logic in Computer Science (LICS '01), pp. 247-258, June 2001.
• Optimal Spilling for CISC Machines with Few Registers, by Andrew W. Appel and Lal George. In PLDI'01: ACM SIGPLAN 2001 Conference on Programming Language Design and Implementation, pages 243-253, May 2001.
• Dictionary Passing for Polytypic Polymorphism. Juan Chen and Andrew W. Appel. Princeton University Computer Science TR-635-01, March 2001.
• Models for Security Policies in Proof-Carrying Code. Andrew W. Appel and Edward W. Felten, Princeton University Computer Science TR-636-01, March 2001.
• Type-preserving garbage collectors by Daniel C. Wang and Andrew W. Appel, Proceedings of the 28th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 166-178, January 2001. [local copy]
• Hints on Proving Theorems in Twelf. Andrew W. Appel, Princeton University, February 2000.
• 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.
• SAFKASI: A Security Mechanism for Language-Based Systems, Dan S. Wallach, Andrew W. Appel, and Edward W. Felten. ACM Transactions on Software Engineering and Methodology, 9 (4) 341-378, October 2000.
• Efficient and Safe-for-Space Closure Conversion, Zhong Shao and Andrew W. Appel, ACM Trans. on Prog. Lang. and Systems 22(1) 129-161, January 2000.
• Machine Instruction Syntax and Semantics in Higher Order Logic. Neophytos G. Michael and Andrew W. Appel. 17th International Conference on Automated Deduction (CADE-17), pp. 7-24, Springer-Verlag (Lecture Notes in Artificial Intelligence), June 2000.
• Technological Access Control Interferes with Noninfringing Scholarship. Andrew W. Appel and Edward W. Felten. Communications of the ACM 43 (9) 21-23, September 2000. [local copy]
• Protection against untrusted code. Andrew W. Appel. IBM Developer Works, September 1999.
• Hierarchical Modularity. Matthias Blume and Andrew W. Appel, ACM Transactions on Programming Languages and Systems, 21 (4) 812-846, July 1999.
• A Semantic Model of Types and Machine Instructions for Proof-Carrying Code, Andrew W. Appel and Amy P. Felty. 27th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL '00), pp. 243-253, January 2000. [local copy]
• Lightweight Lemmas in Lambda Prolog, Andrew W. Appel and Amy P. Felty, in 16th International Conference on Logic Programming, November 1999.
• Proof-Carrying Authentication. Andrew W. Appel and Edward W. Felten, 6th ACM Conference on Computer and Communications Security, November 1999. [local copy]
• Traversal-based Visualization of Data Structures. Jeffrey L. Korn and Andrew W. Appel, IEEE Symposium on Information Visualization (InfoVis '98), pp. 11-18, October 1998.
• A comparison of C, ML, Java on a realistic benchmark, Andrew W. Appel, September 25, 1998.
• SSA is Functional Programming. Andrew W. Appel, ACM SIGPLAN Notices v. 33, no. 4, pp. 17-20, April 1998. [local copy]
• The Zephyr Abstract Syntax Description Language. Daniel C. Wang, Andrew W. Appel, Jeff L. Korn, and Christopher S. Serra. Conference on Domain-Specific Languages, USENIX Association, October 1997.
• Lambda-Splitting: A Higher-Order Approach to Cross-Module Optimizations. Matthias Blume and Andrew W. Appel, Proc. ACM SIGPLAN International Conference on Functional Programming (ICFP '97), pp. 112-124, June 1997.
• Shrinking Lambda Expressions in Linear Time. Andrew W. Appel and Trevor Jim, Princeton University, 1997. Journal of Functional Programming v. 7 no. 5, pp. 515-540, 1997. (Revision of a previous paper, Making Lambda-Calculus Smaller, Faster)
• Modern Compiler Implementation in Java
  Modern Compiler Implementation in ML
  Modern Compiler Implementation in C
  Andrew W. Appel, Cambridge University Press, 1998.
• Book Review of Garbage Collection: Algorithms for Automatic Dynamic Memory Management by Richard Jones and Rafael Lins. Andrew W. Appel. Journal of Functional Programming 7(2), pp. 227-229, March 1997.
• Security and document compatibility for electronic refereeing. Andrew W. Appel. CBE Views 20(1), 1997, published by the Council of Biology Editors.
• Intensional Equality ;=) for Continuations. Andrew W. Appel. ACM SIGPLAN Notices 31 (2), pp. 55-57, February 1996. [local copy]
• Iterated Register Coalescing. Lal George and Andrew W. Appel. ACM Transactions on Programming Languages and Systems 18(3) 300-324, May 1996. Shorter version appeared in 23rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, January 1996. DATA
• How to Edit a Journal by E-mail. Andrew W. Appel. Journal of Scholarly Publishing, vol. 27, no. 2, pp. 82-99, January 1996.
• Cache Performance of Fast-Allocating Programs. Marcelo J. R. Goncalves and Andrew W. Appel. Proc. Seventh Int'l Conf. on Functional Programming and Computer Architecture, pp. 293-305, ACM Press, June 1995. ©1995 ACM. [local copy]
• A Type-Based Compiler for Standard ML. Zhong Shao and Andrew W. Appel. Proc. 1995 ACM Conf. on Programming Language Design and Implementation, (ACM SIGPLAN Notices vol. 30, number 6), pp. 116-129, June 1995. [local copy]
• Hot-sliding in ML. Andrew W. Appel. Princeton University, December 1994.
• Loop Headers in Lambda-calculus or CPS. Andrew W. Appel. Lisp and Symbolic Computation 7, 337-343, 1994.
• Emulating Write-Allocate on a No-Write-Allocate Cache. Andrew W. Appel. CS-TR-459-94, Princeton University, June 20, 1994.
• Empirical and Analytic Study of Stack versus Heap Cost for Languages with Closures. Journal of Functional Programming 6 (1) 47-74, 1996.
• Axiomatic Bootstrapping: A guide for compiler hackers, Andrew W. Appel, ACM Transactions on Programming Languages and Systems, vol. 16, number 6, pp. 1699-1718, November 1994. Older version without diagrams, in ACM SIGPLAN Workshop on ML and its Applications, Orlando, Florida, June 25, 1994.
• A Debugger for Standard ML. Andrew Tolmach and Andrew W. Appel. Journal of Functional Programming, vol. 5, number 2, pp. 155-200, April 1995.
• Unrolling Lists. Zhong Shao, John H. Reppy, and Andrew W. Appel. Proc. 1994 ACM Conf. on Lisp and Functional Programming, June 1994. [local copy]
• Space-Efficient Closure Representations. Zhong Shao and Andrew W. Appel. Proc. 1994 ACM Conf. on Lisp and Functional Programming, June 1994. [local copy]
• Separate Compilation for Standard ML. Andrew W. Appel and David B. MacQueen. Proc. 1994 ACM Conf. on Programming Language Design and Implementation, (ACM SIGPLAN Notices vol. 29, number 6), pp. 13-23, June 1994. [local copy]
• Hash-Consing Garbage Collection, by Andrew W. Appel and Marcelo J.R. Goncalves, Technical report TR-412-93, Department of Computer Science, Princeton University, January 1993.
• A Critique of Standard ML. Andrew W. Appel. Journal of Functional Programming 3 (4) 391-430, 1993.
• Smartest Recompilation. Zhong Shao and Andrew W. Appel. CS-TR-395-92, Princeton University, 1992. Proc. Twenthieth ACM Symp. on Principles of Programming Languages January 1993. [local copy]
• Unrolling recursions saves space. Andrew W. Appel. CS-TR-363-92, Princeton University, March 1992.
• Compiling with Continuations. Andrew W. Appel, Cambridge University Press, 1992.
• Is POPL Mathematics or Science? Report of the Program Chair of the 19th POPL. Andrew W. Appel. ACM SIGPLAN Notices 27 (4), pp. 87-89, April 1992. [local copy]
• Callee-save registers in Continuation-Passing Style. Lisp and Symbolic Computation 5, 189-219, 1992.
• Virtual memory primitives for user programs. Andrew W. Appel and Kai Li. Proc. Fourth Int'l Conf. on Architectural Support for Prog. Languages and Operating Systems, (ACM SIGPLAN Notices 26(4)) pp. 96-107, April 1991. [local copy] Also: VM-PUP benchmark program.
• Garbage Collection, in Topics in Advanced Language Implementation, Peter Lee, ed. MIT Press, 1991.
• Standard ML of New Jersey. Andrew W. Appel and David B. MacQueen. Third Int'l Symp. on Prog. Lang. Implementation and Logic Programming Springer-Verlag LNCS 528, pp. 1-13, August 1991.
• Debuggable concurrency extensions for Standard ML. Andrew P. Tolmach and Andrew W. Appel. Proc. ACM/ONR Workshop on Parallel and Distributed Debugging, May 1991 (ACM SIGPLAN Notices, Dec. 1991), pp. 115-127. [local copy]
• A Runtime System. Andrew W. Appel. Lisp and Symbolic Computation 3, 343-380, 1990.
• An Advisor For Flexible Working Sets. Rafael Alonso and Andrew W. Appel. 1990 ACM SIGMETRICS Conf. on Measurement and Modeling of Computer Systems pp. 153-162, May 1990. [local copy]
• Debugging Standard ML without reverse engineering, Andrew P. Tolmach and Andrew W. Appel, Proc. 1990 ACM Conf. on Lisp and Functional Programming pp. 1-12, June 1990. [local copy]
• Continuation-passing, closure-passing style. Andrew W. Appel and Trevor Jim. Proc. Sixteenth ACM Symposium on Principles of Programming Languages pp. 293-302, January 1989. [local copy]
• Allocation without Locking. Andrew W. Appel. Software--Practice and Experience 19(7):703-705, July 1989.
• Runtime Tags Aren't Necessary. Andrew W. Appel. Lisp and Symbolic Computation 2, 153-162 (1989).
• Simple Generational Garbage Collection and Fast Allocation. Andrew W. Appel. Software--Practice and Experience 19(2):171-183, February 1989.
• Vectorized Garbage Collection. Andrew W. Appel and Aage Bendiksen. The Journal of Supercomputing 3, 151-160 (1989).
• Real-time concurrent collection on stock multiprocessors. Andrew W. Appel, John R. Ellis, and Kai Li. Proc. ACM SIGPLAN '88 Conf. on Prog. Lang. Design and Implementation, June 1988. [local copy]
• The World's Fastest Scrabble Program. Andrew W. Appel and Guy J. Jacobson, Comm. ACM 31(5):572-578,585, May 1988.
• Simulating digital circuits with one bit per wire. Andrew W. Appel, IEEE Trans. on Computer-Aided Design of Integrated Circuits and Systems 7(9):987-993, September 1988.
• Re-opening closures. Andrew W. Appel, January 1988.
• Unifying Exceptions with Constructors in Standard ML. Andrew W. Appel, David MacQueen, Robin Milner, and Mads Tofte. Univ. of Edinburgh Dept. of Comp. Sci. ECS-LFCS-88-55, May 1988.
• Profiling in the presence of optimization and garbage collection. Andrew W. Appel, Bruce Duba, and David B. MacQueen. CS-TR-197-88, Princeton University, November 1988.
• A Standard ML Compiler. Andrew W. Appel and David B. MacQueen, CS-TR-097-87, Princeton University, 1987. Proc. Third Int'l Conf. on Functional Programming and Computer Architecture (LNCS 274, Springer-Verlag) September 1987.
• Generalizations of the Sethi-Ullman algorithm for register allocation. Andrew W. Appel and Kenneth J. Supowit, Software \(em Practice and Experience 17(6):417-421, 1987.
• Garbage collection can be faster than stack allocation. Andrew W. Appel. Information Processing Letters 25(4):275-279, 17 June 1987.
• Concise specifications of locally optimal code generators. Andrew W. Appel. CS-TR-080-87, Princeton University, 1987.
• Semantics-Directed Code Generation. Andrew W. Appel, Proc. Twelfth ACM Symposium on Principles of Programming Languages, January 1985. [local copy]
• An Efficient Program for Many-Body Simulations. Andrew W. Appel, SIAM Journal on Scientific and Statistical Computing 6(1):85-103, 1985.
• Compile-time Evaluation and Code Generation in Semantics-Directed Compilers. Andrew W. Appel, Ph.D. Thesis, Carnegie-Mellon University, July 1985.
• Rogomatic: A Belligerent Expert System, M. L. Mauldin, G. J. Jacobson, A. W. Appel, and L. G. C. Hamey. Proc. Fifth Nat. Conf. Canadian Soc. for Computational Studies of Intelligence, May, 1984. [HTML version]
• An Investigation of Galaxy Clustering Using an Asymptotically Fast N-Body Algorithm. Andrew W. Appel, Senior Thesis, Princeton University, 1981.
• A Braille Printer, by Andrew W. Appel and Douglas W. Jones, Medical Computing Laboratory, University of Illinois, August 1980.
• A Microprocessor-Based CAI System with Graphic Capabilities, F. J. Mabry, A. H. Levy, and A. W. Appel. Proc. 1978 conference, Assoc. for Development of Computer-based Instruction Systems.

The documents contained in these pages are included to ensure timely dissemination of scholarly and technical work on a non-commercial basis. Copyright and all rights therein are maintained by the authors or by other copyright holders, notwithstanding that they have offered their works here electronically. It is understood that all persons copying this information will adhere to the terms and constraints invoked by each author's copyright. These works may not be reposted without the explicit permission of the copyright holder.