| Hits ?▲ |
Authors |
Title |
Venue |
Year |
Link |
Author keywords |
| 1 | Andrew W. Appel |
Verified Software Toolchain.  |
NASA Formal Methods  |
2012 |
DBLP DOI BibTeX RDF |
|
| 1 | Andrew W. Appel |
Security Seals on Voting Machines: A Case Study. |
ACM Trans. Inf. Syst. Secur. |
2011 |
DBLP DOI BibTeX RDF |
|
| 1 | Andrew W. Appel |
VeriSmall: Verified Smallfoot Shape Analysis. |
CPP |
2011 |
DBLP DOI BibTeX RDF |
|
| 1 | Gordon Stewart, Andrew W. Appel |
Local actions for a curry-style operational semantics. |
PLPV |
2011 |
DBLP DOI BibTeX RDF |
|
| 1 | Andrew W. Appel |
Verified Software Toolchain - (Invited Talk). |
ESOP |
2011 |
DBLP DOI BibTeX RDF |
|
| 1 | 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. |
2010 |
DBLP DOI BibTeX RDF |
|
| 1 | Aquinas Hobor, Robert Dockins, Andrew W. Appel |
A theory of indirection via approximation. |
POPL |
2010 |
DBLP DOI BibTeX RDF |
indirection theory, step-indexed models |
| 1 | Aquinas Hobor, Robert Dockins, Andrew W. Appel |
A Logical Mix of Approximation and Separation. |
APLAS |
2010 |
DBLP DOI BibTeX RDF |
|
| 1 | Christian J. Bell, Andrew W. Appel, David Walker |
Concurrent Separation Logic for Pipelined Parallelization. |
SAS |
2010 |
DBLP DOI BibTeX RDF |
|
| 1 | Sandrine Blazy, Benoît Robillard, Andrew W. Appel |
Formal Verification of Coalescing Graph-Coloring Register Allocation. |
ESOP |
2010 |
DBLP DOI BibTeX RDF |
|
| 1 | Robert Dockins, Aquinas Hobor, Andrew W. Appel |
A Fresh Look at Separation Algebras and Share Accounting. |
APLAS |
2009 |
DBLP DOI BibTeX RDF |
|
| 1 | Robert Dockins, Andrew W. Appel, Aquinas Hobor |
Multimodal Separation Logic for Reasoning About Operational Semantics. |
Electr. Notes Theor. Comput. Sci. |
2008 |
DBLP DOI BibTeX RDF |
|
| 1 | Aquinas Hobor, Andrew W. Appel, Francesco Zappa Nardelli |
Oracle Semantics for Concurrent Separation Logic. |
ESOP |
2008 |
DBLP DOI BibTeX RDF |
|
| 1 | Andrew W. Appel, Xavier Leroy |
A List-machine Benchmark for Mechanized Metatheory: (Extended Abstract). |
Electr. Notes Theor. Comput. Sci. |
2007 |
DBLP DOI BibTeX RDF |
|
| 1 | Andrew W. Appel, Sandrine Blazy |
Separation Logic for Small-step Cminor |
CoRR |
2007 |
DBLP BibTeX RDF |
|
| 1 | 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 |
DBLP DOI BibTeX RDF |
impredicative polymorphism, mutable references, recursive types, Kripke models |
| 1 | Andrew W. Appel, Sandrine Blazy |
Separation Logic for Small-Step cminor. |
TPHOLs |
2007 |
DBLP DOI BibTeX RDF |
|
| 1 | Andrew W. Appel |
Compiling with Continuations (corr. version). |
|
2006 |
RDF |
|
| 1 | Gang Tan, Andrew W. Appel |
A Compositional Logic for Control Flow. |
VMCAI |
2006 |
DBLP DOI BibTeX RDF |
|
| 1 | Andrew W. Appel, Amy P. Felty |
Polymorphic lemmas and definitions in Lambda Prolog and Twelf |
CoRR |
2004 |
DBLP BibTeX RDF |
|
| 1 | Andrew W. Appel, Amy P. Felty |
Polymorphic Lemmas and Definitions in lambda-Prolog and Twelf. |
TPLP |
2004 |
DBLP DOI BibTeX RDF |
|
| 1 | Andrew W. Appel, Amy P. Felty |
Dependent types ensure partial correctness of theorem provers. |
J. Funct. Program. |
2004 |
DBLP DOI BibTeX RDF |
|
| 1 | Andrew W. Appel |
Social processes and proofs of theorems and programs, revisited. |
PLDI |
2004 |
DBLP DOI BibTeX RDF |
|
| 1 | Gang Tan, Andrew W. Appel, Kedar N. Swadi, Dinghao Wu |
Construction of a Semantic Model for a Typed Assembly Language. |
VMCAI |
2004 |
DBLP DOI BibTeX RDF |
|
| 1 | Lujo Bauer, Andrew W. Appel, Edward W. Felten |
Mechanisms for secure modular programming in Java. |
Softw., Pract. Exper. |
2003 |
DBLP DOI BibTeX RDF |
|
| 1 | Andrew W. Appel, Neophytos G. Michael, Aaron Stump, Roberto Virga |
A Trustworthy Proof Checker. |
J. Autom. Reasoning |
2003 |
DBLP DOI BibTeX RDF |
proof checker, proof-carrying code |
| 1 | Sudhakar Govindavajhala, Andrew W. Appel |
Using Memory Errors to Attack a Virtual Machine. |
IEEE Symposium on Security and Privacy |
2003 |
DBLP DOI BibTeX RDF |
|
| 1 | Juan Chen, Dinghao Wu, Andrew W. Appel, Hai Fang |
A provably sound TAL for back-end optimization. |
PLDI |
2003 |
DBLP DOI BibTeX RDF |
proof-carrying code, typed assembly language |
| 1 | Lujo Bauer, Michael A. Schneider, Edward W. Felten, Andrew W. Appel |
Access Control on the Web Using Proof-carrying Authorization. |
DISCEX |
2003 |
DBLP DOI BibTeX RDF |
|
| 1 | Dinghao Wu, Andrew W. Appel, Aaron Stump |
Foundational proof checkers with small witnesses. |
PPDP |
2003 |
DBLP DOI BibTeX RDF |
proof checker, proof-carrying code |
| 1 | Eunyoung Lee, Andrew W. Appel |
Policy-enforced linking of untrusted components. |
ESEC / SIGSOFT FSE |
2003 |
DBLP DOI BibTeX RDF |
proof-carrying, linking, formal logic, component composition |
| 1 | Andrew W. Appel, Jens Palsberg |
Modern Compiler Implementation in Java, 2nd edition. |
|
2002 |
RDF |
|
| 1 | 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 |
DBLP DOI BibTeX RDF |
heap traversal, locality based graph traversal, object co-allocation, prolific types, Java, locality, garbage collection, memory management, JVM, memory allocation, run-time systems, object placement |
| 1 | Amal J. Ahmed, Andrew W. Appel, Roberto Virga |
A Stratified Semantics of General References A Stratified Semantics of General References. |
LICS |
2002 |
DBLP DOI BibTeX RDF |
|
| 1 | Andrew W. Appel, David A. McAllester |
An indexed model of recursive types for foundational proof-carrying code. |
ACM Trans. Program. Lang. Syst. |
2001 |
DBLP DOI BibTeX RDF |
|
| 1 | Andrew W. Appel, Lal George |
Optimal Spilling for CISC Machines with Few Registers. |
PLDI |
2001 |
DBLP DOI BibTeX RDF |
|
| 1 | Daniel C. Wang, Andrew W. Appel |
Type-preserving garbage collectors. |
POPL |
2001 |
DBLP DOI BibTeX RDF |
|
| 1 | Andrew W. Appel |
Foundational Proof-Carrying Code. |
LICS |
2001 |
DBLP DOI BibTeX RDF |
|
| 1 | Dan S. Wallach, Andrew W. Appel, Edward W. Felten |
SAFKASI: a security mechanism for language-based systems. |
ACM Trans. Softw. Eng. Methodol. |
2000 |
DBLP DOI BibTeX RDF |
security-passing style, Java, Internet, WWW, access control, applets, stack inspection |
| 1 | Zhong Shao, Andrew W. Appel |
Efficient and safe-for-space closure conversion. |
ACM Trans. Program. Lang. Syst. |
2000 |
DBLP DOI BibTeX RDF |
callee-save registers, closure representation, heap-based compilation, space safety, compiler optimization, flow analysis, closure conversion |
| 1 | Andrew W. Appel, Edward W. Felten |
Technological access control interferes with noninfringing scholarship. |
Commun. ACM |
2000 |
DBLP DOI BibTeX RDF |
|
| 1 | Neophytos G. Michael, Andrew W. Appel |
Machine Instruction Syntax and Semantics in Higher Order Logic. |
CADE |
2000 |
DBLP DOI BibTeX RDF |
|
| 1 | Andrew W. Appel, Amy P. Felty |
A Semantic Model of Types and Machine Instuctions for Proof-Carrying Code. |
POPL |
2000 |
DBLP DOI BibTeX RDF |
|
| 1 | Matthias Blume, Andrew W. Appel |
Hierarchical modularity. |
ACM Trans. Program. Lang. Syst. |
1999 |
DBLP DOI BibTeX RDF |
compilation management, name visibility, modularity, modules, linking, program structure |
| 1 | Andrew W. Appel, Amy P. Felty |
Lightweight Lemmas in lambda-Prolog. |
ICLP |
1999 |
DBLP BibTeX RDF |
|
| 1 | Andrew W. Appel, Edward W. Felten |
Proof-Carrying Authentication. |
ACM Conference on Computer and Communications Security |
1999 |
DBLP DOI BibTeX RDF |
|
| 1 | Andrew W. Appel |
SSA is Functional Programming. |
SIGPLAN Notices |
1998 |
DBLP DOI BibTeX RDF |
|
| 1 | Andrew W. Appel |
Modern Compiler Implementation in Java |
|
1998 |
RDF |
|
| 1 | Andrew W. Appel |
Modern Compiler Implementation in C |
|
1998 |
RDF |
|
| 1 | Andrew W. Appel |
Modern Compiler Implementation in ML |
|
1998 |
RDF |
|
| 1 | Jeffrey L. Korn, Andrew W. Appel |
Traversal-Based Visualization of Data Structures. |
INFOVIS |
1998 |
DBLP DOI BibTeX RDF |
|
| 1 | Andrew W. Appel, Trevor Jim |
Shrinking lambda Expressions in Linear Time. |
J. Funct. Program. |
1997 |
DBLP BibTeX RDF |
|
| 1 | Andrew W. Appel |
Modern Compiler Implementation in ML: Basic Techniques |
|
1997 |
RDF |
|
| 1 | Andrew W. Appel |
Modern Compiler Implementation in Java: Basic Techniques |
|
1997 |
RDF |
|
| 1 | Andrew W. Appel |
Modern Compiler Implementation in C: Basic Techniques |
|
1997 |
RDF |
|
| 1 | Matthias Blume, Andrew W. Appel |
Lambda-Splitting: A Higher-Order Approach to Cross-Module Optimizations. |
ICFP |
1997 |
DBLP DOI BibTeX RDF |
|
| 1 | Daniel C. Wang, Andrew W. Appel, Jeffrey L. Korn, Christopher S. Serra |
The Zephyr Abstract Syntax Description Language. |
DSL |
1997 |
DBLP BibTeX RDF |
|
| 1 | Andrew W. Appel |
Intensional Equality ;=) for Continuations. |
SIGPLAN Notices |
1996 |
DBLP DOI BibTeX RDF |
|
| 1 | Lal George, Andrew W. Appel |
Iterated Register Coalescing. |
ACM Trans. Program. Lang. Syst. |
1996 |
DBLP DOI BibTeX RDF |
copy propagation, graph coloring, register allocation, register coalescing |
| 1 | Andrew W. Appel, Zhong Shao |
Empirical and Analytic Study of Stack Versus Heap Cost for Languages with Closures. |
J. Funct. Program. |
1996 |
DBLP DOI BibTeX RDF |
|
| 1 | Lal George, Andrew W. Appel |
Iterated Register Coalescing. |
POPL |
1996 |
DBLP DOI BibTeX RDF |
|
| 1 | Andrew P. Tolmach, Andrew W. Appel |
A Debugger for Standard ML. |
J. Funct. Program. |
1995 |
DBLP DOI BibTeX RDF |
|
| 1 | Zhong Shao, Andrew W. Appel |
A Type-Based Compiler for Standard ML. |
PLDI |
1995 |
DBLP DOI BibTeX RDF |
Standard ML |
| 1 | Marcelo J. R. Gonçalves, Andrew W. Appel |
Cache Performance of Fast-Allocating Programs. |
FPCA |
1995 |
DBLP BibTeX RDF |
|
| 1 | Andrew W. Appel |
Axiomatic Bootstrapping: A Guide for Compiler Hackers. |
ACM Trans. Program. Lang. Syst. |
1994 |
DBLP DOI BibTeX RDF |
bootstrapping |
| 1 | Andrew W. Appel |
Loop Headers in Lambda-Calculus or CPS. |
Lisp and Symbolic Computation |
1994 |
DBLP BibTeX RDF |
|
| 1 | Andrew W. Appel, David B. MacQueen |
Separate Compilation for Standard ML. |
PLDI |
1994 |
DBLP DOI BibTeX RDF |
ML |
| 1 | Zhong Shao, John H. Reppy, Andrew W. Appel |
Unrolling Lists. |
LISP and Functional Programming |
1994 |
DBLP DOI BibTeX RDF |
|
| 1 | Zhong Shao, Andrew W. Appel |
Space-Efficient Closure Representations. |
LISP and Functional Programming |
1994 |
DBLP DOI BibTeX RDF |
Standard ML |
| 1 | Andrew W. Appel |
A Critique of Standard ML. |
J. Funct. Program. |
1993 |
DBLP DOI BibTeX RDF |
|
| 1 | Zhong Shao, Andrew W. Appel |
Smartest Recompilation. |
POPL |
1993 |
DBLP DOI BibTeX RDF |
ML |
| 1 | Andrew W. Appel |
Is POPL mathematics or science? |
SIGPLAN Notices |
1992 |
DBLP DOI BibTeX RDF |
|
| 1 | Andrew W. Appel, Zhong Shao |
Callee-Save Registers in Continuation-Passing Style. |
Lisp and Symbolic Computation |
1992 |
DBLP BibTeX RDF |
|
| 1 | Andrew W. Appel |
Compiling with Continuations |
|
1992 |
RDF |
|
| 1 | Andrew P. Tolmach, Andrew W. Appel |
Debuggable Concurrency Extensions for Standard ML. |
Workshop on Parallel and Distributed Debugging |
1991 |
DBLP DOI BibTeX RDF |
|
| 1 | Andrew W. Appel, Kai Li |
Virtual Memory Primitives for User Programs. |
ASPLOS |
1991 |
DBLP DOI BibTeX RDF |
|
| 1 | Andrew W. Appel, David B. MacQueen |
Standard ML of New Jersey. |
PLILP |
1991 |
DBLP DOI BibTeX RDF |
|
| 1 | Andrew W. Appel |
A Runtime System. |
Lisp and Symbolic Computation |
1990 |
DBLP BibTeX RDF |
|
| 1 | Andrew P. Tolmach, Andrew W. Appel |
Debugging Standard ML Without Reverse Engineering. |
LISP and Functional Programming |
1990 |
DBLP DOI BibTeX RDF |
|
| 1 | Rafael Alonso, Andrew W. Appel |
An Advisor for Flexible Working Sets. |
SIGMETRICS |
1990 |
DBLP DOI BibTeX RDF |
|
| 1 | Andrew W. Appel |
Simple Generational Garbage Collection and Fast Allocation. |
Softw., Pract. Exper. |
1989 |
DBLP DOI BibTeX RDF |
|
| 1 | Andrew W. Appel |
Allocation without Locking. |
Softw., Pract. Exper. |
1989 |
DBLP DOI BibTeX RDF |
|
| 1 | Andrew W. Appel, Aage Bendiksen |
Vectorized garbage collection. |
The Journal of Supercomputing |
1989 |
DBLP DOI BibTeX RDF |
|
| 1 | Andrew W. Appel |
Runtime Tags Aren't Necessary. |
Lisp and Symbolic Computation |
1989 |
DBLP BibTeX RDF |
|
| 1 | Andrew W. Appel, Trevor Jim |
Continuation-Passing, Closure-Passing Style. |
POPL |
1989 |
DBLP DOI BibTeX RDF |
ML |
| 1 | Andrew W. Appel |
Simulating digital circuits with one bit per wire. |
IEEE Trans. on CAD of Integrated Circuits and Systems |
1988 |
DBLP DOI BibTeX RDF |
|
| 1 | Andrew W. Appel, Guy J. Jacobson |
The World's Fastest Scrabble Program. |
Commun. ACM |
1988 |
DBLP DOI BibTeX RDF |
|
| 1 | Andrew W. Appel |
Real-time concurrent collection on stock multiprocessors (with retrospective) |
Best of PLDI |
1988 |
DBLP DOI BibTeX RDF |
|
| 1 | Andrew W. Appel, John R. Ellis, Kai Li |
Real-Time Concurrent Collection on Stock Multiprocessors. |
PLDI |
1988 |
DBLP DOI BibTeX RDF |
LISP, Modula-2 |
| 1 | Andrew W. Appel |
Garbage Collection can be Faster than Stack Allocation. |
Inf. Process. Lett. |
1987 |
DBLP DOI BibTeX RDF |
|
| 1 | Andrew W. Appel, Kenneth J. Supowit |
Generalization of the Sethi-Ullman Algorithm for Register Allocation. |
Softw., Pract. Exper. |
1987 |
DBLP DOI BibTeX RDF |
|
| 1 | Andrew W. Appel, David B. MacQueen |
A Standard ML compiler. |
FPCA |
1987 |
DBLP DOI BibTeX RDF |
|
| 1 | Andrew W. Appel |
Semantics-Directed Code Generation. |
POPL |
1985 |
DBLP DOI BibTeX RDF |
|
![[Valid RSS]](Pics/valid-rss.png "Validate my RSS feed")