2008 |
80 | EE | Aquinas Hobor,
Andrew W. Appel,
Francesco Zappa Nardelli:
Oracle Semantics for Concurrent Separation Logic.
ESOP 2008: 353-367 |
79 | EE | Robert Dockins,
Andrew W. Appel,
Aquinas Hobor:
Multimodal Separation Logic for Reasoning About Operational Semantics.
Electr. Notes Theor. Comput. Sci. 218: 5-20 (2008) |
2007 |
78 | EE | 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 |
77 | EE | Andrew W. Appel,
Sandrine Blazy:
Separation Logic for Small-Step cminor.
TPHOLs 2007: 5-21 |
76 | EE | Andrew W. Appel,
Sandrine Blazy:
Separation Logic for Small-step Cminor
CoRR abs/0707.4389: (2007) |
75 | EE | Andrew W. Appel,
Xavier Leroy:
A List-machine Benchmark for Mechanized Metatheory: (Extended Abstract).
Electr. Notes Theor. Comput. Sci. 174(5): 95-108 (2007) |
2006 |
74 | EE | Gang Tan,
Andrew W. Appel:
A Compositional Logic for Control Flow.
VMCAI 2006: 80-94 |
2004 |
73 | EE | Andrew W. Appel:
Social processes and proofs of theorems and programs, revisited.
PLDI 2004: 170 |
72 | EE | Gang Tan,
Andrew W. Appel,
Kedar N. Swadi,
Dinghao Wu:
Construction of a Semantic Model for a Typed Assembly Language.
VMCAI 2004: 30-43 |
71 | EE | Andrew W. Appel,
Amy P. Felty:
Polymorphic lemmas and definitions in Lambda Prolog and Twelf
CoRR cs.LO/0403010: (2004) |
70 | EE | Andrew W. Appel,
Amy P. Felty:
Dependent types ensure partial correctness of theorem provers.
J. Funct. Program. 14(1): 3-19 (2004) |
69 | | Andrew W. Appel,
Amy P. Felty:
Polymorphic Lemmas and Definitions in lambda-Prolog and Twelf.
TPLP 4(1-2): 1-39 (2004) |
2003 |
68 | EE | 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 |
67 | EE | Eunyoung Lee,
Andrew W. Appel:
Policy-enforced linking of untrusted components.
ESEC / SIGSOFT FSE 2003: 371-374 |
66 | EE | Sudhakar Govindavajhala,
Andrew W. Appel:
Using Memory Errors to Attack a Virtual Machine.
IEEE Symposium on Security and Privacy 2003: 154-165 |
65 | EE | Juan Chen,
Dinghao Wu,
Andrew W. Appel,
Hai Fang:
A provably sound TAL for back-end optimization.
PLDI 2003: 208-219 |
64 | EE | Dinghao Wu,
Andrew W. Appel,
Aaron Stump:
Foundational proof checkers with small witnesses.
PPDP 2003: 264-274 |
63 | EE | Andrew W. Appel,
Neophytos G. Michael,
Aaron Stump,
Roberto Virga:
A Trustworthy Proof Checker.
J. Autom. Reasoning 31(3-4): 231-260 (2003) |
62 | | Lujo Bauer,
Andrew W. Appel,
Edward W. Felten:
Mechanisms for secure modular programming in Java.
Softw., Pract. Exper. 33(5): 461-480 (2003) |
2002 |
61 | | Andrew W. Appel:
Modern Compiler Implementation in Java, 2nd edition.
Cambridge University Press 2002 |
60 | EE | Amal J. Ahmed,
Andrew W. Appel,
Roberto Virga:
A Stratified Semantics of General References A Stratified Semantics of General References.
LICS 2002: 75- |
59 | EE | 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 |
2001 |
58 | | Andrew W. Appel:
Foundational Proof-Carrying Code.
LICS 2001 |
57 | | Andrew W. Appel,
Lal George:
Optimal Spilling for CISC Machines with Few Registers.
PLDI 2001: 243-253 |
56 | EE | Daniel C. Wang,
Andrew W. Appel:
Type-preserving garbage collectors.
POPL 2001: 166-178 |
55 | EE | 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) |
2000 |
54 | | Neophytos G. Michael,
Andrew W. Appel:
Machine Instruction Syntax and Semantics in Higher Order Logic.
CADE 2000: 7-24 |
53 | EE | Andrew W. Appel,
Amy P. Felty:
A Semantic Model of Types and Machine Instuctions for Proof-Carrying Code.
POPL 2000: 243-253 |
52 | EE | Zhong Shao,
Andrew W. Appel:
Efficient and safe-for-space closure conversion.
ACM Trans. Program. Lang. Syst. 22(1): 129-161 (2000) |
51 | EE | 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) |
50 | EE | Andrew W. Appel,
Edward W. Felten:
Technological access control interferes with noninfringing scholarship.
Commun. ACM 43(9): 21-23 (2000) |
1999 |
49 | EE | Andrew W. Appel,
Edward W. Felten:
Proof-Carrying Authentication.
ACM Conference on Computer and Communications Security 1999: 52-62 |
48 | | Andrew W. Appel,
Amy P. Felty:
Lightweight Lemmas in lambda-Prolog.
ICLP 1999: 411-425 |
47 | EE | Matthias Blume,
Andrew W. Appel:
Hierarchical modularity.
ACM Trans. Program. Lang. Syst. 21(4): 813-847 (1999) |
1998 |
46 | | Andrew W. Appel:
Modern Compiler Implementation in C
Cambridge University Press 1998 |
45 | | Andrew W. Appel:
Modern Compiler Implementation in Java
Cambridge University Press 1998 |
44 | | Andrew W. Appel:
Modern Compiler Implementation in ML
Cambridge University Press 1998 |
43 | EE | Jeffrey L. Korn,
Andrew W. Appel:
Traversal-Based Visualization of Data Structures.
INFOVIS 1998: 11-18 |
42 | | Andrew W. Appel:
SSA is Functional Programming.
SIGPLAN Notices 33(4): 17-20 (1998) |
1997 |
41 | | Andrew W. Appel:
Modern Compiler Implementation in C: Basic Techniques
Cambridge University Press 1997 |
40 | | Andrew W. Appel:
Modern Compiler Implementation in Java: Basic Techniques
Cambridge University Press 1997 |
39 | | Andrew W. Appel:
Modern Compiler Implementation in ML: Basic Techniques
Cambridge University Press 1997 |
38 | EE | Daniel C. Wang,
Andrew W. Appel,
Jeffrey L. Korn,
Christopher S. Serra:
The Zephyr Abstract Syntax Description Language.
DSL 1997: 213-228 |
37 | | Matthias Blume,
Andrew W. Appel:
Lambda-Splitting: A Higher-Order Approach to Cross-Module Optimizations.
ICFP 1997: 112-124 |
36 | | Andrew W. Appel,
Trevor Jim:
Shrinking lambda Expressions in Linear Time.
J. Funct. Program. 7(5): 515-540 (1997) |
1996 |
35 | EE | Lal George,
Andrew W. Appel:
Iterated Register Coalescing.
POPL 1996: 208-218 |
34 | EE | Lal George,
Andrew W. Appel:
Iterated Register Coalescing.
ACM Trans. Program. Lang. Syst. 18(3): 300-324 (1996) |
33 | | 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) |
32 | | Andrew W. Appel:
Intensional Equality ;=) for Continuations.
SIGPLAN Notices 31(2): 55-57 (1996) |
1995 |
31 | | Marcelo J. R. Gonçalves,
Andrew W. Appel:
Cache Performance of Fast-Allocating Programs.
FPCA 1995: 293-305 |
30 | | Zhong Shao,
Andrew W. Appel:
A Type-Based Compiler for Standard ML.
PLDI 1995: 116-129 |
29 | | Andrew P. Tolmach,
Andrew W. Appel:
A Debugger for Standard ML.
J. Funct. Program. 5(2): 155-200 (1995) |
1994 |
28 | EE | Zhong Shao,
Andrew W. Appel:
Space-Efficient Closure Representations.
LISP and Functional Programming 1994: 150-161 |
27 | EE | Zhong Shao,
John H. Reppy,
Andrew W. Appel:
Unrolling Lists.
LISP and Functional Programming 1994: 185-195 |
26 | | Andrew W. Appel,
David B. MacQueen:
Separate Compilation for Standard ML.
PLDI 1994: 13-23 |
25 | EE | Andrew W. Appel:
Axiomatic Bootstrapping: A Guide for Compiler Hackers.
ACM Trans. Program. Lang. Syst. 16(6): 1699-1718 (1994) |
24 | | Andrew W. Appel:
Loop Headers in Lambda-Calculus or CPS.
Lisp and Symbolic Computation 7(4): 337-343 (1994) |
1993 |
23 | | Zhong Shao,
Andrew W. Appel:
Smartest Recompilation.
POPL 1993: 439-450 |
22 | | Andrew W. Appel:
A Critique of Standard ML.
J. Funct. Program. 3(4): 391-429 (1993) |
1992 |
21 | | Andrew W. Appel:
Compiling with Continuations
Cambridge University Press 1992 |
20 | | Andrew W. Appel,
Zhong Shao:
Callee-Save Registers in Continuation-Passing Style.
Lisp and Symbolic Computation 5(3): 191-221 (1992) |
19 | EE | Andrew W. Appel:
Is POPL mathematics or science?
SIGPLAN Notices 27(4): 87-89 (1992) |
1991 |
18 | | Andrew W. Appel,
Kai Li:
Virtual Memory Primitives for User Programs.
ASPLOS 1991: 96-107 |
17 | | Andrew W. Appel,
David B. MacQueen:
Standard ML of New Jersey.
PLILP 1991: 1-13 |
16 | | Andrew P. Tolmach,
Andrew W. Appel:
Debuggable Concurrency Extensions for Standard ML.
Workshop on Parallel and Distributed Debugging 1991: 120-131 |
1990 |
15 | EE | Andrew P. Tolmach,
Andrew W. Appel:
Debugging Standard ML Without Reverse Engineering.
LISP and Functional Programming 1990: 1-12 |
14 | EE | Rafael Alonso,
Andrew W. Appel:
An Advisor for Flexible Working Sets.
SIGMETRICS 1990: 153-162 |
13 | | Andrew W. Appel:
A Runtime System.
Lisp and Symbolic Computation 3(4): 343-380 (1990) |
1989 |
12 | | Andrew W. Appel,
Trevor Jim:
Continuation-Passing, Closure-Passing Style.
POPL 1989: 293-302 |
11 | | Andrew W. Appel:
Runtime Tags Aren't Necessary.
Lisp and Symbolic Computation 2(2): 153-162 (1989) |
10 | | Andrew W. Appel:
Simple Generational Garbage Collection and Fast Allocation.
Softw., Pract. Exper. 19(2): 171-183 (1989) |
9 | | Andrew W. Appel:
Allocation without Locking.
Softw., Pract. Exper. 19(7): 703-705 (1989) |
1988 |
8 | EE | Andrew W. Appel:
Real-time concurrent collection on stock multiprocessors (with retrospective)
Best of PLDI 1988: 205-216 |
7 | | Andrew W. Appel,
John R. Ellis,
Kai Li:
Real-Time Concurrent Collection on Stock Multiprocessors
PLDI 1988: 11-20 |
6 | | Andrew W. Appel,
Guy J. Jacobson:
The World's Fastest Scrabble Program.
Commun. ACM 31(5): 572-578 (1988) |
5 | EE | 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) |
1987 |
4 | | Andrew W. Appel,
David B. MacQueen:
A Standard ML compiler.
FPCA 1987: 301-324 |
3 | | Andrew W. Appel:
Garbage Collection can be Faster than Stack Allocation.
Inf. Process. Lett. 25(4): 275-279 (1987) |
2 | | Andrew W. Appel,
Kenneth J. Supowit:
Generalization of the Sethi-Ullman Algorithm for Register Allocation.
Softw., Pract. Exper. 17(6): 417-421 (1987) |
1985 |
1 | | Andrew W. Appel:
Semantics-Directed Code Generation.
POPL 1985: 315-324 |