Andrew W. Appel

According to our database1, Andrew W. Appel authored at least 115 papers between 1985 and 2020.

Collaborative distances:
  • Dijkstra number2 of four.
  • Erdős number3 of four.

Awards

ACM Fellow

ACM Fellow 1998, "Significant research contributions in the area of programming languages and compilers. Important contributions to the ACM Transactions on Programming Languages and Systems.".

Timeline

Legend:

Book 
In proceedings 
Article 
PhD thesis 
Other 

Links

Online presence:

On csauthors.net:

Bibliography

2020
Verified sequential Malloc/Free.
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.
Proceedings of the Programming Languages and Systems, 2020

2019
Closure conversion is safe for space.
Proc. ACM Program. Lang., 2019

Proof Pearl: Magic Wand as Frame.
CoRR, 2019

Technical Perspective: The scalability of CertiKOS.
Commun. ACM, 2019

Abstraction and Subsumption in Modular Verification of C Programs.
Proceedings of the Formal Methods - The Next 30 Years - Third World Congress, 2019

2018
VST-Floyd: A Separation Logic Tool to Verify Correctness of C Programs.
J. Autom. Reason., 2018

2017
A verified messaging system.
Proc. ACM Program. Lang., 2017

Shrink fast correctly!
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.
Proceedings of the 2017 ACM SIGSAC Conference on Computer and Communications Security, 2017

Bringing Order to the Separation Logic Jungle.
Proceedings of the Programming Languages and Systems - 15th Asian Symposium, 2017

2016
Modular Verification for Computer Security.
Proceedings of the IEEE 29th Computer Security Foundations Symposium, 2016

2015
Verification of a Cryptographic Primitive: SHA-256.
ACM Trans. Program. Lang. Syst., 2015

Verified Correctness and Security of OpenSSL HMAC.
Proceedings of the 24th USENIX Security Symposium, 2015

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

Verification of a cryptographic primitive: SHA-256 (abstract).
Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation, 2015

2014
Verified Compilation for Shared-Memory C.
Proceedings of the Programming Languages and Systems, 2014

Portable Software Fault Isolation.
Proceedings of the IEEE 27th Computer Security Foundations Symposium, 2014

Program Logics - for Certified Compilers.
Cambridge University Press, ISBN: 978-1-10-704801-0, 2014

2013
Mostly Sound Type System Improves a Foundational Program Verifier.
Proceedings of the Certified Programs and Proofs - Third International Conference, 2013

2012
A List-Machine Benchmark for Mechanized Metatheory.
J. Autom. Reason., 2012

A Certificate Infrastructure for Machine-Checked Proofs of Conditional Information Flow.
Proceedings of the Principles of Security and Trust - First International Conference, 2012

Verified Software Toolchain.
Proceedings of the NASA Formal Methods, 2012

Verified heap theorem prover by paramodulation.
Proceedings of the ACM SIGPLAN International Conference on Functional Programming, 2012

2011
Security Seals on Voting Machines: A Case Study.
ACM Trans. Inf. Syst. Secur., 2011

Local actions for a curry-style operational semantics.
Proceedings of the 5th ACM Workshop Programming Languages meets Program Verification, 2011

Verified Software Toolchain - (Invited Talk).
Proceedings of the Programming Languages and Systems, 2011

VeriSmall: Verified Smallfoot Shape Analysis.
Proceedings of the Certified Programs and Proofs - First International Conference, 2011

2010
Semantic foundations for typed assembly languages.
ACM Trans. Program. Lang. Syst., 2010

Concurrent Separation Logic for Pipelined Parallelization.
Proceedings of the Static Analysis - 17th International Symposium, 2010

A theory of indirection via approximation.
Proceedings of the 37th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2010

Formal Verification of Coalescing Graph-Coloring Register Allocation.
Proceedings of the Programming Languages and Systems, 2010

A Logical Mix of Approximation and Separation.
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.
Proceedings of the 2009 Electronic Voting Technology Workshop / Workshop on Trustworthy Elections, 2009

A Fresh Look at Separation Algebras and Share Accounting.
Proceedings of the Programming Languages and Systems, 7th Asian Symposium, 2009

