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 |