Vita

Andrew W. Appel

Eugene Higgins Professor of Computer Science
Chair, Department of Computer Science, Princeton University
35 Olden Street, Princeton NJ 08540

appel@princeton.edu, +1-609-258-4627, fax: +1-609-258-2016
http://www.cs.princeton.edu/~appel

Research Interests

Programming languages, computer security, compilers, type theory, semantics, software engineering, automated theorem proving, elections and voting technology.

Education

A.B. summa cum laude (physics) Princeton University, 1981
Ph.D. (computer science) Carnegie-Mellon University, 1985

Professional Appointments

Princeton University, Princeton, NJ. Chair of the Department of Computer Science, since 2009. Eugene Higgins Professor of Computer Science, since 2011; Professor of Computer Science, 1995-2011; Associate Chair, 1997-2007; Assoc. Prof., 1992-95; Asst. Prof. 1986-92.

INRIA (Institut National de Recherche en Informatique et en Automatique), Rocquencourt, France. Visiting Professor, academic year 2005-06 & summers 2004, 2007.

Bell Laboratories, Murray Hill, NJ. Member of Technical Staff, Summer 1984. Consultant, 1983-2001.

Carnegie-Mellon University, Pittsburgh, PA. Research and teaching assistant, 1982-85.

College of Medicine, University of Illinois, Urbana, IL. Computer programmer, summers 1976-80.

Awards and Honors

Kusaka Memorial Prize in Physics, Princeton University, 1981.

National Science Foundation Graduate Student Fellowship, 1981-1984.

ACM Fellow (Association for Computing Machinery), 1998.

The Other Prize, Programming Contest of the ACM International Conference on Functional Programming, 1998.

ACM SIGPLAN Distinguished Service Award, 2002.

ACM SIGPLAN selected "Real-time Concurrent Collection on Stock Multiprocessors" (Appel, Ellis, Li 1988) as one of the 50 most influential papers in 20 years of the PLDI conference, 2002.

