Andrew Appel

Q: What Schools Are Affiliated With Andrew Appel

Andrew Appel is affiliated with the following schools: Clausthal University of Technology, Princeton University, Carnegie Mellon University

Andrew Appel's AcademicInfluence.com Rankings

Andrew Appel

Computer Science

#711

World Rank

#733

Historical Rank

#381

USA Rank

Database

#1147

World Rank

#1204

Historical Rank

#319

USA Rank

computer-science Degrees

Download Badge

Computer Science

Why Is Andrew Appel Influential?

(Suggest an Edit or Addition)

According to Wikipedia, Andrew Wilson Appel is the Eugene Higgins Professor of computer science at Princeton University. He is especially well-known because of his compiler books, the Modern Compiler Implementation in ML series, as well as Compiling With Continuations . He is also a major contributor to the Standard ML of New Jersey compiler, along with David MacQueen, John H. Reppy, Matthias Blume and others and one of the authors of Rog-O-Matic.

(See a Problem?)

Andrew Appel's Published Works

Number of citations in a given year to any of this author's works

Total number of citations to an author for the works they published in a given year. This highlights publication of the most important work(s) by the author

Published Works

Compiling with Continuations (1991) (1009)
MulVAL: A Logic-based Network Security Analyzer (2005) (651)
An Efficient Program for Many-Body Simulation (1985) (586)
Modern Compiler Implementation in Java (1997) (585)
Modern Compiler Implementation in ML (2007) (391)
Foundational proof-carrying code (2001) (356)
An indexed model of recursive types for foundational proof-carrying code (2001) (347)
Simple generational garbage collection and fast allocation (1989) (332)
Standard ML of New Jersey (1991) (325)
Proof-carrying authentication (1999) (297)
Virtual memory primitives for user programs (1991) (258)
Real-time concurrent collection on stock multiprocessors (1988) (229)
Iterated register coalescing (1996) (222)
Using memory errors to attack a virtual machine (2003) (214)
SSA is functional programming (1998) (196)
Continuation-passing, closure-passing style (1989) (194)
Garbage Collection can be Faster than Stack Allocation (1987) (182)
Program Logics - for Certified Compilers (2014) (169)
A semantic model of types and machine instructions for proof-carrying code (2000) (167)
A very modal model of a modern, major, general type system (2007) (165)
Formal aspects of mobile code security (1999) (165)
Oracle Semantics for Concurrent Separation Logic (2008) (163)
Optimal spilling for CISC machines with few registers (2001) (156)
Verified Software Toolchain (2012) (155)
A Standard ML compiler (1987) (136)
A type-based compiler for standard ML (1995) (135)
Verification of a Cryptographic Primitive: SHA-256 (2015) (131)
SAFKASI: a security mechanism for language-based systems (2000) (130)
A Fresh Look at Separation Algebras and Share Accounting (2009) (124)
The Zephyr Abstract Syntax Description Language (1997) (107)
Separation Logic for Small-Step cminor (2007) (104)
Modern Compiler Implementation in ML: Basic Techniques (1997) (99)
Verified Correctness and Security of OpenSSL HMAC (2015) (98)
Space-efficient closure representations (1994) (97)
Runtime tags aren't necessary (1989) (97)
The world's fastest Scrabble program (1988) (92)
Compositional CompCert (2015) (90)
Debugging standard ML without reverse engineering (1990) (89)
Iterated register coalescing (1996) (88)
Smartest recompilation (1993) (87)
CertiCoq : A verified compiler for Coq (2016) (84)
A runtime system (1990) (81)
A Debugger for Standard ML (1995) (75)
The CompCert Memory Model, Version 2 (2012) (70)
Modern Compiler Implementation in Java, 2nd edition (2002) (69)
Access control for the web via proof-carrying authorization (2003) (69)
Hierarchical modularity (1999) (64)
VST-Floyd: A Separation Logic Tool to Verify Correctness of C Programs (2018) (63)
Safe Java Native Interface (2006) (62)
Creating and preserving locality of java applications at allocation and garbage collection times (2002) (61)
A Trustworthy Proof Checker (2004) (60)
A stratified semantics of general references embeddable in higher-order logic (2002) (59)
Foundational proof checkers with small witnesses (2003) (59)
Type-preserving garbage collectors (2001) (56)
Shrinking lambda expressions in linear time (1997) (52)
A Compositional Logic for Control Flow (2006) (51)
A provably sound TAL for back-end optimization (2003) (51)
Machine Instruction Syntax and Semantics in Higher Order Logic (2000) (50)
Separate compilation for Standard ML (1994) (50)
A logic-programming approach to network security analysis (2005) (49)
Verified Software Toolchain - (Invited Talk) (2011) (47)
An Empirical and Analytic Study of Stack vs . Heap Cost for Languages with Closures (1993) (47)
Empirical and analytic study of stack versus heap cost for languages with closures (1996) (46)
Garbage Collection: Algorithms for Automatic Dynamic Memory Management by Richard Jones and Rafael Lins, John Wiley & Sons, 1996. (1997) (46)
Verified Compilation for Shared-Memory C (2014) (45)
Unrolling lists (1994) (45)
Verified Correctness and Security of mbedTLS HMAC-DRBG (2017) (44)
A critique of Standard ML (1993) (42)
Hash-consing Garbage Collection (1993) (42)
Semantic foundations for typed assembly languages (2010) (40)
A theory of indirection via approximation (2010) (40)
Position paper: the science of deep specification (2017) (38)
Callee-save registers in continuation-passing style (1992) (35)
Real-time concurrent collection on stock multiprocessors (1988) (34)
Efficient and safe-for-space closure conversion (2000) (33)
An advisor for flexible working sets (1990) (32)
The New Jersey Voting-machine Lawsuit and the AVC Advantage DRE Voting Machine (2009) (32)
Mechanisms for secure modular programming in Java (2003) (31)
Oracle semantics (2008) (30)
Formal Verification of Coalescing Graph-Coloring Register Allocation (2010) (29)
Lambda-splitting: a higher-order approach to cross-module optimizations (1997) (29)
Space-E cient Closure Representations (1994) (29)
An Indexed Model of Impredicative Polymorphism and Mutable References (2003) (28)
Concurrent Separation Logic for Pipelined Parallelization (2010) (28)
Dependent types ensure partial correctness of theorem provers (2004) (27)
Foundational proof-carrying code (2003) (27)
Debuggable concurrency extensions for standard ML (1991) (27)
Semantics-directed code generation (1985) (27)
Windows Access Control Demystified ∗ (2006) (26)
Simulating digital circuits with one bit per wire (1988) (26)
Portable Software Fault Isolation (2014) (26)
Construction of a Semantic Model for a Typed Assembly Language (2004) (25)
Modern Compiler Implementation in Java: Basic Techniques (1997) (25)
Deobfuscation is in NP (24)
An efficient program for many-body simulations (or, Cray performance from a VAX) (1983) (23)
VeriSmall: Verified Smallfoot Shape Analysis (2011) (22)
Rog-O-Matic : a belligerent expert system (1983) (22)
Traversal-based visualization of data structures (1998) (21)
Security Seals on Voting Machines: A Case Study (2011) (21)
A Certificate Infrastructure for Machine-Checked Proofs of Conditional Information Flow (2012) (21)
Cache performance of fast-allocating programs (1995) (20)
Generalizations of the sethi‐ullman algorithm for register allocation (1987) (20)
Efficient Verified Red-Black Trees (2011) (20)
Closure conversion is safe for space (2019) (18)
Models for Security Policies in Proof-Carrying Code (18)
Ballot-Marking Devices (BMDs) Cannot Assure the Will of the Voters (2019) (17)
The CompCert memory model (2014) (17)
A verified messaging system (2017) (17)
Bringing Order to the Separation Logic Jungle (2017) (17)
Verified heap theorem prover by paramodulation (2012) (16)
Axiomatic bootstrapping: a guide for compiler hackers (1994) (16)
Ballot-Marking Devices Cannot Ensure the Will of the Voters (2020) (15)
Access control on the Web using proof-carrying authorization (2003) (14)
A List-Machine Benchmark for Mechanized Metatheory (2012) (14)
Principles and a Preliminary Design for ML2000 (2000) (14)
A compositional logic for control flow and its application in foundational proof-carrying code (2005) (13)
Lightweight Lemmas in lambda-Prolog (1999) (12)
Abstraction and subsumption in modular verification of C programs (2019) (12)
Typed machine language (2003) (12)
JVM TCB: Measurements of the Trusted Computing Base of Java Virtual Machines (12)
Multimodal Separation Logic for Reasoning About Operational Semantics (2008) (11)
Alan Turing's Systems of Logic: The Princeton Thesis (2012) (11)
Loop headers in λ-calculus or CPS (1994) (10)
Proof Pearl: Magic Wand as Frame (2019) (10)
Allocation without locking (1989) (10)
ML-Yacc User's Manual Version 2.4 (2000) (9)
Compositional optimizations for CertiCoq (2021) (9)
Modern Compiler Implementation in Java: Bibliography (2002) (9)
The approximation modality in models of higher-order types (2010) (9)
Typed Machine Language and its Semantics (2001) (9)
Modular Verification for Computer Security (2016) (9)
Operational refinement for compiler correctness (2012) (8)
Emulating Write-Allocate on a No-Write-Allocate Cache (1994) (8)
Verified sequential Malloc/Free (2020) (8)
Connecting Higher-Order Separation Logic to a First-Order Outside World (2020) (8)
Shrink fast correctly! (2017) (8)
Dictionary Passing for Polytypic Polymorphism (8)
Eective audit policy for voter-verified paper ballots (2007) (8)
Lightweight Lemmas in lProlog (1999) (8)
Event-Based Realization of Dynamic Adaptive Systems (2010) (7)
A List-machine Benchmark for Mechanized Metatheory: (Extended Abstract) (2007) (7)
Policy-enforced linking of untrusted components (2003) (7)
Compile-time evaluation and code generation for semantics-directed compilers (denotational) (1985) (7)
Polymorphic lemmas and definitions in $\lambda$Prolog and Twelf (2004) (7)
Insecurities and Inaccuracies of the Sequoia AVC Advantage 9 . 00 H DRE Voting Machine (2008) (7)
Safe Garbage Collection = Regions + Intensional Type Analysis (7)
Concise specifications of locally optimal code generators (1987) (7)
Vectorized garbage collection (1989) (7)
Technological access control interferes with noninfringing scholarship. (2000) (6)
Copying Garbage Collection in the Presence of Ambiguous References (1988) (6)
Compiling with Continuations (corr. version) (2006) (6)
Modern Compiler Implementation in Java: Static Single-Assignment Form (2002) (6)
A Stratified Semantics of General References A Stratified Semantics of General References (2002) (6)
Modelling the CoCoME with DisCComp (2007) (6)
A Kind System for Typed Machine Language (2002) (6)
Program Logics for Certified Compilers: Hoare logic (2014) (6)
Intensional equality ;=) for continuations (1996) (6)
A Logical Mix of Approximation and Separation (2010) (5)
A low-level typed assembly language with a machine-checkable soundness proof (2004) (5)
Loop Headers in Lambda-Calculus or CPS (1994) (5)
Mostly Sound Type System Improves a Foundational Program Verifier (2013) (5)
Network Security Management with High-level Security Policies (5)
Verification of a cryptographic primitive: SHA-256 (abstract) (2015) (4)
Lightweight Lemmas in λ Prolog (1999) (4)
Compiling with Continuations: Continuation-passing style (1991) (4)
Re-opening Closures (1988) (4)
Oracle Semantics for Concurrent Separation Logic (Extended Version) (2008) (4)
Interfacing compilers, proof checkers, and proofs for foundational proof-carrying code (2005) (4)
Policy-based Multihost Multistage Vulnerability Analysis ∗ (4)
Modern Compiler Implementation in Java: Introduction (2002) (4)
Semantics of General References by a Hierarchy of Gödel Numberings (3)
Policy-Enforced Linking of Untrusted Components (Extended Abstract) (2003) (3)
Designing extensible , domain-specific languages for mathematical diagrams (2016) (3)
Modern Compiler Implementation in Java: The Memory Hierarchy (2002) (2)
Coq’s vibrant ecosystem for verification engineering (invited talk) (2022) (2)
Foundational High-level Static Analysis (2008) (2)
Special Issue on ML (1992) (2)
Is POPL mathematics or science? (1992) (2)
Separation Logic for Small-step Cminor (extended version) (2007) (2)
Deriving efficient program transformations from rewrite rules (2021) (2)
Secure linking: a logical framework for policy-enforced component composition (2004) (2)
C-language floating-point proofs layered with VST and Flocq (2020) (2)
C floating-point proofs layered with VST and Flocq (2020) (2)
Foundational semantics for tal syntactic rules via typed machine language (2002) (2)
Type-Preserving Garbage Collectors (Extended Version) (2)
Local actions for a curry-style operational semantics (2011) (2)
Certified code generation from CPS to C (2019) (2)
Should Your Specification Language Be Typed ? (1999) (2)
Modern Compiler Implementation in ML: Object-Oriented Languages (1997) (2)
Compiling with Continuations: The runtime system (1991) (2)
Making Lambda Calculus Smaller , Faster (1994) (2)
Polymorphic Lemmas and De nitions in Prolog and Twelf (2004) (2)
Modern Compiler Implementation in ML: Preface (1997) (1)
Viewpoint: Technological access control interferes with noninfringing scholarship (2000) (1)
A formal approach to practical network security management (2006) (1)
Hierarchical Modularity: Compilation Management for Standard ML (1997) (1)
Modern Compiler Implementation in Java: Appendix: MiniJava Language Reference Manual (2002) (1)
Tactics for Separation Logic early draft (1)
Scaling Proof-Carrying Code to Production Compilers and Security Policies (2005) (1)
How to Edit a Journal by E-mail (2004) (1)
Higher order separation logic (2014) (1)
Automatic Conﬁguration Vulnerability Analysis (2007) (1)
Verified Numerical Methods for Ordinary Differential Equations (2022) (1)
Efficient Extensional Binary Tries (2021) (1)
Modern Compiler Implementation in C: Introduction (1997) (1)
Compiling with Continuations: The abstract machine (1991) (1)
Managing memory with types (2002) (1)
Program Logics for Certified Compilers: Mechanized Semantic Library (2014) (1)
Modern Compiler Implementation in ML by Andrew W. Appel (1997) (1)
Pipelining and Scheduling (1997) (0)
A Solver for Arrays with Concatenation (2023) (0)
Compiling with Continuations: Bibliography (1991) (0)
Operational semantics of CompCert (2014) (0)
Security and document compatibility for electronic refereeing (1996) (0)
Lifted separation logics (2014) (0)
Ar tifact * A E C Compositional CompCert (2014) (0)
Higher-order Hoare logic (2014) (0)
Technical Perspective: The scalability of CertiKOS (2019) (0)
Compiling with Continuations: Semantics of the CPS (1991) (0)
Compiling with Continuations: Introduction to ML (1991) (0)
Session details: Verification (2009) (0)
Compiling with Continuations: Readings (1991) (0)
Soundness of Hoare logic (2014) (0)
Modern Compiler Implementation in Java: Semantic Analysis (2002) (0)
Semantic models of predicates-in-the-heap (2014) (0)
Program Logics for Certified Compilers: Covariant recursive predicates (2014) (0)
Separation logic for CompCert (2014) (0)
New Results - Mechanization of type systems and axiomatic and operational semantics (2007) (0)
Program Logics for Certified Compilers: Separation algebras (2014) (0)
Operators on separation algebras (2014) (0)
Preface (2021) (0)
The Birth of Computer Science at Princeton in the 1930s (2012) (0)
Safe Heterogeneous Applications : Curing the Java Native Interface ∗ (0)
Modular Verification for Computer Security ( Invited Paper ) (2016) (0)
Typechecking for Verifiable C (2014) (0)
More C programs (2014) (0)
Oracle Semantics for Concurrent Separation Logic ( preliminary version ) (2007) (0)
Compiling with Continuations: Conversion into CPS (1991) (0)
Program Logics for Certified Compilers: Separation logic as a logic (2014) (0)
Object-Oriented Languages (1997) (0)
Separation algebra for CompCert (2014) (0)
Modern Compiler Implementation in ML: The Memory Hierarchy (1997) (0)
Appendix: Tiger Language Reference Manual (1997) (0)
Program Logics for Certified Compilers: Share accounting (2014) (0)
Predicate implication and subtyping (2014) (0)
Applying higher-order separation logic (2014) (0)
A List-Machine Benchmark for Mechanized Metatheory (2011) (0)
A Debugger for Standard Ml 1 (1993) (0)
How to specify a compiler (2014) (0)
Compiling with Continuations: Machine-code generation (1991) (0)
Modern Compiler Implementation in C: Instruction Selection (1997) (0)
Modern Compiler Implementation in ML: Abstract Syntax (1997) (0)
Modern Compiler Implementation in ML: Polymorphic Types (1997) (0)
Basic Blocks and Traces (1997) (0)
Compiling with Continuations: Space complexity (1991) (0)
Case study: Lambda-calculus with references (2014) (0)
Derived rules and proof automation for C light (2014) (0)
Optimization of the CPS (1991) (0)
Modern Compiler Implementation in ML: Dataflow Analysis (1997) (0)
Social processes and proofs of theorems and programs, revisited (2004) (0)
Introduction to step-indexing (2014) (0)
Program Logics for Certified Compilers: The VST separation logic for C light (2014) (0)
Data structures in indirection theory (2014) (0)
Compiling with Continuations: Common subexpressions (1991) (0)
A Project Summary High-Assurance Common Language Runtime (2002) (0)
Modern Compiler Implementation in ML: Basic Blocks and Traces (1997) (0)
Modern Compiler Implementation in Java: Translation to Intermediate Code (1997) (0)
Modern Compiler Implementation in Java: Liveness Analysis (2002) (0)
Chapter 13 Event-Based Realization of Dynamic Adaptive Systems (2015) (0)
Modern Compiler Implementation in Java: Polymorphic Types (2002) (0)
Program Logics for Certified Compilers: Separation logic (2014) (0)
Modern Compiler Implementation in C: Bibliography (1997) (0)
Modern Compiler Implementation in C: Putting It All Together (1997) (0)
Foundational static analysis (2014) (0)
Modern Compiler Implementation in C: Semantic Analysis (1997) (0)
Program Logics for Certified Compilers: Simplification by rewriting (2014) (0)
Modern Compiler Implementation in ML: Activation Records (1997) (0)
Modern Compiler Implementation in C: Static Single-Assignment Form (1997) (0)
Compiling with Continuations: Register spilling (1991) (0)
Modern Compiler Implementation in ML: Bibliography (1997) (0)
Modern Compiler Implementation in ML: Lexical Analysis (1997) (0)
Secure Linking: a Framework for Trusted Software Components (0)
Jacke – A Parser-Generator Tool for Standard (0)
Corrigendum: C floating-point proofs layered with VST and Flocq (2020) (0)
ML-specific optimizations (1991) (0)
C light operational semantics (2014) (0)
Higher-order semantic models (2014) (0)
A Type-Based Compiler for Standard ML Zhong (1994) (0)
Compiling with Continuations: Obtaining Standard ML of New Jersey (1991) (0)
Modern Compiler Implementation in ML: Instruction Selection (1997) (0)
Modern Compiler Implementation in ML: Garbage Collection (1997) (0)
Special Issue on ML (1993) (0)
Compiling with Continuations: Beta expansion (1991) (0)
VST-Floyd: A Separation Logic Tool to Verify Correctness of C Programs (2018) (0)
Program Logics for Certified Compilers: Generic separation logic (2014) (0)
Semantic model and soundness of Verifiable C (2014) (0)
Expressions, values, and assertions (2014) (0)
Compiling with Continuations: Performance evaluation (1991) (0)
Towards Verified Shared-memory Cooperation for C (2013) (0)
Separation Logic Predicates for Aggregate Data Types (2017) (0)
Semantic model of CSL (2014) (0)
Compiling with Continuations: Parallel programming (1991) (0)
A Second Edition : Verification of a Cryptographic Primitive : SHA-256 (2016) (0)
Modern Compiler Implementation in ML: Register Allocation (1997) (0)
A Type-based Compiler for Standard Ml a Type-based Compiler for Standard Ml (1994) (0)
Modern Compiler Implementation in C: Register Allocation (1997) (0)
Is Internet Voting Trustworthy? The Science and the Policy Battles (2022) (0)
Proof-Carrying Code with Correct Compilers (2009) (0)
Program Logics for Certified Compilers: Introduction (2014) (0)
Functional Programming Languages (1997) (0)
Modern Compiler Implementation in Java: Register Allocation (2002) (0)
The Performance of Italian Basso Continuo: Style in Keyboard Accompaniment in the Seventeenth and Eighteenth Centuries (review) (2008) (0)
Modern Compiler Implementation in C: Lexical Analysis (1997) (0)
Real-time concurrent collection on stock multiprocessors (with retrospective) (1988) (0)
Session details: Separation logic (2014) (0)
General recursive predicates (2014) (0)
Modern Compiler Implementation in ML: Pipelining and Scheduling (1997) (0)
From separation algebras to separation logic (2014) (0)
Program Logics for Certified Compilers: Road map (2014) (0)
Putting order to the separation logic jungle (2017) (0)
Roundtable Panel II: Digital Video (2001) (0)
Modern Compiler Implementation in ML: Putting It All Together (1997) (0)
Modern Compiler Implementation in ML: Static Single-Assignment Form (1997) (0)
Veriﬁed Numerical Methods for Ordinary Diﬀerential Equations (2022) (0)
Optimal Spilling for CISC Machines with Few (2000) (0)
Program Logics for Certified Compilers: Proof of a program (2014) (0)
Modular structure of the development (2014) (0)
Modern Compiler Implementation in Java: Lexical Analysis (2002) (0)
Modeling the Hoare judgment (2014) (0)
Concurrent separation logic (2014) (0)
Dependently typed C programs (2014) (0)
Compiling with Continuations: Overview (1991) (0)
5.4 Summary of the Performance of Translated Java Code 5.2 the Inevitable Factors 5.2.1 Memory Allocation and Lack of Stack Locality 5.1 the Evitable Factors 5 Bridging the Performance Gap 4.2 Application Programs (2007) (0)
A little case study (2014) (0)
First-order separation logic (2014) (0)
Heap theorem prover (2014) (0)
Program Logics for Certified Compilers: Bibliography (2014) (0)
Verified Erasure Correction in Coq with MathComp and VST (2022) (0)
Case study: Separation logic with first-class functions (2014) (0)
A Coinductive Formulation of the \coinduction Theorem" by Michael and Appel (2000) (0)

This paper list is powered by the following services:

Other Resources About Andrew Appel

en.wikipedia.org

What Schools Are Affiliated With Andrew Appel?

Andrew Appel is affiliated with the following schools:

Andrew Appel's Academic­Influence.com Rankings