Andrew Appel - Publications

Affiliations: 
Computer Science Princeton University, Princeton, NJ 
Area:
Software verification, computer security, programming languages, compilers.

83 high-probability publications. We are testing a new system for linking publications to authors. You can help! If you notice any inaccuracies, please sign in and mark papers as correct or incorrect matches. If you identify any major omissions or other inaccuracies in the publication list, please let us know.

Year Citation  Score
2017 Appel AW, Beringer L, Chlipala A, Pierce BC, Shao Z, Weirich S, Zdancewic S. Position paper: the science of deep specification. Philosophical Transactions. Series a, Mathematical, Physical, and Engineering Sciences. 375. PMID 28871056 DOI: 10.1098/Rsta.2016.0331  1
2015 Appel AW. Verification of a cryptographic primitive: SHA-256 (abstract) Proceedings of the Acm Sigplan Conference On Programming Language Design and Implementation (Pldi). 2015: 153. DOI: 10.1145/2737924.2774972  1
2015 Appel AW. Verification of a cryptographic primitive: SHA-256 7 Acm Transactions On Programming Languages and Systems. 37. DOI: 10.1145/2701415  1
2015 Stewart G, Beringer L, Cuellar S, Appel AW. Compositional CompCert Acm Sigplan Notices. 50: 275-287. DOI: 10.1145/2676726.2676985  1
2014 Kroll JA, Stewart G, Appel AW. Portable software fault isolation Proceedings of the Computer Security Foundations Workshop. 2014: 18-32. DOI: 10.1109/CSF.2014.10  1
2014 Appel AW, Dockins R, Hobor A, Beringer L, Dodds J, Stewart G, Blazy S, Leroy X. Program logics for certified compilers Program Logics For Certified Compilers. 1-451. DOI: 10.1017/CBO9781107256552  1
2014 Beringer L, Stewart G, Dockins R, Appel AW. Verified compilation for shared-memory C Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). 8410: 107-127. DOI: 10.1007/978-3-642-54833-8_7  1
2013 Dodds J, Appel AW. Mostly sound type system improves a foundational program verifier Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). 8307: 17-32. DOI: 10.1007/978-3-319-03545-1_2  1
2012 Stewart G, Beringer L, Appel AW. Verified heap theorem prover by paramodulation Proceedings of the Acm Sigplan International Conference On Functional Programming, Icfp. 3-14. DOI: 10.1145/2364527.2364531  1
2012 Appel AW, Dockins R, Leroy X. A list-machine benchmark for mechanized metatheory Journal of Automated Reasoning. 49: 453-491. DOI: 10.1007/S10817-011-9226-1  1
2012 Amtoft T, Dodds J, Zhang Z, Appel A, Beringer L, Hatcliff J, Ou X, Cousino A. A certificate infrastructure for machine-checked proofs of conditional information flow Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). 7215: 369-389. DOI: 10.1007/978-3-642-28641-4_20  1
2011 Appel AW. Security seals on voting machines: A case study Acm Transactions On Information and System Security. 14. DOI: 10.1145/2019599.2019603  1
2011 Stewart G, Appel AW. Local actions for a curry-style operational semantics Plpv'11 - Proceedings of the 5th Acm Workshop On Programming Languages Meets Program Verification. 31-42. DOI: 10.1145/1929529.1929535  1
2011 Appel AW. VeriSmall: Verified smallfoot shape analysis Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). 7086: 231-246. DOI: 10.1007/978-3-642-25379-9_18  1
2011 Appel AW. Verified software toolchain (Invited talk) Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). 6602: 1-17. DOI: 10.1007/978-3-642-19718-5_1  1
2010 Ahmed A, Appel AW, Richards CD, Swadi KN, Tan G, Wang DC. Semantic foundations for typed assembly languages Acm Transactions On Programming Languages and Systems. 32. DOI: 10.1145/1709093.1709094  1
2010 Hobor A, Dockins R, Appel AW. A theory of indirection via approximation Conference Record of the Annual Acm Symposium On Principles of Programming Languages. 171-184. DOI: 10.1145/1706299.1706322  1
2010 Hobor A, Dockins R, Appel AW. A logical mix of approximation and separation Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). 6461: 439-454. DOI: 10.1007/978-3-642-17164-2_30  1
2010 Bell CJ, Appel AW, Walker D. Concurrent separation logic for pipelined parallelization Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). 6337: 151-166. DOI: 10.1007/978-3-642-15769-1_10  1
2010 Blazy S, Robillard B, Appel AW. Formal verification of coalescing graph-coloring register allocation Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). 6012: 145-164. DOI: 10.1007/978-3-642-11957-6_9  1
2009 Dockins R, Hobor A, Appel AW. A fresh look at separation algebras and share accounting Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). 5904: 161-177. DOI: 10.1007/978-3-642-10672-9_13  1
2008 Dockins R, Appel AW, Hobor A. Multimodal Separation Logic for Reasoning About Operational Semantics Electronic Notes in Theoretical Computer Science. 218: 5-20. DOI: 10.1016/J.Entcs.2008.10.002  1
2008 Hobor A, Appel AW, Nardelli FZ. Oracle semantics for concurrent separation logic Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). 4960: 353-367. DOI: 10.1007/978-3-540-78739-6_27  1
2007 Appel AW, Melliès PA, Richards CD, Vouillon J. A very modal model of a modern, major, general type system Conference Record of the Annual Acm Symposium On Principles of Programming Languages. 109-122. DOI: 10.1145/1190216.1190235  1
2007 Appel AW, Leroy X. A List-machine Benchmark for Mechanized Metatheory. (Extended Abstract) Electronic Notes in Theoretical Computer Science. 174: 95-108. DOI: 10.1016/j.entcs.2007.01.020  1
2007 Appel AW, Blazy S. Separation logic for small-step Cminor Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). 4732: 5-21.  1
2006 Tan G, Appel AW. A compositional logic for control flow Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). 3855: 80-94.  1
2004 Appel AW, Ellis JR, Li K. Real-time concurrent collection on stock multiprocessors Acm Sigplan Notices. 39: 207-216. DOI: 10.1145/989393.989417  1
2004 Appel AW, Felty AP. Dependent types ensure partial correctness of theorem provers Journal of Functional Programming. 14: 3-19. DOI: 10.1017/S0956796803004921  1
2004 Appel AW, Felty AP. Polymorphic lemmas and definitions in λProlog and Twelf Theory and Practice of Logic Programming. 4: 1-39.  1
2004 Tan G, Appel AW, Swadi KN, Wu D. Construction of a semantic model for a typed assembly language Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). 2937: 30-43.  1
2003 Govindavajhala S, Appel AW. Using memory errors to attack a virtual machine Proceedings of the Ieee Computer Society Symposium On Research in Security and Privacy. 154-165. DOI: 10.1109/SECPRI.2003.1199334  1
2003 Appel AW. Foundational proof-carrying code Foundations of Intrusion Tolerant Systems, Oasis 2003. 25-34. DOI: 10.1109/FITS.2003.1264926  1
2003 Bauer L, Schneider MA, Felten EW, Appel AW. Access control on the Web using proof-carrying authorization Proceedings - Darpa Information Survivability Conference and Exposition, Discex 2003. 2: 117-119. DOI: 10.1109/DISCEX.2003.1194942  1
2003 Bauer L, Appel AW, Felten EW. Mechanisms for secure modular programming in Java Software - Practice and Experience. 33: 461-480. DOI: 10.1002/Spe.516  1
2003 Chen J, Wu D, Appel AW, Fang H. A provably sound TAL for back-end optimization Proceedings of the Acm Sigplan Conference On Programming Language Design and Implementation (Pldi). 208-219.  1
2003 Lee E, Appel AW. Policy-Enforced Linking of Untrusted Components (Extended Abstract) Proceedings of the Joint European Software Engineering Conference (Esec) and Sigsoft Symposium On the Foundations of Software Engineering (Fse-11). 371-374.  1
2003 Appel AW, Michael N, Stump A, Virga R. A Trustworthy Proof Checker Journal of Automated Reasoning. 31: 231-260.  1
2003 Wu D, Appel AW, Stump A. Foundational Proof Checkers with Small Witnesses Proceedings of the Acm Sigplan Conference On Principles and Practice of Declarative Programming. 5: 264-274.  1
2002 Shuf Y, Gupta M, Franke H, Appel A, Pal Singh J. Creating and preserving locality of Java applications at allocation and garbage collection times Proceedings of the Conference On Object-Oriented Programming Systems, Languages, and Applications, Oopsla. 13-25.  1
2002 Ahmed AJ, Appel AW, Virga R. A stratified semantics of general references embeddable in higher-order logic Proceedings - Symposium On Logic in Computer Science. 75-86.  1
2001 Appel AW, McAllester D. An indexed model of recursive types for foundational proof-carrying code Acm Transactions On Programming Languages and Systems. 23: 657-683. DOI: 10.1145/504709.504712  1
2001 Appel AW, Swadi KN, Virga R. Efficient substitution in hoare logic expressions Electronic Notes in Theoretical Computer Science. 41: 35-49. DOI: 10.1016/S1571-0661(04)80872-7  1
2001 Appel AW, George L. Optimal spilling for CISC machines with few registers Sigplan Notices (Acm Special Interest Group On Programming Languages). 36: 243-253.  1
2001 Wang DC, Appel AW. Type-preserving garbage collectors Sigplan Notices (Acm Special Interest Group On Programming Languages). 36: 166-178.  1
2000 Wallach DS, Appel AW, Felten EW. SAFKASI: A security mechanism for language-based systems Acm Transactions On Software Engineering and Methodology. 9: 341-378. DOI: 10.1145/363516.363520  1
2000 Appel AW, Felty AP. Semantic model of types and machine instructions for proof-carrying code Conference Record of the Annual Acm Symposium On Principles of Programming Languages. 243-253.  1
2000 Shao Z, Appel AW. Efficient and safe-for-space closure conversion Acm Transactions On Programming Languages and Systems. 22: 129-161.  1
2000 Michael NG, Appel AW. Machine instruction syntax and semantics in higher order logic Lecture Notes in Artificial Intelligence (Subseries of Lecture Notes in Computer Science). 1831: 7-24.  1
2000 Appel AW, Felten EW. Technological access control interferes with noninfringing scholarship Communications of the Acm. 43: 21-23.  1
1999 Appel AW, Felten EW. Proof-carrying authentication Proceedings of the Acm Conference On Computer and Communications Security. 52-62.  1
1999 Blume M, Appel AW. Hierarchical modularity Acm Transactions On Programming Languages and Systems. 21: 813-847.  1
1998 Korn JL, Appel AW. Traversal-based visualization of data structures Proceedings of the Ieee Symposium On Information Visualization. 11-18.  1
1998 Appel AW. SSA is Functional Programming Sigplan Notices (Acm Special Interest Group On Programming Languages). 33: 17-20.  1
1997 Blume M, Appel AW. Lambda-Splitting: A Higher-Order Approach to Cross-Module Optimizations Sigplan Notices (Acm Special Interest Group On Programming Languages). 32: 112-124.  1
1997 Appel AW, Jim T. Shrinking lambda expressions in linear time Journal of Functional Programming. 7: 515-540.  1
1996 George L, Appel AW. Iterated Register Coalescing Acm Transactions On Programming Languages and Systems. 18: 300-324.  1
1996 Appel AW. Intensional Equality ;= for Continuations Sigplan Notices (Acm Special Interest Group On Programming Languages). 31: 55-57.  1
1996 Appel AW, Shao Z. Empirical and analytic study of stack versus heap cost for languages with closures Journal of Functional Programming. 6: 47-74.  1
1995 Tolmhch A, Appel AW. A Debugger for standard ML Journal of Functional Programming. 5: 155-200. DOI: 10.1017/S0956796800001313  1
1995 Goncalves MJR, Appel AW. Cache performance of fast-allocating programs . 293-305.  1
1994 Appel AW. Axiomatic bootstrapping: a guide for compiler hackers Acm Transactions On Programming Languages and Systems. 16: 1699-1718. DOI: 10.1145/197320.197336  1
1994 Appel AW. Loop headers in λ-calculus or CPS Lisp and Symbolic Computation. 7: 337-343. DOI: 10.1007/BF01018615  1
1994 Shao Z, Appel AW. Space-efficient closure representations Proceedings of the Acm Conference On Lisp and Functional Programming. 7: 150-161.  1
1994 Appel AW, MacQueen DB. Separate compilation for standard ML Proceedings of the Acm Sigplan Conference On Programming Language Design and Implementation (Pldi). 13-23.  1
1994 Shao Z, Reppy JH, Appel AW. Unrolling lists Proceedings of the Acm Conference On Lisp and Functional Programming. 7: 185-195.  1
1993 Appel AW. A critique of Standard ML Journal of Functional Programming. 3: 391-429. DOI: 10.1017/S0956796800000836  1
1993 Appel AW, Harper R. Special Issue on ML Journal of Functional Programming. 3: 389. DOI: 10.1017/S0956796800000812  1
1993 Shao Z, Appel AW. Smartest recompilation Conference Record of the Annual Acm Symposium On Principles of Programming Languages. 439-450.  1
1992 Appel AW, Shao Z. Callee-save registers in continuation-passing style Lisp and Symbolic Computation. 5: 191-221. DOI: 10.1007/BF01807505  1
1991 Appel AW, Li K. Virtual memory primitives for user programs International Conference On Architectural Support For Programming Languages and Operating Systems - Asplos. 26: 96-107.  1
1990 Appel AW. A runtime system Lisp and Symbolic Computation. 3: 343-380. DOI: 10.1007/BF01807697  1
1990 Tolmach AP, Appel AW. Debugging standard ML without reverse engineering . 1-12.  1
1990 Alonso R, Appel AW. Advisor for flexible working sets . 153-162.  1
1989 Appel AW. Runtime tags aren't necessary Lisp and Symbolic Computation. 2: 153-162. DOI: 10.1007/BF01811537  1
1989 Appel AW, Bendiksen A. Vectorized garbage collection The Journal of Supercomputing. 3: 151-160. DOI: 10.1007/BF00127826  1
1989 Appel AW, Jim T. Continuation-passing, closure-passing style . 293-302.  1
1989 Appel AW. Simple generational garbage collection and fast allocation Software - Practice and Experience. 19: 171-183.  1
1988 Appel AW, Jacobson GJ. WORLD'S FASTEST SCRABBLE PROGRAM Communications of the Acm. 31: 572-578. DOI: 10.1145/42411.42420  1
1988 Appel AW. Simulating Digital Circuits with One Bit Per Wire Ieee Transactions On Computer-Aided Design of Integrated Circuits and Systems. 7: 987-993. DOI: 10.1109/43.7796  1
1987 Appel AW. Garbage collection can be faster than stack allocation Information Processing Letters. 25: 275-279. DOI: 10.1016/0020-0190(87)90175-X  1
1987 Appel AW, Supowit KJ. GENERALIZATIONS OF THE SETHI-ULLMAN ALGORITHM FOR REGISTER ALLOCATION Software - Practice and Experience. 17: 417-421. DOI: 10.1002/spe.4380170607  1
1985 Appel AW. SEMANTICS-DIRECTED CODE GENERATION Conference Record of the Annual Acm Symposium On Principles of Programming Languages. 315-324.  1
Show low-probability matches.