Multimodal Separation Logic for Reasoning About Operational Semantics, by Robert Dockins, Andrew W. Appel, and Aquinas Hobor, (to appear) in Twenty-fourth Conference on the Mathematical Foundations of Programming Semantics, May 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.
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.
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.
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.
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
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.
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.
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. To appear in 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.
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.
Hints on Proving Theorems in Twelf. Andrew W. Appel, Princeton University, February 2000.
Optimal Spilling for CISC Machines with Few Registers. Andrew W. Appel and Lal George. ACM SIGPLAN 2001 Conference on Programming Language Design and Implementation , pp. 243-253, June 2001.
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.
Type-Preserving Garbage Collectors. Daniel C. Wang and Andrew W. Appel. POPL 2001: The 28th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 166-178, January 2001. Extended Version (Technical Report)
Efficient Substitution in Hoare Logic Expressions. Andrew W. Appel, Kedar N. Swadi, and Roberto Virga. 4th International Workshop on Higher-Order Operational Techniques in Semantics (HOOTS 2000), pp. 35-50, September 2000. [PDF]
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.
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.
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.
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.
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.
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.
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. ©1995 ACM.
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, ©1994 ACM.
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. ©1994 ACM.
Space-Efficient Closure Representations. Zhong Shao and Andrew W. Appel. Proc. 1994 ACM Conf. on Lisp and Functional Programming, June 1994. ©1994 ACM.
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. ©1994 ACM.
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. ©1993 ACM.
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.
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. ©1991 ACM. 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. ©1991 ACM.
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.
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.
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.
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 19(7):703-705, July 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.
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. CSR-266-88, 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.
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.
An Investigation of Galaxy Clustering Using an Asymptotically Fast N-Body Algorithm. Andrew W. Appel, Senior Thesis, Princeton University, 1981.
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.