| Year |
Citation |
Score |
| 2018 |
Cao Q, Beringer L, Gruetter S, Dodds J, Appel AW. VST-Floyd: A Separation Logic Tool to Verify Correctness of C Programs Journal of Automated Reasoning. 61: 367-422. DOI: 10.1007/s10817-018-9457-5 |
0.32 |
|
| 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 |
0.602 |
|
| 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 |
0.343 |
|
| 2015 |
Appel AW. Verification of a cryptographic primitive: SHA-256 7 Acm Transactions On Programming Languages and Systems. 37. DOI: 10.1145/2701415 |
0.353 |
|
| 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 |
0.392 |
|
| 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 |
0.799 |
|
| 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 |
0.447 |
|
| 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 |
0.719 |
|
| 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 |
0.486 |
|
| 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 |
0.429 |
|
| 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 |
0.495 |
|
| 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 |
0.741 |
|
| 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 |
0.696 |
|
| 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 |
0.773 |
|
| 2009 |
Appel A. Session details: Verification Sigplan Notices. 44. DOI: 10.1145/3263686 |
0.303 |
|
| 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 |
0.775 |
|
| 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 |
0.71 |
|
| 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 |
0.804 |
|
| 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 |
0.447 |
|
| 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 |
0.323 |
|
| 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. |
0.503 |
|
| 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. |
0.46 |
|
| 2004 |
Appel AW, Felty AP. Dependent types ensure partial correctness of theorem provers Journal of Functional Programming. 14: 3-19. DOI: 10.1017/S0956796803004921 |
0.437 |
|
| 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. |
0.791 |
|
| 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 |
0.699 |
|
| 2003 |
Appel AW. Foundational proof-carrying code Foundations of Intrusion Tolerant Systems, Oasis 2003. 25-34. DOI: 10.1109/FITS.2003.1264926 |
0.306 |
|
| 2003 |
Appel AW, Michael N, Stump A, Virga R. A Trustworthy Proof Checker Journal of Automated Reasoning. 31: 231-260. |
0.406 |
|
| 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. |
0.427 |
|
| 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. |
0.389 |
|
| 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 |
0.774 |
|
| 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 |
0.344 |
|
| 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. |
0.471 |
|
| 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. |
0.463 |
|
| 1999 |
Blume M, Appel AW. Hierarchical modularity Acm Transactions On Programming Languages and Systems. 21: 813-847. |
0.328 |
|
| 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. |
0.316 |
|
| 1995 |
Tolmhch A, Appel AW. A Debugger for standard ML Journal of Functional Programming. 5: 155-200. DOI: 10.1017/S0956796800001313 |
0.387 |
|
| 1994 |
Shao Z, Reppy JH, Appel AW. Unrolling lists Proceedings of the Acm Conference On Lisp and Functional Programming. 7: 185-195. |
0.342 |
|
| 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. |
0.341 |
|
| 1993 |
Appel AW. A critique of Standard ML Journal of Functional Programming. 3: 391-429. DOI: 10.1017/S0956796800000836 |
0.305 |
|
| 1993 |
Appel AW, Harper R. Special Issue on ML Journal of Functional Programming. 3: 389. DOI: 10.1017/S0956796800000812 |
0.339 |
|
| 1993 |
Shao Z, Appel AW. Smartest recompilation Conference Record of the Annual Acm Symposium On Principles of Programming Languages. 439-450. |
0.342 |
|
| 1989 |
Appel AW. Runtime tags aren't necessary Lisp and Symbolic Computation. 2: 153-162. DOI: 10.1007/BF01811537 |
0.32 |
|
| Show low-probability matches. |