Andrew W. Appel

According to our database, Andrew W. Appel authored at least 131 papers between 1985 and 2024.

Collaborative distances:

• Dijkstra number of four.
• Erdős number of four.

2024

VST-A: A Foundationally Sound Annotation Verifier.

Litao Zhou, Jianxing Qin, Qinshi Wang, Andrew W. Appel, Qinxiang Cao

Proc. ACM Program. Lang., January, 2024

VCFloat2: Floating-Point Error Analysis in Coq.

Andrew W. Appel, Ariel Kellison

Proceedings of the 13th ACM SIGPLAN International Conference on Certified Programs and Proofs, 2024

2023

Efficient Extensional Binary Tries.

Andrew W. Appel, Xavier Leroy

J. Autom. Reason., March, 2023

A Solver for Arrays with Concatenation.

Qinshi Wang, Andrew W. Appel

J. Autom. Reason., 2023

Specifying and Verifying a Real-World Packet Error-Correction System.

Joshua M. Cohen, Andrew W. Appel

Proceedings of the Verified Software. Theories, Tools and Experiments, 2023

Verified Correctness, Accuracy, and Convergence of a Stationary Iterative Linear Solver: Jacobi Method.

Mohit Tekriwal, Andrew W. Appel, Ariel E. Kellison, David Bindel, Jean-Baptiste Jeannin

Proceedings of the Intelligent Computer Mathematics - 16th International Conference, 2023

Foundational Verification of Stateful P4 Packet Processing.

Qinshi Wang, Mengying Pan, Shengyi Wang, Ryan Doenges, Lennart Beringer, Andrew W. Appel

Proceedings of the 14th International Conference on Interactive Theorem Proving, 2023

LAProof: A Library of Formal Proofs of Accuracy and Correctness for Linear Algebra Programs.

Ariel E. Kellison, Andrew W. Appel, Mohit Tekriwal, David Bindel

Proceedings of the 30th IEEE Symposium on Computer Arithmetic, 2023

2022

Coq's vibrant ecosystem for verification engineering (invited talk).

Andrew W. Appel

Proceedings of the CPP '22: 11th ACM SIGPLAN International Conference on Certified Programs and Proofs, Philadelphia, PA, USA, January 17, 2022

Verified Numerical Methods for Ordinary Differential Equations.

Ariel E. Kellison, Andrew W. Appel

Proceedings of the Software Verification and Formal Methods for ML-Enabled Autonomous Systems, 2022

Verified Erasure Correction in Coq with MathComp and VST.

Joshua M. Cohen, Qinshi Wang, Andrew W. Appel

Proceedings of the Computer Aided Verification - 34th International Conference, 2022

2021

Compositional optimizations for CertiCoq.

Zoe Paraskevopoulou, John M. Li, Andrew W. Appel

Proc. ACM Program. Lang., 2021

Deriving efficient program transformations from rewrite rules.

John M. Li, Andrew W. Appel

Proc. ACM Program. Lang., 2021

Abstraction and subsumption in modular verification of C programs.

Lennart Beringer, Andrew W. Appel

Formal Methods Syst. Des., 2021

2020

Corrigendum: C floating-point proofs layered with VST and Flocq.

Andrew W. Appel, Yves Bertot

J. Formaliz. Reason., 2020

C floating-point proofs layered with VST and Flocq.

Andrew W. Appel, Yves Bertot

J. Formaliz. Reason., 2020

Verified sequential Malloc/Free.

Andrew W. Appel, David A. Naumann

Proceedings of the ISMM '20: 2020 ACM SIGPLAN International Symposium on Memory Management, 2020

Connecting Higher-Order Separation Logic to a First-Order Outside World.

William Mansky, Wolf Honoré, Andrew W. Appel

Proceedings of the Programming Languages and Systems, 2020

2019

Closure conversion is safe for space.

Zoe Paraskevopoulou, Andrew W. Appel

Proc. ACM Program. Lang., 2019

