Andrew W. Appel

Andrew W. Appel, Robert Dockins, Xavier Leroy: A List-Machine Benchmark for Mechanized Metatheory. J. Autom. Reasoning 49(3): 453-491 (2012)

Gordon Stewart, Lennart Beringer, Andrew W. Appel: Verified heap theorem prover by paramodulation. ICFP 2012: 3-14

Andrew W. Appel: Verified Software Toolchain. NASA Formal Methods 2012: 2

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

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

Andrew W. Appel: VeriSmall: Verified Smallfoot Shape Analysis. CPP 2011: 231-246

Andrew W. Appel: Verified Software Toolchain - (Invited Talk). ESOP 2011: 1-17

Gordon Stewart, Andrew W. Appel: Local actions for a curry-style operational semantics. PLPV 2011: 31-42

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

Aquinas Hobor, Robert Dockins, Andrew W. Appel: A Logical Mix of Approximation and Separation. APLAS 2010: 439-454

Sandrine Blazy, Benoît Robillard, Andrew W. Appel: Formal Verification of Coalescing Graph-Coloring Register Allocation. ESOP 2010: 145-164

Aquinas Hobor, Robert Dockins, Andrew W. Appel: A theory of indirection via approximation. POPL 2010: 171-184

Christian J. Bell, Andrew W. Appel, David Walker: Concurrent Separation Logic for Pipelined Parallelization. SAS 2010: 151-166

Robert Dockins, Aquinas Hobor, Andrew W. Appel: A Fresh Look at Separation Algebras and Share Accounting. APLAS 2009: 161-177

Robert Dockins, Andrew W. Appel, Aquinas Hobor: Multimodal Separation Logic for Reasoning About Operational Semantics. Electr. Notes Theor. Comput. Sci. 218: 5-20 (2008)

Aquinas Hobor, Andrew W. Appel, Francesco Zappa Nardelli: Oracle Semantics for Concurrent Separation Logic. ESOP 2008: 353-367

Andrew W. Appel, Xavier Leroy: A List-machine Benchmark for Mechanized Metatheory: (Extended Abstract). Electr. Notes Theor. Comput. Sci. 174(5): 95-108 (2007)

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

Andrew W. Appel, Sandrine Blazy: Separation Logic for Small-Step cminor. TPHOLs 2007: 5-21

Andrew W. Appel, Sandrine Blazy: Separation Logic for Small-step Cminor. CoRR abs/0707.4389 (2007)

Andrew W. Appel: Compiling with Continuations (corr. version). Cambridge University Press 2006, isbn 978-0-521-03311-4, pp. I-X, 1-260

Gang Tan, Andrew W. Appel: A Compositional Logic for Control Flow. VMCAI 2006: 80-94

Andrew W. Appel, Amy P. Felty: Dependent types ensure partial correctness of theorem provers. J. Funct. Program. 14(1): 3-19 (2004)

Andrew W. Appel, Amy P. Felty: Polymorphic Lemmas and Definitions in lambda-Prolog and Twelf. TPLP 4(1-2): 1-39 (2004)

Andrew W. Appel: Social processes and proofs of theorems and programs, revisited. PLDI 2004: 170

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

Andrew W. Appel, Amy P. Felty: Polymorphic lemmas and definitions in Lambda Prolog and Twelf. CoRR cs.LO/0403010 (2004)

Andrew W. Appel, Neophytos G. Michael, Aaron Stump, Roberto Virga: A Trustworthy Proof Checker. J. Autom. Reasoning 31(3-4): 231-260 (2003)

Lujo Bauer, Andrew W. Appel, Edward W. Felten: Mechanisms for secure modular programming in Java. Softw., Pract. Exper. 33(5): 461-480 (2003)

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

Juan Chen, Dinghao Wu, Andrew W. Appel, Hai Fang: A provably sound TAL for back-end optimization. PLDI 2003: 208-219

Dinghao Wu, Andrew W. Appel, Aaron Stump: Foundational proof checkers with small witnesses. PPDP 2003: 264-274

Eunyoung Lee, Andrew W. Appel: Policy-enforced linking of untrusted components. ESEC / SIGSOFT FSE 2003: 371-374

