Stop the war!Остановите войну!
for scientists:
default search action
Google
Google Scholar
Semantic Scholar
Internet Archive Scholar
CiteSeerX
ORCIDAndrew W. Appel
Person information
- affiliation: Princeton University, USA
Refine list
refinements active!
zoomed in on ?? of ?? records
view refined list in
export refined list as
showing all ?? records
2020 – today
- 2023
[j44]Qinshi Wang
, Andrew W. Appel:
A Solver for Arrays with Concatenation. J. Autom. Reason. 67(1): 4 (2023)- [j43]Andrew W. Appel, Xavier Leroy:
Efficient Extensional Binary Tries. J. Autom. Reason. 67(1): 8 (2023) - [c73]Qinshi Wang, Mengying Pan, Shengyi Wang, Ryan Doenges, Lennart Beringer, Andrew W. Appel:
Foundational Verification of Stateful P4 Packet Processing. ITP 2023: 32:1-32:20 - [c72]Mohit Tekriwal, Andrew W. Appel, Ariel E. Kellison, David Bindel, Jean-Baptiste Jeannin:
Verified Correctness, Accuracy, and Convergence of a Stationary Iterative Linear Solver: Jacobi Method. CICM 2023: 206-221 - 2022
- [c71]Ariel E. Kellison, Andrew W. Appel:
Verified Numerical Methods for Ordinary Differential Equations. NSV/FoMLAS@CAV 2022: 147-163 - [c70]Joshua M. Cohen, Qinshi Wang, Andrew W. Appel:
Verified Erasure Correction in Coq with MathComp and VST. CAV (2) 2022: 272-292 - [c69]Andrew W. Appel:
Coq's vibrant ecosystem for verification engineering (invited talk). CPP 2022: 2-11 - 2021
- [j42]Lennart Beringer, Andrew W. Appel:
Abstraction and subsumption in modular verification of C programs. Formal Methods Syst. Des. 58(1-2): 322-345 (2021) - [j41]John M. Li, Andrew W. Appel:
Deriving efficient program transformations from rewrite rules. Proc. ACM Program. Lang. 5(ICFP): 1-29 (2021) - [j40]Zoe Paraskevopoulou, John M. Li, Andrew W. Appel:
Compositional optimizations for CertiCoq. Proc. ACM Program. Lang. 5(ICFP): 1-30 (2021) - [i5]Andrew W. Appel, Xavier Leroy:
Efficient Extensional Binary Tries. CoRR abs/2110.05063 (2021) - 2020
- [j39]Andrew W. Appel, Yves Bertot:
C floating-point proofs layered with VST and Flocq. J. Formaliz. Reason. 13(1): 1-16 (2020) - [j38]Andrew W. Appel, Yves Bertot:
Corrigendum: C floating-point proofs layered with VST and Flocq. J. Formaliz. Reason. 13(1) (2020) - [c68]William Mansky, Wolf Honoré, Andrew W. Appel:
Connecting Higher-Order Separation Logic to a First-Order Outside World. ESOP 2020: 428-455 - [c67]Andrew W. Appel, David A. Naumann:
Verified sequential Malloc/Free. ISMM 2020: 48-59
2010 – 2019
- 2019
- [j37]Andrew W. Appel:
Technical Perspective: The scalability of CertiKOS. Commun. ACM 62(10): 88 (2019) - [j36]Zoe Paraskevopoulou, Andrew W. Appel:
Closure conversion is safe for space. Proc. ACM Program. Lang. 3(ICFP): 83:1-83:29 (2019) - [c66]Lennart Beringer, Andrew W. Appel:
Abstraction and Subsumption in Modular Verification of C Programs. FM 2019: 573-590 - [i4]Qinxiang Cao, Shengyi Wang, Aquinas Hobor, Andrew W. Appel:
Proof Pearl: Magic Wand as Frame. CoRR abs/1909.08789 (2019) - 2018
- [j35]Qinxiang Cao, Lennart Beringer, Samuel Gruetter, Josiah Dodds, Andrew W. Appel:
VST-Floyd: A Separation Logic Tool to Verify Correctness of C Programs. J. Autom. Reason. 61(1-4): 367-422 (2018) - 2017
- [j34]William Mansky, Andrew W. Appel, Aleksey Nogin:
A verified messaging system. Proc. ACM Program. Lang. 1(OOPSLA): 87:1-87:28 (2017) - [c65]Qinxiang Cao, Santiago Cuellar, Andrew W. Appel:
Bringing Order to the Separation Logic Jungle. APLAS 2017: 190-211 - [c64]Katherine Q. Ye, Matthew Green, Naphat Sanguansin, Lennart Beringer, Adam Petcher, Andrew W. Appel:
Verified Correctness and Security of mbedTLS HMAC-DRBG. CCS 2017: 2007-2020 - [c63]Olivier Savary Bélanger, Andrew W. Appel:
Shrink fast correctly! PPDP 2017: 49-60 - [i3]Katherine Q. Ye, Matthew Green, Naphat Sanguansin, Lennart Beringer, Adam Petcher, Andrew W. Appel:
Verified Correctness and Security of mbedTLS HMAC-DRBG. CoRR abs/1708.08542 (2017) - 2016
- [c62]Andrew W. Appel:
Modular Verification for Computer Security. CSF 2016: 1-8 - 2015
- [j33]Andrew W. Appel:
Verification of a Cryptographic Primitive: SHA-256. ACM Trans. Program. Lang. Syst. 37(2): 7:1-7:31 (2015) - [c61]Andrew W. Appel:
Verification of a cryptographic primitive: SHA-256 (abstract). PLDI 2015: 153 - [c60]Gordon Stewart, Lennart Beringer, Santiago Cuellar, Andrew W. Appel:
Compositional CompCert. POPL 2015: 275-287 - [c59]Lennart Beringer, Adam Petcher, Katherine Q. Ye, Andrew W. Appel:
Verified Correctness and Security of OpenSSL HMAC. USENIX Security Symposium 2015: 207-221 - 2014
- [b10]Andrew W. Appel:
Program Logics - for Certified Compilers. Cambridge University Press 2014, ISBN 978-1-10-704801-0, pp. I-X, 1-458 - [c58]Joshua A. Kroll, Gordon Stewart, Andrew W. Appel:
Portable Software Fault Isolation. CSF 2014: 18-32 - [c57]Lennart Beringer, Gordon Stewart, Robert Dockins, Andrew W. Appel:
Verified Compilation for Shared-Memory C. ESOP 2014: 107-127 - 2013
- [c56]Josiah Dodds, Andrew W. Appel:
Mostly Sound Type System Improves a Foundational Program Verifier. CPP 2013: 17-32 - 2012
- [j32]Andrew W. Appel, Robert Dockins, Xavier Leroy:
A List-Machine Benchmark for Mechanized Metatheory. J. Autom. Reason. 49(3): 453-491 (2012) - [c55]Gordon Stewart, Lennart Beringer, Andrew W. Appel:
Verified heap theorem prover by paramodulation. ICFP 2012: 3-14 - [c54]Andrew W. Appel:
Verified Software Toolchain. NASA Formal Methods 2012: 2 - [c53]Torben Amtoft, Josiah Dodds, Zhi Zhang, Andrew W. Appel, Lennart Beringer, John Hatcliff, Xinming Ou, Andrew Cousino:
A Certificate Infrastructure for Machine-Checked Proofs of Conditional Information Flow. POST 2012: 369-389 - 2011
- [j31]Andrew W. Appel:
Security Seals on Voting Machines: A Case Study. ACM Trans. Inf. Syst. Secur. 14(2): 18:1-18:29 (2011) - [c52]Andrew W. Appel:
VeriSmall: Verified Smallfoot Shape Analysis. CPP 2011: 231-246 - [c51]Andrew W. Appel:
Verified Software Toolchain - (Invited Talk). ESOP 2011: 1-17 - [c50]Gordon Stewart, Andrew W. Appel:
Local actions for a curry-style operational semantics. PLPV 2011: 31-42 - 2010
- [j30]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. 32(3): 7:1-7:67 (2010) - [c49]Aquinas Hobor, Robert Dockins, Andrew W. Appel:
A Logical Mix of Approximation and Separation. APLAS 2010: 439-454 - [c48]Sandrine Blazy, Benoît Robillard, Andrew W. Appel:
Formal Verification of Coalescing Graph-Coloring Register Allocation. ESOP 2010: 145-164 - [c47]Aquinas Hobor, Robert Dockins, Andrew W. Appel:
A theory of indirection via approximation. POPL 2010: 171-184 - [c46]Christian J. Bell, Andrew W. Appel, David Walker:
Concurrent Separation Logic for Pipelined Parallelization. SAS 2010: 151-166
2000 – 2009
- 2009
- [c45]Robert Dockins, Aquinas Hobor, Andrew W. Appel:
A Fresh Look at Separation Algebras and Share Accounting. APLAS 2009: 161-177 - [c44]Andrew W. Appel, Maia Ginsburg, Harri Hursti, Brian W. Kernighan, Christopher D. Richards, Gang Tan, Penny Venetis:
The New Jersey Voting-machine Lawsuit and the AVC Advantage DRE Voting Machine. EVT/WOTE 2009 - 2008
- [c43]Aquinas Hobor, Andrew W. Appel, Francesco Zappa Nardelli:
Oracle Semantics for Concurrent Separation Logic. ESOP 2008: 353-367 - [c42]Robert Dockins, Andrew W. Appel, Aquinas Hobor:
Multimodal Separation Logic for Reasoning About Operational Semantics. MFPS 2008: 5-20 - 2007
- [c41]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 - [c40]Andrew W. Appel, Sandrine Blazy:
Separation Logic for Small-Step cminor. TPHOLs 2007: 5-21 - [i2]Andrew W. Appel, Sandrine Blazy:
Separation Logic for Small-step Cminor. CoRR abs/0707.4389 (2007) - 2006
- [b9]Andrew W. Appel:
Compiling with Continuations (corr. version). Cambridge University Press 2006, ISBN 978-0-521-03311-4, pp. I-X, 1-260 - [c39]Gang Tan, Andrew W. Appel:
A Compositional Logic for Control Flow. VMCAI 2006: 80-94 - [c38]Andrew W. Appel, Xavier Leroy:
A List-machine Benchmark for Mechanized Metatheory: (Extended Abstract). LFMTP@FLoC 2006: 95-108 - 2005
- [c37]Xinming Ou, Sudhakar Govindavajhala, Andrew W. Appel:
MulVAL: A Logic-based Network Security Analyzer. USENIX Security Symposium 2005 - 2004
- [j29]Andrew W. Appel, Amy P. Felty:
Dependent types ensure partial correctness of theorem provers. J. Funct. Program. 14(1): 3-19 (2004) - [j28]Andrew W. Appel, Amy P. Felty:
Polymorphic Lemmas and Definitions in lambda-Prolog and Twelf. Theory Pract. Log. Program. 4(1-2): 1-39 (2004) - [c36]Andrew W. Appel:
Social processes and proofs of theorems and programs, revisited. PLDI 2004: 170 - [c35]Gang Tan, Andrew W. Appel, Kedar N. Swadi, Dinghao Wu:
Construction of a Semantic Model for a Typed Assembly Language. VMCAI 2004: 30-43 - [i1]Andrew W. Appel, Amy P. Felty:
Polymorphic lemmas and definitions in Lambda Prolog and Twelf. CoRR cs.LO/0403010 (2004) - 2003
- [j27]Andrew W. Appel, Neophytos G. Michael, Aaron Stump, Roberto Virga:
A Trustworthy Proof Checker. J. Autom. Reason. 31(3-4): 231-260 (2003) - [j26]Lujo Bauer, Andrew W. Appel, Edward W. Felten:
Mechanisms for secure modular programming in Java. Softw. Pract. Exp. 33(5): 461-480 (2003) - [c34]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 - [c33]Juan Chen, Dinghao Wu, Andrew W. Appel, Hai Fang:
A provably sound TAL for back-end optimization. PLDI 2003: 208-219 - [c32]Dinghao Wu, Andrew W. Appel, Aaron Stump:
Foundational proof checkers with small witnesses. PPDP 2003: 264-274 - [c31]Eunyoung Lee, Andrew W. Appel:
Policy-enforced linking of untrusted components. ESEC / SIGSOFT FSE 2003: 371-374 - [c30]Sudhakar Govindavajhala, Andrew W. Appel:
Using Memory Errors to Attack a Virtual Machine. S&P 2003: 154-165 - 2002
- [b8]Andrew W. Appel, Jens Palsberg:
Modern Compiler Implementation in Java, 2nd edition. Cambridge University Press 2002, ISBN 0-521-82060-X - [c29]Amal J. Ahmed, Andrew W. Appel, Roberto Virga:
A Stratified Semantics of General References A Stratified Semantics of General References. LICS 2002: 75- - [c28]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
- [j25]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) - [c27]Andrew W. Appel:
Foundational Proof-Carrying Code. LICS 2001: 247-256 - [c26]Andrew W. Appel, Lal George:
Optimal Spilling for CISC Machines with Few Registers. PLDI 2001: 243-253 - [c25]Daniel C. Wang, Andrew W. Appel:
Type-preserving garbage collectors. POPL 2001: 166-178 - 2000
- [j24]Andrew W. Appel, Edward W. Felten:
Technological access control interferes with noninfringing scholarship. Commun. ACM 43(9): 21-23 (2000) - [j23]Zhong Shao, Andrew W. Appel:
Efficient and safe-for-space closure conversion. ACM Trans. Program. Lang. Syst. 22(1): 129-161 (2000) - [j22]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) - [c24]Neophytos G. Michael, Andrew W. Appel:
Machine Instruction Syntax and Semantics in Higher Order Logic. CADE 2000: 7-24 - [c23]Andrew W. Appel, Amy P. Felty:
A Semantic Model of Types and Machine Instuctions for Proof-Carrying Code. POPL 2000: 243-253
1990 – 1999
- 1999
- [j21]Matthias Blume, Andrew W. Appel:
Hierarchical modularity. ACM Trans. Program. Lang. Syst. 21(4): 813-847 (1999) - [c22]Andrew W. Appel, Edward W. Felten:
Proof-Carrying Authentication. CCS 1999: 52-62 - [c21]Andrew W. Appel, Amy P. Felty:
Lightweight Lemmas in lambda-Prolog. ICLP 1999: 411-425 - [e1]Andrew W. Appel, Alex Aiken:
POPL '99, Proceedings of the 26th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, San Antonio, TX, USA, January 20-22, 1999. ACM 1999, ISBN 1-58113-095-3 [contents] - 1998
- [b7]Andrew W. Appel:
Modern Compiler Implementation in Java. Cambridge University Press 1998, ISBN 0-521-58388-8 - [b6]Andrew W. Appel:
Modern Compiler Implementation in C. Cambridge University Press 1998, ISBN 0-521-58390-X - [b5]Andrew W. Appel:
Modern Compiler Implementation in ML. Cambridge University Press 1998, ISBN 0-521-58274-1 - [j20]Andrew W. Appel:
SSA is Functional Programming. ACM SIGPLAN Notices 33(4): 17-20 (1998) - [c20]Jeffrey L. Korn, Andrew W. Appel:
Traversal-Based Visualization of Data Structures. INFOVIS 1998: 11-18 - 1997
- [b4]Andrew W. Appel:
Modern Compiler Implementation in Java: Basic Techniques. Cambridge University Press 1997, ISBN 0-521-58654-2 - [b3]Andrew W. Appel:
Modern Compiler Implementation in C: Basic Techniques. Cambridge University Press 1997, ISBN 0-521-58653-4 - [b2]Andrew W. Appel:
Modern Compiler Implementation in ML: Basic Techniques. Cambridge University Press 1997, ISBN 0-521-58775-1 - [j19]Andrew W. Appel, Trevor Jim:
Shrinking lambda Expressions in Linear Time. J. Funct. Program. 7(5): 515-540 (1997) - [c19]Daniel C. Wang, Andrew W. Appel, Jeffrey L. Korn, Christopher S. Serra:
The Zephyr Abstract Syntax Description Language. DSL 1997: 213-228 - [c18]Matthias Blume, Andrew W. Appel:
Lambda-Splitting: A Higher-Order Approach to Cross-Module Optimizations. ICFP 1997: 112-124 - 1996
- [j18]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) - [j17]Andrew W. Appel:
Intensional Equality ;=) for Continuations. ACM SIGPLAN Notices 31(2): 55-57 (1996) - [j16]Lal George, Andrew W. Appel:
Iterated Register Coalescing. ACM Trans. Program. Lang. Syst. 18(3): 300-324 (1996) - [c17]Lal George, Andrew W. Appel:
Iterated Register Coalescing. POPL 1996: 208-218 - 1995
- [j15]Andrew P. Tolmach, Andrew W. Appel:
A Debugger for Standard ML. J. Funct. Program. 5(2): 155-200 (1995) - [c16]Marcelo J. R. Gonçalves, Andrew W. Appel:
Cache Performance of Fast-Allocating Programs. FPCA 1995: 293-305 - [c15]Zhong Shao, Andrew W. Appel:
A Type-Based Compiler for Standard ML. PLDI 1995: 116-129 - 1994
- [j14]Andrew W. Appel:
Loop Headers in Lambda-Calculus or CPS. LISP Symb. Comput. 7(4): 337-343 (1994) - [j13]Andrew W. Appel:
Axiomatic Bootstrapping: A Guide for Compiler Hackers. ACM Trans. Program. Lang. Syst. 16(6): 1699-1718 (1994) - [c14]Zhong Shao, Andrew W. Appel:
Space-Efficient Closure Representations. LISP and Functional Programming 1994: 150-161 - [c13]Zhong Shao, John H. Reppy, Andrew W. Appel:
Unrolling Lists. LISP and Functional Programming 1994: 185-195 - [c12]Andrew W. Appel, David B. MacQueen:
Separate Compilation for Standard ML. PLDI 1994: 13-23 - 1993
- [j12]Andrew W. Appel:
A Critique of Standard ML. J. Funct. Program. 3(4): 391-429 (1993) - [c11]Zhong Shao, Andrew W. Appel:
Smartest Recompilation. POPL 1993: 439-450 - 1992
- [b1]Andrew W. Appel:
Compiling with Continuations. Cambridge University Press 1992, ISBN 0-521-41695-7 - [j11]Andrew W. Appel, Zhong Shao:
Callee-Save Registers in Continuation-Passing Style. LISP Symb. Comput. 5(3): 191-221 (1992) - [j10]Andrew W. Appel:
Is POPL mathematics or science? ACM SIGPLAN Notices 27(4): 87-89 (1992) - 1991
- [c10]Andrew W. Appel, Kai Li:
Virtual Memory Primitives for User Programs. ASPLOS 1991: 96-107 - [c9]Andrew P. Tolmach, Andrew W. Appel:
Debuggable Concurrency Extensions for Standard ML. Workshop on Parallel and Distributed Debugging 1991: 120-131 - [c8]Andrew W. Appel, David B. MacQueen:
Standard ML of New Jersey. PLILP 1991: 1-13 - 1990
- [j9]Andrew W. Appel:
A Runtime System. LISP Symb. Comput. 3(4): 343-380 (1990) - [c7]Andrew P. Tolmach, Andrew W. Appel:
Debugging Standard ML Without Reverse Engineering. LISP and Functional Programming 1990: 1-12 - [c6]Rafael Alonso, Andrew W. Appel:
An Advisor for Flexible Working Sets. SIGMETRICS 1990: 153-162
1980 – 1989
- 1989
- [j8]Andrew W. Appel:
Runtime Tags Aren't Necessary. LISP Symb. Comput. 2(2): 153-162 (1989) - [j7]Andrew W. Appel:
Simple Generational Garbage Collection and Fast Allocation. Softw. Pract. Exp. 19(2): 171-183 (1989) - [j6]Andrew W. Appel:
Allocation without Locking.