Proof Pearl: Magic Wand as Frame.

Qinxiang Cao, Shengyi Wang, Aquinas Hobor, Andrew W. Appel

CoRR, 2019

Technical Perspective: The scalability of CertiKOS.

Andrew W. Appel

Commun. ACM, 2019

2018

VST-Floyd: A Separation Logic Tool to Verify Correctness of C Programs.

Qinxiang Cao, Lennart Beringer, Samuel Gruetter, Josiah Dodds, Andrew W. Appel

J. Autom. Reason., 2018

2017

A verified messaging system.

William Mansky, Andrew W. Appel, Aleksey Nogin

Proc. ACM Program. Lang., 2017

Shrink fast correctly!

Olivier Savary Bélanger, Andrew W. Appel

Proceedings of the 19th International Symposium on Principles and Practice of Declarative Programming, Namur, Belgium, October 09, 2017

Verified Correctness and Security of mbedTLS HMAC-DRBG.

Katherine Q. Ye, Matthew Green, Naphat Sanguansin, Lennart Beringer, Adam Petcher, Andrew W. Appel

Proceedings of the 2017 ACM SIGSAC Conference on Computer and Communications Security, 2017

Bringing Order to the Separation Logic Jungle.

Qinxiang Cao, Santiago Cuéllar, Andrew W. Appel

Proceedings of the Programming Languages and Systems - 15th Asian Symposium, 2017

2016

Modular Verification for Computer Security.

Andrew W. Appel

Proceedings of the IEEE 29th Computer Security Foundations Symposium, 2016

2015

Verification of a Cryptographic Primitive: SHA-256.

Andrew W. Appel

ACM Trans. Program. Lang. Syst., 2015

Verified Correctness and Security of OpenSSL HMAC.

Lennart Beringer, Adam Petcher, Katherine Q. Ye, Andrew W. Appel

Proceedings of the 24th USENIX Security Symposium, 2015

Compositional CompCert.

Gordon Stewart, Lennart Beringer, Santiago Cuéllar, Andrew W. Appel

Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2015

Verification of a cryptographic primitive: SHA-256 (abstract).

Andrew W. Appel

Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation, 2015

2014

Verified Compilation for Shared-Memory C.

Lennart Beringer, Gordon Stewart, Robert Dockins, Andrew W. Appel

Proceedings of the Programming Languages and Systems, 2014

Portable Software Fault Isolation.

Joshua A. Kroll, Gordon Stewart, Andrew W. Appel

Proceedings of the IEEE 27th Computer Security Foundations Symposium, 2014

Program Logics - for Certified Compilers.

Andrew W. Appel

Cambridge University Press, ISBN: 978-1-10-704801-0, 2014

2013

Mostly Sound Type System Improves a Foundational Program Verifier.

Josiah Dodds, Andrew W. Appel

Proceedings of the Certified Programs and Proofs - Third International Conference, 2013

2012

A List-Machine Benchmark for Mechanized Metatheory.

Andrew W. Appel, Robert Dockins, Xavier Leroy

J. Autom. Reason., 2012

A Certificate Infrastructure for Machine-Checked Proofs of Conditional Information Flow.

Torben Amtoft, Josiah Dodds, Zhi Zhang, Andrew W. Appel, Lennart Beringer, John Hatcliff, Xinming Ou, Andrew Cousino

Proceedings of the Principles of Security and Trust - First International Conference, 2012

Verified Software Toolchain.

Andrew W. Appel

Proceedings of the NASA Formal Methods, 2012

Verified heap theorem prover by paramodulation.

Gordon Stewart, Lennart Beringer, Andrew W. Appel

Proceedings of the ACM SIGPLAN International Conference on Functional Programming, 2012

2011

Security Seals on Voting Machines: A Case Study.

Andrew W. Appel

ACM Trans. Inf. Syst. Secur., 2011

Local actions for a curry-style operational semantics.