2008
Multimodal Separation Logic for Reasoning About Operational Semantics.
Proceedings of the 24th Conference on the Mathematical Foundations of Programming Semantics, 2008

Oracle Semantics for Concurrent Separation Logic.
Proceedings of the Programming Languages and Systems, 2008

2007
A List-machine Benchmark for Mechanized Metatheory: (Extended Abstract).
Electron. Notes Theor. Comput. Sci., 2007

Separation Logic for Small-Step cminor.
Proceedings of the Theorem Proving in Higher Order Logics, 20th International Conference, 2007

A very modal model of a modern, major, general type system.
Proceedings of the 34th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2007

2006
A Compositional Logic for Control Flow.
Proceedings of the Verification, 2006

Compiling with Continuations (corr. version).
Cambridge University Press, ISBN: 978-0-521-03311-4, 2006

2005
MulVAL: A Logic-based Network Security Analyzer.
Proceedings of the 14th USENIX Security Symposium, Baltimore, MD, USA, July 31, 2005

2004
Polymorphic Lemmas and Definitions in lambda-Prolog and Twelf.
Theory Pract. Log. Program., 2004

Dependent types ensure partial correctness of theorem provers.
J. Funct. Program., 2004

Construction of a Semantic Model for a Typed Assembly Language.
Proceedings of the Verification, 2004

Social processes and proofs of theorems and programs, revisited.
Proceedings of the ACM SIGPLAN 2004 Conference on Programming Language Design and Implementation 2004, 2004

2003
Mechanisms for secure modular programming in Java.
Softw. Pract. Exp., 2003

A Trustworthy Proof Checker.
J. Autom. Reason., 2003

Using Memory Errors to Attack a Virtual Machine.
Proceedings of the 2003 IEEE Symposium on Security and Privacy (S&P 2003), 2003

Policy-enforced linking of untrusted components.
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.
Proceedings of the 5th International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming, 2003

A provably sound TAL for back-end optimization.
Proceedings of the ACM SIGPLAN 2003 Conference on Programming Language Design and Implementation 2003, 2003

Access Control on the Web Using Proof-carrying Authorization.
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.
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.
Proceedings of the 17th IEEE Symposium on Logic in Computer Science (LICS 2002), 2002

Modern Compiler Implementation in Java, 2nd edition.
Cambridge University Press, ISBN: 0-521-82060-X, 2002

2001
An indexed model of recursive types for foundational proof-carrying code.
ACM Trans. Program. Lang. Syst., 2001

Type-preserving garbage collectors.
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.
Proceedings of the 2001 ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), 2001

Foundational Proof-Carrying Code.
Proceedings of the 16th Annual IEEE Symposium on Logic in Computer Science, 2001

2000
SAFKASI: a security mechanism for language-based systems.
ACM Trans. Softw. Eng. Methodol., 2000

Efficient and safe-for-space closure conversion.
ACM Trans. Program. Lang. Syst., 2000

Technological access control interferes with noninfringing scholarship.
Commun. ACM, 2000

A Semantic Model of Types and Machine Instuctions for Proof-Carrying Code.
Proceedings of the POPL 2000, 2000

Machine Instruction Syntax and Semantics in Higher Order Logic.
Proceedings of the Automated Deduction, 2000

1999
Hierarchical modularity.
ACM Trans. Program. Lang. Syst., 1999

Lightweight Lemmas in lambda-Prolog.
Proceedings of the Logic Programming: The 1999 International Conference, Las Cruces, New Mexico, USA, November 29, 1999

Proof-Carrying Authentication.
Proceedings of the CCS '99, 1999

1998
SSA is Functional Programming.
ACM SIGPLAN Notices, 1998