Sudhakar Govindavajhala, Andrew W. Appel: Using Memory Errors to Attack a Virtual Machine. IEEE Symposium on Security and Privacy 2003: 154-165

Andrew W. Appel, Jens Palsberg: Modern Compiler Implementation in Java, 2nd edition. Cambridge University Press 2002, isbn 0-521-82060-X

Amal J. Ahmed, Andrew W. Appel, Roberto Virga: A Stratified Semantics of General References A Stratified Semantics of General References. LICS 2002: 75-

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

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

Andrew W. Appel: Foundational Proof-Carrying Code. LICS 2001: 247-256

Andrew W. Appel, Lal George: Optimal Spilling for CISC Machines with Few Registers. PLDI 2001: 243-253

Daniel C. Wang, Andrew W. Appel: Type-preserving garbage collectors. POPL 2001: 166-178

Andrew W. Appel, Edward W. Felten: Technological access control interferes with noninfringing scholarship. Commun. ACM 43(9): 21-23 (2000)

Zhong Shao, Andrew W. Appel: Efficient and safe-for-space closure conversion. ACM Trans. Program. Lang. Syst. 22(1): 129-161 (2000)

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

Neophytos G. Michael, Andrew W. Appel: Machine Instruction Syntax and Semantics in Higher Order Logic. CADE 2000: 7-24

Andrew W. Appel, Amy P. Felty: A Semantic Model of Types and Machine Instuctions for Proof-Carrying Code. POPL 2000: 243-253

Matthias Blume, Andrew W. Appel: Hierarchical modularity. ACM Trans. Program. Lang. Syst. 21(4): 813-847 (1999)

Andrew W. Appel, Edward W. Felten: Proof-Carrying Authentication. ACM Conference on Computer and Communications Security 1999: 52-62

Andrew W. Appel, Amy P. Felty: Lightweight Lemmas in lambda-Prolog. ICLP 1999: 411-425

Andrew W. Appel, Alex Aiken (Eds.): POPL '99, Proceedings of the 26th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, San Antonio, TX, USA, January 20-22, 1999. ACM 1999, isbn 1-58113-095-3

Andrew W. Appel: Modern Compiler Implementation in Java. Cambridge University Press 1998, isbn 0-521-58388-8

Andrew W. Appel: Modern Compiler Implementation in C. Cambridge University Press 1998, isbn 0-521-58390-X

Andrew W. Appel: Modern Compiler Implementation in ML. Cambridge University Press 1998, isbn 0-521-58274-1

Andrew W. Appel: SSA is Functional Programming. SIGPLAN Notices 33(4): 17-20 (1998)

Jeffrey L. Korn, Andrew W. Appel: Traversal-Based Visualization of Data Structures. INFOVIS 1998: 11-18

Andrew W. Appel: Modern Compiler Implementation in Java: Basic Techniques. Cambridge University Press 1997, isbn 0-521-58654-2

Andrew W. Appel: Modern Compiler Implementation in C: Basic Techniques. Cambridge University Press 1997, isbn 0-521-58653-4

Andrew W. Appel: Modern Compiler Implementation in ML: Basic Techniques. Cambridge University Press 1997, isbn 0-521-58775-1

Andrew W. Appel, Trevor Jim: Shrinking lambda Expressions in Linear Time. J. Funct. Program. 7(5): 515-540 (1997)

Daniel C. Wang, Andrew W. Appel, Jeffrey L. Korn, Christopher S. Serra: The Zephyr Abstract Syntax Description Language. DSL 1997: 213-228

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

Andrew W. Appel, Zhong Shao: Empirical and Analytic Study of Stack Versus Heap Cost for Languages with Closures. J. Funct. Program. 6(1): 47-74 (1996)

Andrew W. Appel: Intensional Equality ;=) for Continuations. SIGPLAN Notices 31(2): 55-57 (1996)

Lal George, Andrew W. Appel: Iterated Register Coalescing. ACM Trans. Program. Lang. Syst. 18(3): 300-324 (1996)