Gordon Stewart, Andrew W. Appel

Proceedings of the 5th ACM Workshop Programming Languages meets Program Verification, 2011

Verified Software Toolchain - (Invited Talk).

Andrew W. Appel

Proceedings of the Programming Languages and Systems, 2011

VeriSmall: Verified Smallfoot Shape Analysis.

Andrew W. Appel

Proceedings of the Certified Programs and Proofs - First International Conference, 2011

2010

Semantic foundations for typed assembly languages.

Amal Ahmed, Andrew W. Appel, Christopher D. Richards, Kedar N. Swadi, Gang Tan, Daniel C. Wang

ACM Trans. Program. Lang. Syst., 2010

Concurrent Separation Logic for Pipelined Parallelization.

Christian J. Bell, Andrew W. Appel, David Walker

Proceedings of the Static Analysis - 17th International Symposium, 2010

A theory of indirection via approximation.

Aquinas Hobor, Robert Dockins, Andrew W. Appel

Proceedings of the 37th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2010

Formal Verification of Coalescing Graph-Coloring Register Allocation.

Sandrine Blazy, Benoît Robillard, Andrew W. Appel

Proceedings of the Programming Languages and Systems, 2010

A Logical Mix of Approximation and Separation.

Aquinas Hobor, Robert Dockins, Andrew W. Appel

Proceedings of the Programming Languages and Systems - 8th Asian Symposium, 2010

2009

The New Jersey Voting-machine Lawsuit and the AVC Advantage DRE Voting Machine.

Andrew W. Appel, Maia Ginsburg, Harri Hursti, Brian W. Kernighan, Christopher D. Richards, Gang Tan, Penny Venetis

Proceedings of the 2009 Electronic Voting Technology Workshop / Workshop on Trustworthy Elections, 2009

A Fresh Look at Separation Algebras and Share Accounting.

Robert Dockins, Aquinas Hobor, Andrew W. Appel

Proceedings of the Programming Languages and Systems, 7th Asian Symposium, 2009

2008

Multimodal Separation Logic for Reasoning About Operational Semantics.

Robert Dockins, Andrew W. Appel, Aquinas Hobor

Proceedings of the 24th Conference on the Mathematical Foundations of Programming Semantics, 2008

Oracle Semantics for Concurrent Separation Logic.

Aquinas Hobor, Andrew W. Appel, Francesco Zappa Nardelli

Proceedings of the Programming Languages and Systems, 2008

2007

Separation Logic for Small-Step cminor.

Andrew W. Appel, Sandrine Blazy

Proceedings of the Theorem Proving in Higher Order Logics, 20th International Conference, 2007

A very modal model of a modern, major, general type system.

Andrew W. Appel, Paul-André Melliès, Christopher D. Richards, Jérôme Vouillon

Proceedings of the 34th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2007

2006

A List-machine Benchmark for Mechanized Metatheory: (Extended Abstract).

Andrew W. Appel, Xavier Leroy

Proceedings of the First International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice, 2006

A Compositional Logic for Control Flow.

Gang Tan, Andrew W. Appel

Proceedings of the Verification, 2006

Safe Java Native Interface.

Gang Tan, Andrew W. Appel, Srimat Chakradhar, Anand Raghunathan, Srivaths Ravi, Daniel C. Wang

Proceedings of the 2006 IEEE International Symposium on Secure Software Engineering, 2006

Compiling with Continuations (corr. version).

Andrew W. Appel

Cambridge University Press, ISBN: 978-0-521-03311-4, 2006

2005

MulVAL: A Logic-based Network Security Analyzer.

Xinming Ou, Sudhakar Govindavajhala, Andrew W. Appel

Proceedings of the 14th USENIX Security Symposium, Baltimore, MD, USA, July 31, 2005

2004

Polymorphic Lemmas and Definitions in lambda-Prolog and Twelf.

Andrew W. Appel, Amy P. Felty

Theory Pract. Log. Program., 2004