Traversal-Based Visualization of Data Structures.
Proceedings of the 1998 IEEE Symposium on Information Visualization (InfoVis '98), 1998

Modern Compiler Implementation in ML
Cambridge University Press, ISBN: 0-521-58274-1, 1998

Modern Compiler Implementation in C
Cambridge University Press, ISBN: 0-521-58390-X, 1998

Modern Compiler Implementation in Java
Cambridge University Press, ISBN: 0-521-58388-8, 1998

1997
Shrinking lambda Expressions in Linear Time.
J. Funct. Program., 1997

Lambda-Splitting: A Higher-Order Approach to Cross-Module Optimizations.
Proceedings of the 1997 ACM SIGPLAN International Conference on Functional Programming (ICFP '97), 1997

The Zephyr Abstract Syntax Description Language.
Proceedings of the Conference on Domain-Specific Languages, 1997

Modern Compiler Implementation in ML: Basic Techniques
Cambridge University Press, ISBN: 0-521-58775-1, 1997

Modern Compiler Implementation in C: Basic Techniques
Cambridge University Press, ISBN: 0-521-58653-4, 1997

Modern Compiler Implementation in Java: Basic Techniques
Cambridge University Press, ISBN: 0-521-58654-2, 1997

1996
Iterated Register Coalescing.
ACM Trans. Program. Lang. Syst., 1996

Intensional Equality ;=) for Continuations.
ACM SIGPLAN Notices, 1996

Empirical and Analytic Study of Stack Versus Heap Cost for Languages with Closures.
J. Funct. Program., 1996

1995
A Debugger for Standard ML.
J. Funct. Program., 1995

A Type-Based Compiler for Standard ML.
Proceedings of the ACM SIGPLAN'95 Conference on Programming Language Design and Implementation (PLDI), 1995

Cache Performance of Fast-Allocating Programs.
Proceedings of the seventh international conference on Functional programming languages and computer architecture, 1995

1994
Axiomatic Bootstrapping: A Guide for Compiler Hackers.
ACM Trans. Program. Lang. Syst., 1994

Loop Headers in Lambda-Calculus or CPS.
LISP Symb. Comput., 1994

Separate Compilation for Standard ML.
Proceedings of the ACM SIGPLAN'94 Conference on Programming Language Design and Implementation (PLDI), 1994

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

Space-Efficient Closure Representations.
Proceedings of the 1994 ACM Conference on LISP and Functional Programming, 1994

1993
A Critique of Standard ML.
J. Funct. Program., 1993

Smartest Recompilation.
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?
ACM SIGPLAN Notices, 1992

Callee-Save Registers in Continuation-Passing Style.
LISP Symb. Comput., 1992

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

1991
Standard ML of New Jersey.
Proceedings of the Programming Language Implementation and Logic Programming, 1991

Debuggable Concurrency Extensions for Standard ML.
Proceedings of the ACM/ONR Workshop on Parallel and Distributed Debugging, 1991

Virtual Memory Primitives for User Programs.
Proceedings of the ASPLOS-IV Proceedings, 1991

1990
A Runtime System.
LISP Symb. Comput., 1990

An Advisor for Flexible Working Sets.
Proceedings of the 1990 ACM SIGMETRICS conference on Measurement and modeling of computer systems, 1990

Debugging Standard ML Without Reverse Engineering.
Proceedings of the 1990 ACM Conference on LISP and Functional Programming, 1990

1989
Vectorized garbage collection.
J. Supercomput., 1989

Allocation without Locking.
Softw. Pract. Exp., 1989

Simple Generational Garbage Collection and Fast Allocation.
Softw. Pract. Exp., 1989

Runtime Tags Aren't Necessary.
LISP Symb. Comput., 1989

Continuation-Passing, Closure-Passing Style.
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.
IEEE Trans. Comput. Aided Des. Integr. Circuits Syst., 1988

The World's Fastest Scrabble Program.
Commun. ACM, 1988

Real-Time Concurrent Collection on Stock Multiprocessors.
Proceedings of the ACM SIGPLAN'88 Conference on Programming Language Design and Implementation (PLDI), 1988

Real-time concurrent collection on stock multiprocessors (with retrospective)
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.
Softw. Pract. Exp., 1987

Garbage Collection can be Faster than Stack Allocation.
Inf. Process. Lett., 1987

A Standard ML compiler.
Proceedings of the Functional Programming Languages and Computer Architecture, 1987

1985
Semantics-Directed Code Generation.
Proceedings of the Conference Record of the Twelfth Annual ACM Symposium on Principles of Programming Languages, 1985


  Loading...