Professional Activities

  1. Program Committee, ACM SIGPLAN '89 Conf. on Prog. Lang. Design and Implementation, 1989.
  2. Program Committee, Seventeenth ACM Symp. on Principles of Programming Languages, 1990.
  3. Associate Editor, ACM Transactions on Programming Languages and Systems, 1990-1992.
  4. Associate Editor, ACM Letters on Programming Languages and Systems, 1991-1992.
  5. Program Chair, Nineteenth ACM Symp. on Principles of Programming Languages, 1992.
  6. Co-editor, Journal of Functional Programming special issue on ML, 1992.
  7. Program Committee, Sixth ACM Conf. on Functional Prog. Lang. and Computer Architecture, 1993.
  8. Editor in Chief, ACM Transactions on Programming Languages and Systems, 1993-97.
  9. Program Committee, International Conference on Functional Programming, 1997.
  10. General Chair, 26th ACM Symp. on Principles of Programming Languages, 1999.
  11. Program Committee, IEEE Symposium on Security and Privacy, 2002.
  12. Program Committee, ACM SIGPLAN Workshop on Types in Language Design and Implementation, 2003.
  13. Program Committee, Nineteenth Annual IEEE Symposium on Logic in Computer Science, 2004.
  14. Program Committee, ACM SIGPLAN 2005 Conference on Programming Language Design and Implementation (PLDI), 2005.
  15. Program Committee, International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice (LFMTP'06), 2006.
  16. Program Committee, EVT'07: 2007 Usenix/ACCURATE Electronic Voting Technology Workshop.
  17. Program Committee, POPL'09: 36th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2009.
  18. Program Committee, PLDI 2011: 32nd ACM SIGPLAN conference on Programming Language Design and Implementation.

Research Grants

  1. Implementation of an efficient reducer for lambda expressions, National Science Foundation DCR-8603453, $115,799, 1986-88.
  2. Digital Equipment Corporation Faculty Incentive Grant, $180,000, 1986-89.
  3. Unifying compile-time and run-time evaluation, National Science Foundation CCR-8806121, $123,510, 1988-90.
  4. Standard ML of New Jersey software capitalization, National Science Foundation CCR-8914570, $119,545, 1990-91.
  5. Using immutable types for debugging and parallelism, National Science Foundation CCR-9002786, $174,618, 1990-92.
  6. Optimization of space usage, National Science Foundation CCR-9200790, $348,119, 1992-96.
  7. Framework, Algorithms, and Applications for Cross-module Inlining, National Science Foundation CCR-9625413, $180,331, 1996-98.
  8. Development of a HIL/LIL Framework for a National Compiler Infrastructure, Defense Advanced Research Projects Agency and National Science Foundation (as subcontractor to Univ. of Virginia), $1,397,293, 1996-99.
  9. Tools, Interfaces, and Access Control for Secure Programming, National Science Foundation CCR-9870316, $322,000, 1998-2001 (co-PI).
  10. Scaling Proof-Carrying Code to Production Compilers and Security Policies, Defense Advanced Research Projects Agency, $3,870,378, 1999-2004.
  11. Applying Compiler Techniques to Proof-Carrying Code, National Science Foundation CCR-9974553, $220,000, 1999-2002.
  12. IBM University Partnership Program, $40,000, 1999-2000.
  13. High-Assurance Common Language Runtime, National Science Foundation CCR-0208601, $400,000, 2002-2005.
  14. Assurance-Carrying Components, Advanced Research and Development Agency contract NBCHC030106, $759,910, 2003-05.
  15. Sun Microsystems research grant, $20,000, 2004.
  16. End-to-end source-to-object verification of interface safety, National Science Foundation grant CCF-0540914, $325,000, 2006-09.
  17. MulVAL Technologies Plan, New Jersey Commission on Science and Technology, $60,000, 2006.
  18. Microsoft Corporation research grant, $25,000, 2006.
  19. Evidence-based Trust in Large-scale MLS Systems, Air Force Office of Scientific Research FA9550-09-1-0138 (as subcontractor to Kansas State University), $1,000,000, 2009-14.
  20. Combining Foundational and Lightweight Formal Methods to Build Certifiably Dependable Software, National Science Foundation grant CNS-0910448, $500,000, 2009-13.
  21. Compositionality and Automation for Robotics Security, Defense Advanced Research Projects Agency award FA8750-12-2-0293, $5,113,351, 2012-2017.

Publications

    Books, chapters in books

  1. ``Garbage Collection,'' in Topics in Advanced Language Implementation, Peter Lee, ed. MIT Press, 1991.
  2. Compiling with Continuations, Cambridge University Press, 1992.
  3. Modern Compiler Implementation in ML, Cambridge University Press, 1998.
  4. Modern Compiler Implementation in Java, Cambridge University Press, 1998.
  5. Modern Compiler Implementation in C, Cambridge University Press, 1998.
  6. Modern Compiler Implementation in Java, 2nd edition, with Jens Palsberg, Cambridge University Press, 2002.
  7. Alan Turing's Systems of Logic: The Princeton Thesis, edited and introduced by Andrew W. Appel, Princeton University Press, 2012.

    Journal papers

  8. An Efficient Program for Many-Body Simulations. SIAM Journal on Scientific and Statistical Computing 6(1):85-103, 1985.
  9. Generalizations of the Sethi-Ullman algorithm for register allocation. with Kenneth J. Supowit. Software -- Practice & Experience 17(6):417-421, 1987.
  10. Garbage collection can be faster than stack allocation. Information Processing Letters, 25(4):275-279, 17 June 1987.
  11. The World's Fastest Scrabble Program, with Guy J. Jacobson, Comm. ACM 31(5):572-578,585, May 1988.
  12. Simulating digital circuits with one bit per wire, IEEE Trans. on Computer-Aided Design of Integrated Circuits and Systems 7(9):987-993, September 1988.
  13. Simple Generational Garbage Collection and Fast Allocation. Software -- Practice & Experience 19(2):171-183, February 1989.
  14. Allocation without Locking. Software -- Practice & Experience 19(7):703-705, July 1989.
  15. Runtime Tags Aren't Necessary. Lisp and Symbolic Computation 2, 153-162 (1989).
  16. Vectorized Garbage Collection, with Aage Bendiksen. The Journal of Supercomputing 3, 151-160 (1989).
  17. A Runtime System. Lisp and Symbolic Computation 3, 343-380, 1990.
  18. Real-time concurrent garbage collection system and method, with John R. Ellis and Kai Li. U.S. Patent 5,088,036, 1992.
  19. Callee-save registers in Continuation-Passing Style, with Zhong Shao. Lisp and Symbolic Computation 5, 189-219, 1992.
  20. A Critique of Standard ML. Journal of Functional Programming 3 (4) 391-430, 1993.
  21. A Debugger for Standard ML, with Andrew Tolmach. Journal of Functional Programming 5 (2) 155-200, 1995.
  22. Axiomatic Bootstrapping: A Guide for Compiler Hackers. ACM Trans. on Prog. Lang. and Systems 16 (6) 1699-1718, November 1994.
  23. Loop Headers in Lambda-calculus or CPS. Lisp and Symbolic Computation 7, 337-343, 1994.
  24. Empirical and Analytic Study of Stack versus Heap Cost for Languages with Closures, with Zhong Shao. Journal of Functional Programming 6 (1) 47-74, 1996.
  25. How to Edit a Journal by E-mail, Journal of Scholarly Publishing 27 (2) 82-99, January 1996.
  26. Iterated Register Coalescing, with Lal George. ACM Trans. on Prog. Lang. and Systems 18(3) 300-324, May 1996.
  27. Security and document compatibility for electronic refereeing, CBE Views 20(1) 9-10, 1997, published by the Council of Biology Editors.
  28. Shrinking lambda-calculus in linear time, with Trevor Jim. Journal of Functional Programming 7 (5) 515-540, 1997.
  29. Hierarchical Modularity, with Matthias Blume. ACM Transactions on Programming Languages and Systems, 21 (4) 812-846, July 1999.
  30. Efficient and Safe-for-Space Closure Conversion, with Zhong Shao, ACM Trans. on Prog. Lang. and Systems 22(1) 129-161, January 2000.
  31. Technological Access Control Interferes with Noninfringing Scholarship, with Edward W. Felten. Communications of the ACM 43 (9) 21-23, September 2000.
  32. An Indexed Model of Recursive Types for Foundational Proof-Carrying Code, with David McAllester. ACM Transactions on Programming Languages and Systems 23 (5) 657-683, September 2001.
  33. SAFKASI: A Security Mechanism for Language-Based Systems with Dan Wallach and Edward W. Felten. ACM Transactions on Software Engineering and Methodology, 9 (4) 341-378, October 2000.
  34. Mechanisms for secure modular programming in Java, with Lujo Bauer and Edward W. Felten. Software--Practice and Experience 33:461-480, 2003.
  35. A Trustworthy Proof Checker, with Neophytos G. Michael, Aaron Stump, and Roberto Virga. Journal of Automated Reasoning 31:231-260, 2003.
  36. Polymorphic Lemmas and Definitions in Lambda Prolog and Twelf, with Amy P. Felty. Theory and Practice of Logic Programming 4 (1) 1-39, January 2004.
  37. Dependent Types Ensure Partial Correctness of Theorem Provers, with Amy P. Felty. Journal of Functional Programming 14(1):3-19, January 2004.
  38. Semantic Foundations for Typed Assembly Languages, with A. Ahmed, C. D. Richards, G. Tan, and D. C. Wang. ACM Transactions on Programming Languages and Systems, 32(3):7.1-7.67, March 2010.
  39. 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
  40. 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.

    Conference papers

  41. A Microprocessor-Based CAI System with Graphic Capabilities, with F. J. Mabry and A. H. Levy. Proc. 1978 conference, Assoc. for Development of Computer-based Instruction Systems.
  42. Rogomatic: A Belligerent Expert System, with M. L. Mauldin, G. J. Jacobson, and L. G. C. Hamey. Proc. Fifth Nat. Conf. Canadian Soc. for Computational Studies of Intelligence, May, 1984.
  43. Semantics-Directed Code Generation, Proc. Twelfth ACM Symposium on Principles of Programming Languages, January 1985.
  44. A Standard ML compiler, with D. B. MacQueen, Proc. Third Int'l Conf. on Functional Programming & Computer Architecture (LNCS 274, Springer-Verlag), Portland, Oregon, September 1987.
  45. Real-time concurrent collection on stock multiprocessors, with John Ellis & Kai Li. Proc. ACM SIGPLAN '88 Conf. on Prog. Lang. Design & Implementation, pp. 11-20, June 1988.
  46. Continuation-passing, closure-passing style, with Trevor Jim. Proc. Sixteenth ACM Symposium on Principles of Programming Languages, pp. 293-302, January 1989.
  47. An advisor for flexible working sets, with Rafael Alonso. 1990 ACM SIGMETRICS Conf. on Measurement and Modeling of Computer Systems, pp. 153-162, May 1990.
  48. Debugging Standard ML without reverse engineering, with Andrew P. Tolmach. Proc. 1990 ACM Conf. on Lisp and Functional Programming, pp. 1-12, June 1990.
  49. Virtual memory primitives for user programs, with Kai Li. Proc. Fourth Int'l Conf. on Architectural Support for Prog. Languages and Operating Systems, (SIGPLAN Notices 26(4)) pp. 96-107, April 1991.
  50. Standard ML of New Jersey, with David B. MacQueen. Third Int'l Symp. on Prog. Lang. Implementation and Logic Programming, Springer-Verlag LNCS 528, pp. 1-13, August 1991.
  51. Debuggable concurrency extensions for Standard ML, with Andrew P. Tolmach. Proc. ACM/ONR Workshop on Parallel and Distributed Debugging, May 1991 (SIGPLAN Notices, Dec. 1991), pp. 115-127.
  52. Smartest Recompilation, with Zhong Shao. Proc. Twenthieth ACM Symp. on Principles of Programming Languages, January 1993.
  53. Unrolling Lists, with Zhong Shao and John H. Reppy. Proc. 1994 ACM Conf. on Lisp and Functional Programming, pp. 185-195, June 1994.
  54. Space-Efficient Closure Representations, with Zhong Shao. Proc. 1994 ACM Conf. on Lisp and Functional Programming, pp. 150-161, June 1994.
  55. Separate Compilation for Standard ML, with David B. MacQueen. Proc. 1994 ACM Conf. on Programming Language Design and Implementation (SIGPLAN Notices v. 29 #6), pp. 13-23, June 1994.
  56. A Type-Based Compiler for Standard ML, with Zhong Shao. Proc. 1995 ACM Conf. on Programming Language Design and Implementation (SIGPLAN Notices v. 30 #6), pp. 116-129, June 1995.
  57. Cache Performance of Fast-Allocating Programs, with Marcelo J. R. Goncalves. Proc. Seventh Int'l Conf. on Functional Programming and Computer Architecture, pp. 293-305, ACM Press, June 1995.
  58. Iterated Register Coalescing, with Lal George. 23rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages pp. 208-218, January 1996.
  59. Lambda-Splitting: A Higher-Order Approach to Cross-Module Optimizations, with Matthias Blume. Proc. ACM SIGPLAN International Conference on Functional Programming (ICFP '97), pp. 112-124, June 1997.
  60. The Zephyr Abstract Syntax Description Language, with Daniel C. Wang, Jeff L. Korn, and Christopher S. Serra. Conference on Domain-Specific Languages, USENIX Association, October 1997.
  61. Traversal-based Visualization of Data Structures, with Jeffrey L. Korn, IEEE Symposium on Information Visualization (InfoVis '98), pp. 11-18, October 1998.
  62. Lightweight Lemmas in Lambda Prolog, with Amy Felty, 16th International Conference on Logic Programming, pp. 411-425, MIT Press, November 1999.
  63. Proof-Carrying Authentication, with Edward Felten, 6th ACM Conference on Computer and Communications Security, November 1999.
  64. A Semantic Model of Types and Machine Instructions for Proof-Carrying Code, with Amy P. Felty. 27th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL '00), pp. 243-253, January 2000.
  65. Machine Instruction Syntax and Semantics in Higher Order Logic, with Neophytos G. Michael. 17th International Conference on Automated Deduction (CADE-17), Springer-Verlag (Lecture Notes in Artificial Intelligence), pp. 7-24, June 2000.
  66. Efficient Substitution in Hoare Logic Expressions, with Kedar Swadi and Roberto Virga. 4th International Workshop on Higher-Order Operational Techniques in Semantics (HOOTS 2000), pp. 35-50, September 2000.
  67. Type-Preserving Garbage Collectors, with Daniel C. Wang. POPL 2001: The 28th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 166-178, January 2001.
  68. Fair use, public domain, or piracy ... should the digital exchange of copyrighted works be permitted or prevented? (panel symposium) with Y. Benkler, M. Carlinsky, et al., Fordham Intellectual Property, Media & Entertainment Law Journal, 11(2) 257-408, Winter 2001.
  69. Optimal Spilling for CISC Machines with Few Registers, with Lal George. ACM SIGPLAN 2001 Conference on Programming Language Design and Implementation , pp. 243-253, June 2001.
  70. Foundational Proof-Carrying Code. 16th Annual IEEE Symposium on Logic in Computer Science (LICS '01), pp. 247-258, June 2001.
  71. A Stratified Semantics of General References Embeddable in Higher-Order Logic, with Amal Ahmed and Roberto Virga. 17th Annual IEEE Symposium on Logic in Computer Science (LICS 2002), pp. 75-86, June 2002.
  72. Creating and Preserving Locality of Java Applications at Allocation and Garbage Collection Times, with Yefim Shuf, Manish Gupta, Hubertus Franke, 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.
  73. A Trustworthy Proof Checker, with Neophytos G. Michael, Aaron Stump, and Roberto Virga. In Verification Workshop - VERIFY 2002 and (jointly) in Foundations of Computer Security - FCS 2002 Copenhagen, Denmark, July 25-26, 2002.
  74. Using Memory Errors to Attack a Virtual Machine, with Sudhakar Govindavajhala, 2003 IEEE Symposium on Security and Privacy, pp. 154-165, May 2003.
  75. A Provably Sound TAL for Back-end Optimization, with Juan Chen, Dinghao Wu, and Hai Fang. PLDI 2003: ACM SIGPLAN Conference on Programming Language Design and Implementation, pp. 208-219, June 2003.
  76. Foundational Proof Checkers with Small Witnesses, with Dinghao Wu and Aaron Stump. 5th ACM-SIGPLAN International Conference on Principles and Practice of Declarative Programming, pp. 264-274, August 2003.
  77. Policy-Enforced Linking of Untrusted Components (Extended Abstract), with Eunyoung Lee. European Software Engineering Conference and ACM SIGSOFT Symposium on the Foundations of Software Engineering, pp. 371-374, September 2003.
  78. 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.
  79. MulVAL: A Logic-based Network Security Analyzer with Xinming Ou and Sudhakar Govindavajhala. In 14th Usenix Security Symposium, August 2005.
  80. A Compositional Logic for Control Flow with Gang Tan. In 7th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI), January 2006.
  81. 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.
  82. A list-machine benchmark for mechanized metatheory (extended abstract) by Andrew W. Appel and Xavier Leroy. LFMTP'06: International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice, August 2006.
  83. 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.
  84. 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.
  85. Effective Audit Policy for Voter-Verified Paper Ballots, presented at 2007 Annual Meeting of the American Political Science Association, Chicago, September 1, 2007.
  86. Oracle Semantics for Concurrent Separation Logic, by Aquinas Hobor, Andrew W. Appel, and Francesco Zappa Nardelli, in ESOP'08: European Symposium on Programming, April 2008.
  87. 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.
  88. The New Jersey Voting-machine Lawsuit and the AVC Advantage DRE Voting Machine, with Maia Ginsburg, Harri Hursti, Brian W. Kernighan, Christopher D. Richards, Gang Tan, and Penny Venetis. In EVT/WOTE'09, 2009 Electronic Voting Technology Workshop / Workshop on Trustworthy Elections, August 2009.
  89. A Fresh Look at Separation Algebras and Share Accounting by Robert Dockins, Aquinas Hobor, and Andrew W. Appel. Seventh Asian Symposium on Programming Languages and Systems (APLAS 2009), December 2009.
  90. A Theory of Indirection via Approximation, by Aquinas Hobor, Robert Dockins, and Andrew W. Appel. POPL 2010: The 37th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 171-184, January 2010.
  91. 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.
  92. Formal Verification of Coalescing Graph-Coloring Register Allocation, by Sandrine Blazy, Benoit Robillard and Andrew W. Appel. ESOP 2010: 19th European Symposium on Programming, pp. 145-164, March 2010.
  93. 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.
  94. Verified Software Toolchain, by Andrew W. Appel. In ESOP 2011: 20th European Symposium on Programming, LNCS 6602, pp. 1-17, March 2011.
  95. 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.
  96. 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.
  97. 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.

    Review Articles, Tutorials, Position Papers

  98. Book Review of Garbage Collection: Algorithms for Automatic Dynamic Memory Management by Richard Jones and Rafael Lins. Journal of Functional Programming 7(2), pp. 227-229, March 1997.
  99. SSA is Functional Programming. ACM SIGPLAN Notices v. 33, no. 4, pp. 17-20, April 1998.
  100. Protection against untrusted code. IBM Developer Works, September 1999.
  101. Retrospective: Real-time Concurrent Collection on Stock Multiprocessors. 20 Years of the ACM/SIGPLAN Conference on Programming Language Design and Implementation (1979-1999): A Selection, ACM Press, 2004.
  102. Foundational High-level Static Analysis. In CAV 2008 Workshop on Exploiting Concurrency Efficiently and Correctly, July 2008.
  103. Freedom-to-Tinker: 16 articles on the freedom-to-tinker.com blog between 2007 and 2009; 6 articles in 2010; 15 articles in 2011.
  104. 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.
  105. The Birth of Computer Science at Princeton in the 1930s, in A. W. Appel, ed., Alan Turing's Systems of Logic: The Princeton Thesis, Princeton University Press, 2012.

    Unrefereed papers

  106. An Investigation of Galaxy Clustering Using an Asymptotically Fast N-Body Algorithm. Senior Thesis, Princeton University, 1981.
  107. Compile-time Evaluation and Code Generation in Semantics-Directed Compilers. Ph.D. Thesis, Carnegie-Mellon University, July 1985.
  108. Concise specifications of locally optimal code generators, Princeton Univ. Dept. of Computer Science CS-TR-080-87, 1987.
  109. Re-opening closures, Princeton Univ. Dept. of Computer Science CS-TR-079-87, February 1987.
  110. Optimizing closure environment representations, with Trevor Jim. Princeton Univ. Dept. of Computer Science CS-TR-168-88, July 1988.
  111. Unifying Exceptions with Constructors in Standard ML, with David MacQueen, Robin Milner, and Mads Tofte. Univ. of Edinburgh Dept. of Comp. Sci. CSR-266-88, May 1988.
  112. Profiling in the presence of optimization and garbage collection, with Bruce Duba and David MacQueen. CS-TR-197-88, November 1988.
  113. Emulating Write-Allocate on a No-Write-Allocate Cache, CS-TR-459-94, Princeton University, June 20, 1994.
  114. Is POPL Mathematics or Science? ACM SIGPLAN Notices 27 (4), pp. 87-89, April 1992.
  115. Intensional Equality ;=) for Continuations, ACM SIGPLAN Notices 31 (2), pp. 55-57, February 1996.
  116. Ceci n'est pas une urne: On the Internet vote for the Assemblée des Français de l'Etranger, June 2006.
  117. 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.
  118. The CompCert Memory Model, Version 2, by Xavier Leroy, Andrew W. Appel, Sandrine Blazy, and Gordon Stewart. INRIA Research Report RR-7987, June 2012.

PhD Students

  1. Andrew P. Tolmach, Ph.D. (1992) Debugging Standard ML. Associate Professor, Portland State University.
  2. Zhong Shao, Ph.D. (1994) Compiling Standard ML for Efficient Execution on Modern Machines. Professor, Yale University.
  3. Marcelo J. R. Goncalves, Ph.D. (1995) Cache Performance of Programs with Intensive Heap Allocation and Generational Garbage Collection. Software Engineer, Oracle.com, Portland, Oregon.
  4. Matthias Blume, Ph.D. (1997) Hierarchical Modularity and Intermodule Optimization. Computer Scientist, Google, Inc.
  5. Richard (Drew) Dean, Ph.D. (1999) Formal Aspects of Mobile Code Security. Program Manager, DARPA.
  6. Jeffrey L. Korn, Ph.D. (1999) Abstraction and Visualization in Graphical Debuggers. Software Engineer, Google, Inc.
  7. Daniel C. Wang, Ph.D. (2002) Managing Memory with Types. Computer Scientist, Microsoft Corporation.
  8. Kedar N. Swadi, Ph.D. (2003) Typed Machine Language. CTO, AlgoAnalytics, Pune, India.
  9. Lujo Bauer, Ph.D. (2003) Access Control for the Web via Proof-Carrying Authorization. Assistant Research Professor, Carnegie Mellon University.
  10. Eunyoung Lee, Ph.D. (2003) Secure Linking: A Logical Framework for Policy-Enforced Component Composition. Associate Professor, Dongduk Women's University, Seoul, Korea.
  11. Juan Chen, Ph.D. (2004) A Low-Level Typed Assembly Language with a Machine-checkable Soundness Proof. Researcher, Microsoft Research.
  12. Amal J. Ahmed, Ph.D. (2004) Semantics of Types for Mutable State. Assistant Professor, Northeastern University.
  13. Gang Tan, Ph.D. (2005) A Compositional Logic for Control Flow and its Application to Foundational Proof-Carrying Code. Assistant Professor, Lehigh University.
  14. Dinghao Wu, Ph.D. (2005) Interfacing Compilers, Proof Checkers, and Proofs for Foundational Proof-Carrying Code. Assistant Professor, Pennsylvania State University.
  15. Xinming Ou, Ph.D. (2005) A Logic Programming Approach to Network Security Analysis. Associate Professor, Kansas State University.
  16. Sudhakar Govindavajhala, Ph.D. (2006) A Formal Approach to Practical Network Security Management. Computer and network security consultant.
  17. Aquinas Hobor, Ph.D. (2008) Oracle Semantics. Lecturer, National University of Singapore.
  18. Christopher D. Richards, Ph.D. (2010) The Approximation Modality in Models of Higher-Order Types. Computer Scientist, Google, Inc.
  19. Robert Dockins, Ph.D. (2012) Operational Refinement for Compiler Correctness. Postdoc, Portland State University.
The documents linked from this page 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.