Dependent types ensure partial correctness of theorem provers.

Andrew W. Appel, Amy P. Felty

J. Funct. Program., 2004

Construction of a Semantic Model for a Typed Assembly Language.

Gang Tan, Andrew W. Appel, Kedar N. Swadi, Dinghao Wu

Proceedings of the Verification, 2004

Social processes and proofs of theorems and programs, revisited.

Andrew W. Appel

Proceedings of the ACM SIGPLAN 2004 Conference on Programming Language Design and Implementation 2004, 2004

2003

Mechanisms for secure modular programming in Java.

Lujo Bauer, Andrew W. Appel, Edward W. Felten

Softw. Pract. Exp., 2003

A Trustworthy Proof Checker.

Andrew W. Appel, Neophytos G. Michael, Aaron Stump, Roberto Virga

J. Autom. Reason., 2003

Using Memory Errors to Attack a Virtual Machine.

Sudhakar Govindavajhala, Andrew W. Appel

Proceedings of the 2003 IEEE Symposium on Security and Privacy (S&P 2003), 2003

Policy-enforced linking of untrusted components.

Eunyoung Lee, Andrew W. Appel

Proceedings of the 11th ACM SIGSOFT Symposium on Foundations of Software Engineering 2003 held jointly with 9th European Software Engineering Conference, 2003

Foundational proof checkers with small witnesses.

Dinghao Wu, Andrew W. Appel, Aaron Stump

Proceedings of the 5th International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming, 2003

A provably sound TAL for back-end optimization.

Juan Chen, Dinghao Wu, Andrew W. Appel, Hai Fang

Proceedings of the ACM SIGPLAN 2003 Conference on Programming Language Design and Implementation 2003, 2003

Access Control on the Web Using Proof-carrying Authorization.

Lujo Bauer, Michael A. Schneider, Edward W. Felten, Andrew W. Appel

Proceedings of the 3rd DARPA Information Survivability Conference and Exposition (DISCEX-III 2003), 2003

2002

Creating and preserving locality of java applications at allocation and garbage collection times.

Yefim Shuf, Manish Gupta, Hubertus Franke, Andrew W. Appel, Jaswinder Pal Singh

Proceedings of the 2002 ACM SIGPLAN Conference on Object-Oriented Programming Systems, 2002

A Stratified Semantics of General References A Stratified Semantics of General References.

Amal J. Ahmed, Andrew W. Appel, Roberto Virga

Proceedings of the 17th IEEE Symposium on Logic in Computer Science (LICS 2002), 2002

Modern Compiler Implementation in Java, 2nd edition.

Andrew W. Appel, Jens Palsberg

Cambridge University Press, ISBN: 0-521-82060-X, 2002

2001

An indexed model of recursive types for foundational proof-carrying code.

Andrew W. Appel, David A. McAllester

ACM Trans. Program. Lang. Syst., 2001

Type-preserving garbage collectors.

Daniel C. Wang, Andrew W. Appel

Proceedings of the Conference Record of POPL 2001: The 28th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2001

Optimal Spilling for CISC Machines with Few Registers.

Andrew W. Appel, Lal George

Proceedings of the 2001 ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), 2001

Foundational Proof-Carrying Code.

Andrew W. Appel

Proceedings of the 16th Annual IEEE Symposium on Logic in Computer Science, 2001

2000

SAFKASI: a security mechanism for language-based systems.

Dan S. Wallach, Andrew W. Appel, Edward W. Felten

ACM Trans. Softw. Eng. Methodol., 2000

Efficient and safe-for-space closure conversion.

Zhong Shao, Andrew W. Appel

ACM Trans. Program. Lang. Syst., 2000

Technological access control interferes with noninfringing scholarship.

Andrew W. Appel, Edward W. Felten

Commun. ACM, 2000

A Semantic Model of Types and Machine Instructions for Proof-Carrying Code.

Andrew W. Appel, Amy P. Felty