Lal George, Andrew W. Appel: Iterated Register Coalescing. POPL 1996: 208-218

Andrew P. Tolmach, Andrew W. Appel: A Debugger for Standard ML. J. Funct. Program. 5(2): 155-200 (1995)

Marcelo J. R. Gonçalves, Andrew W. Appel: Cache Performance of Fast-Allocating Programs. FPCA 1995: 293-305

Zhong Shao, Andrew W. Appel: A Type-Based Compiler for Standard ML. PLDI 1995: 116-129

Andrew W. Appel: Loop Headers in Lambda-Calculus or CPS. Lisp and Symbolic Computation 7(4): 337-343 (1994)

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

Zhong Shao, Andrew W. Appel: Space-Efficient Closure Representations. LISP and Functional Programming 1994: 150-161

Zhong Shao, John H. Reppy, Andrew W. Appel: Unrolling Lists. LISP and Functional Programming 1994: 185-195

Andrew W. Appel, David B. MacQueen: Separate Compilation for Standard ML. PLDI 1994: 13-23

Andrew W. Appel: A Critique of Standard ML. J. Funct. Program. 3(4): 391-429 (1993)

Zhong Shao, Andrew W. Appel: Smartest Recompilation. POPL 1993: 439-450

Andrew W. Appel: Compiling with Continuations. Cambridge University Press 1992, isbn 0-521-41695-7

Andrew W. Appel, Zhong Shao: Callee-Save Registers in Continuation-Passing Style. Lisp and Symbolic Computation 5(3): 191-221 (1992)

Andrew W. Appel: Is POPL mathematics or science? SIGPLAN Notices 27(4): 87-89 (1992)

Andrew W. Appel, Kai Li: Virtual Memory Primitives for User Programs. ASPLOS 1991: 96-107

Andrew P. Tolmach, Andrew W. Appel: Debuggable Concurrency Extensions for Standard ML. Workshop on Parallel and Distributed Debugging 1991: 120-131

Andrew W. Appel, David B. MacQueen: Standard ML of New Jersey. PLILP 1991: 1-13

Andrew W. Appel: A Runtime System. Lisp and Symbolic Computation 3(4): 343-380 (1990)

Andrew P. Tolmach, Andrew W. Appel: Debugging Standard ML Without Reverse Engineering. LISP and Functional Programming 1990: 1-12

Rafael Alonso, Andrew W. Appel: An Advisor for Flexible Working Sets. SIGMETRICS 1990: 153-162

Andrew W. Appel: Runtime Tags Aren't Necessary. Lisp and Symbolic Computation 2(2): 153-162 (1989)

Andrew W. Appel: Simple Generational Garbage Collection and Fast Allocation. Softw., Pract. Exper. 19(2): 171-183 (1989)

Andrew W. Appel: Allocation without Locking. Softw., Pract. Exper. 19(7): 703-705 (1989)

Andrew W. Appel, Aage Bendiksen: Vectorized garbage collection. The Journal of Supercomputing 3(3): 151-160 (1989)

Andrew W. Appel, Trevor Jim: Continuation-Passing, Closure-Passing Style. POPL 1989: 293-302

Andrew W. Appel, Guy J. Jacobson: The World's Fastest Scrabble Program. Commun. ACM 31(5): 572-578 (1988)

Andrew W. Appel: Simulating digital circuits with one bit per wire. IEEE Trans. on CAD of Integrated Circuits and Systems 7(9): 987-993 (1988)

Andrew W. Appel, John R. Ellis, Kai Li: Real-Time Concurrent Collection on Stock Multiprocessors. PLDI 1988: 11-20

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

Andrew W. Appel: Garbage Collection can be Faster than Stack Allocation. Inf. Process. Lett. 25(4): 275-279 (1987)

Andrew W. Appel, Kenneth J. Supowit: Generalization of the Sethi-Ullman Algorithm for Register Allocation. Softw., Pract. Exper. 17(6): 417-421 (1987)

Andrew W. Appel, David B. MacQueen: A Standard ML compiler. FPCA 1987: 301-324

Andrew W. Appel: Semantics-Directed Code Generation. POPL 1985: 315-324