Proceedings of the POPL 2000, 2000

Machine Instruction Syntax and Semantics in Higher Order Logic.

Neophytos G. Michael, Andrew W. Appel

Proceedings of the Automated Deduction, 2000

1999

Hierarchical modularity.

Matthias Blume, Andrew W. Appel

ACM Trans. Program. Lang. Syst., 1999

Lightweight Lemmas in lambda-Prolog.

Andrew W. Appel, Amy P. Felty

Proceedings of the Logic Programming: The 1999 International Conference, Las Cruces, New Mexico, USA, November 29, 1999

Proof-Carrying Authentication.

Andrew W. Appel, Edward W. Felten

Proceedings of the CCS '99, 1999

1998

SSA is Functional Programming.

Andrew W. Appel

ACM SIGPLAN Notices, 1998

Traversal-Based Visualization of Data Structures.

Jeffrey L. Korn, Andrew W. Appel

Proceedings of the 1998 IEEE Symposium on Information Visualization (InfoVis '98), 1998

Modern Compiler Implementation in ML

Andrew W. Appel

Cambridge University Press, ISBN: 0-521-58274-1, 1998

Modern Compiler Implementation in C

Andrew W. Appel

Cambridge University Press, ISBN: 0-521-58390-X, 1998

Modern Compiler Implementation in Java

Andrew W. Appel

Cambridge University Press, ISBN: 0-521-58388-8, 1998

1997

Shrinking lambda Expressions in Linear Time.

Andrew W. Appel, Trevor Jim

J. Funct. Program., 1997

Lambda-Splitting: A Higher-Order Approach to Cross-Module Optimizations.

Matthias Blume, Andrew W. Appel

Proceedings of the 1997 ACM SIGPLAN International Conference on Functional Programming (ICFP '97), 1997

The Zephyr Abstract Syntax Description Language.

Daniel C. Wang, Andrew W. Appel, Jeffrey L. Korn, Christopher S. Serra

Proceedings of the Conference on Domain-Specific Languages, 1997

Modern Compiler Implementation in ML: Basic Techniques

Andrew W. Appel

Cambridge University Press, ISBN: 0-521-58775-1, 1997

Modern Compiler Implementation in C: Basic Techniques

Andrew W. Appel

Cambridge University Press, ISBN: 0-521-58653-4, 1997

Modern Compiler Implementation in Java: Basic Techniques

Andrew W. Appel

Cambridge University Press, ISBN: 0-521-58654-2, 1997

1996

Iterated Register Coalescing.

Lal George, Andrew W. Appel

ACM Trans. Program. Lang. Syst., 1996

Intensional Equality ;=) for Continuations.

Andrew W. Appel

ACM SIGPLAN Notices, 1996

Empirical and Analytic Study of Stack Versus Heap Cost for Languages with Closures.

Andrew W. Appel, Zhong Shao

J. Funct. Program., 1996

1995

A Debugger for Standard ML.

Andrew P. Tolmach, Andrew W. Appel

J. Funct. Program., 1995

A Type-Based Compiler for Standard ML.

Zhong Shao, Andrew W. Appel

Proceedings of the ACM SIGPLAN'95 Conference on Programming Language Design and Implementation (PLDI), 1995

Cache Performance of Fast-Allocating Programs.

Marcelo J. R. Gonçalves, Andrew W. Appel

Proceedings of the seventh international conference on Functional programming languages and computer architecture, 1995

1994

Axiomatic Bootstrapping: A Guide for Compiler Hackers.

Andrew W. Appel

ACM Trans. Program. Lang. Syst., 1994

Loop Headers in Lambda-Calculus or CPS.

Andrew W. Appel

LISP Symb. Comput., 1994

Separate Compilation for Standard ML.

Andrew W. Appel, David B. MacQueen

Proceedings of the ACM SIGPLAN'94 Conference on Programming Language Design and Implementation (PLDI), 1994

Unrolling Lists.

Zhong Shao, John H. Reppy, Andrew W. Appel

Proceedings of the 1994 ACM Conference on LISP and Functional Programming, 1994

Space-Efficient Closure Representations.

Zhong Shao, Andrew W. Appel

Proceedings of the 1994 ACM Conference on LISP and Functional Programming, 1994

1993

A Critique of Standard ML.

Andrew W. Appel

J. Funct. Program., 1993

Smartest Recompilation.

Zhong Shao, Andrew W. Appel

Proceedings of the Conference Record of the Twentieth Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 1993

1992

Is POPL mathematics or science?

Andrew W. Appel

ACM SIGPLAN Notices, 1992

Callee-Save Registers in Continuation-Passing Style.

Andrew W. Appel, Zhong Shao

LISP Symb. Comput., 1992

Compiling with Continuations

Andrew W. Appel

Cambridge University Press, ISBN: 0-521-41695-7, 1992

1991

Standard ML of New Jersey.

Andrew W. Appel, David B. MacQueen

Proceedings of the Programming Language Implementation and Logic Programming, 1991

Debuggable Concurrency Extensions for Standard ML.

Andrew P. Tolmach, Andrew W. Appel

Proceedings of the ACM/ONR Workshop on Parallel and Distributed Debugging, 1991

Virtual Memory Primitives for User Programs.

Andrew W. Appel, Kai Li

Proceedings of the ASPLOS-IV Proceedings, 1991

1990

A Runtime System.

Andrew W. Appel

LISP Symb. Comput., 1990

An Advisor for Flexible Working Sets.

Rafael Alonso, Andrew W. Appel

Proceedings of the 1990 ACM SIGMETRICS conference on Measurement and modeling of computer systems, 1990

Debugging Standard ML Without Reverse Engineering.

Andrew P. Tolmach, Andrew W. Appel

Proceedings of the 1990 ACM Conference on LISP and Functional Programming, 1990

1989

Vectorized garbage collection.

Andrew W. Appel, Aage Bendiksen

J. Supercomput., 1989

Allocation without Locking.

Andrew W. Appel

Softw. Pract. Exp., 1989

Simple Generational Garbage Collection and Fast Allocation.

Andrew W. Appel

Softw. Pract. Exp., 1989

Runtime Tags Aren't Necessary.

Andrew W. Appel

LISP Symb. Comput., 1989

Continuation-Passing, Closure-Passing Style.

Andrew W. Appel, Trevor Jim

Proceedings of the Conference Record of the Sixteenth Annual ACM Symposium on Principles of Programming Languages, 1989

1988

Simulating digital circuits with one bit per wire.

Andrew W. Appel

IEEE Trans. Comput. Aided Des. Integr. Circuits Syst., 1988

The World's Fastest Scrabble Program.

Andrew W. Appel, Guy J. Jacobson

Commun. ACM, 1988

Real-Time Concurrent Collection on Stock Multiprocessors.

Andrew W. Appel, John R. Ellis, Kai Li

Proceedings of the ACM SIGPLAN'88 Conference on Programming Language Design and Implementation (PLDI), 1988

Real-time concurrent collection on stock multiprocessors (with retrospective)

Andrew W. Appel

Proceedings of the 20 Years of the ACM SIGPLAN Conference on Programming Language Design and Implementation 1979-1999, 1988

1987

Generalization of the Sethi-Ullman Algorithm for Register Allocation.

Andrew W. Appel, Kenneth J. Supowit

Softw. Pract. Exp., 1987

Garbage Collection can be Faster than Stack Allocation.

Andrew W. Appel

Inf. Process. Lett., 1987

A Standard ML compiler.

Andrew W. Appel, David B. MacQueen

Proceedings of the Functional Programming Languages and Computer Architecture, 1987

1985

Semantics-Directed Code Generation.

Andrew W. Appel

Proceedings of the Conference Record of the Twelfth Annual ACM Symposium on Principles of Programming Languages, 1985