BibSLEIGH
BibSLEIGH corpus
BibSLEIGH tags
BibSLEIGH bundles
BibSLEIGH people
EDIT!
CC-BY
Open Knowledge
XHTML 1.0 W3C Rec
CSS 2.1 W3C CanRec
email twitter
Travelled to:
1 × Cyprus
1 × Finland
1 × Hungary
1 × India
1 × Spain
1 × Sweden
1 × The Netherlands
1 × United Kingdom
2 × Denmark
2 × Germany
21 × USA
4 × France
Collaborated with:
Z.Shao D.B.MacQueen L.George A.P.Felty G.Stewart L.Beringer D.Wu K.Li G.Tan A.Hobor R.Dockins E.Lee D.C.Wang N.G.Michael M.Blume M.J.R.Gonçalves A.P.Tolmach T.Jim Olivier Savary Bélanger S.Blazy B.Robillard C.J.Bell D.Walker F.Z.Nardelli A.Stump A.J.Ahmed R.Virga J.H.Reppy J.R.Ellis W.Mansky A.Nogin S.Cuellar P.Melliès C.D.Richards J.Vouillon K.N.Swadi J.Chen H.Fang Y.Shuf M.Gupta H.Franke J.P.Singh
Talks about:
semant (7) standard (5) type (5) ml (5) concurr (4) verifi (4) compil (4) proof (4) logic (4) program (3)

Person: Andrew W. Appel

DBLP DBLP: Appel:Andrew_W=

Facilitated 1 volumes:

POPL 1999Ed

Contributed to:

PLDI 20152015
POPL 20152015
ESOP 20142014
ICFP 20122012
ESOP 20112011
ESOP 20102010
POPL 20102010
SAS 20102010
ESOP 20082008
POPL 20072007
VMCAI 20062006
PLDI 20042004
VMCAI 20042004
ESEC/FSE 20032003
PLDI 20032003
PPDP 20032003
LICS 20022002
OOPSLA 20022002
LICS 20012001
PLDI 20012001
POPL 20012001
CADE 20002000
POPL 20002000
ICLP 19991999
ICFP 19971997
POPL 19961996
FPCA 19951995
PLDI 19951995
LFP 19941994
PLDI 19941994
POPL 19931993
ASPLOS 19911991
PLILP 19911991
LFP 19901990
POPL 19891989
Best of PLDI 20041988
PLDI 19881988
FPCA 19871987
POPL 19851985
OOPSLA 20172017
PPDP 20172017

Wrote 42 papers:

PLDI-2015-Appel #encryption #verification
Verification of a cryptographic primitive: SHA-256 (AWA), p. 153.
POPL-2015-StewartBCA #composition
Compositional CompCert (GS, LB, SC, AWA), pp. 275–287.
ESOP-2014-BeringerSDA #c #compilation
Verified Compilation for Shared-Memory C (LB, GS, RD, AWA), pp. 107–127.
ICFP-2012-StewartBA #proving #theorem proving
Verified heap theorem prover by paramodulation (GS, LB, AWA), pp. 3–14.
ESOP-2011-Appel
Verified Software Toolchain — (AWA), pp. 1–17.
ESOP-2010-BlazyRA #graph #verification
Formal Verification of Coalescing Graph-Coloring Register Allocation (SB, BR, AWA), pp. 145–164.
POPL-2010-HoborDA #approximate #formal method
A theory of indirection via approximation (AH, RD, AWA), pp. 171–184.
SAS-2010-BellAW #concurrent #logic #parallel #pipes and filters
Concurrent Separation Logic for Pipelined Parallelization (CJB, AWA, DW), pp. 151–166.
ESOP-2008-HoborAN #concurrent #logic #semantics
Oracle Semantics for Concurrent Separation Logic (AH, AWA, FZN), pp. 353–367.
POPL-2007-AppelMRV #type system
A very modal model of a modern, major, general type system (AWA, PAM, CDR, JV), pp. 109–122.
VMCAI-2006-TanA #composition #control flow #logic
A Compositional Logic for Control Flow (GT, AWA), pp. 80–94.
PLDI-2004-Appel #process #proving #revisited #social #source code #theorem
Social processes and proofs of theorems and programs, revisited (AWA), p. 170.
VMCAI-2004-TanASW #assembly #semantics
Construction of a Semantic Model for a Typed Assembly Language (GT, AWA, KNS, DW), pp. 30–43.
ESEC-FSE-2003-LeeA #component
Policy-enforced linking of untrusted components (EL, AWA), pp. 371–374.
PLDI-2003-ChenWAF #optimisation
A provably sound TAL for back-end optimization (JC, DW, AWA, HF), pp. 208–219.
PPDP-2003-WuAS #proving
Foundational proof checkers with small witnesses (DW, AWA, AS), pp. 264–274.
LICS-2002-AhmedAV #semantics
A Stratified Semantics of General References A Stratified Semantics of General References (AJA, AWA, RV), p. 75–?.
OOPSLA-2002-ShufGFAS #garbage collection #java #locality
Creating and preserving locality of java applications at allocation and garbage collection times (YS, MG, HF, AWA, JPS), pp. 13–25.
LICS-2001-Appel
Foundational Proof-Carrying Code (AWA), pp. 247–256.
PLDI-2001-AppelG
Optimal Spilling for CISC Machines with Few Registers (AWA, LG), pp. 243–253.
POPL-2001-WangA #garbage collection
Type-preserving garbage collectors (DCW, AWA), pp. 166–178.
CADE-2000-MichaelA #bytecode #higher-order #logic #semantics #syntax
Machine Instruction Syntax and Semantics in Higher Order Logic (NGM, AWA), pp. 7–24.
POPL-2000-AppelF #semantics
A Semantic Model of Types and Machine Instuctions for Proof-Carrying Code (AWA, APF), pp. 243–253.
ICLP-1999-AppelF #lightweight #prolog
Lightweight Lemmas in λ-Prolog (AWA, APF), pp. 411–425.
ICFP-1997-BlumeA #approach #higher-order #named #optimisation
λ-Splitting: A Higher-Order Approach to Cross-Module Optimizations (MB, AWA), pp. 112–124.
POPL-1996-GeorgeA
Iterated Register Coalescing (LG, AWA), pp. 208–218.
FPCA-1995-GoncalvesA #performance #source code
Cache Performance of Fast-Allocating Programs (MJRG, AWA), pp. 293–305.
PLDI-1995-ShaoA #compilation #ml #standard #type system
A Type-Based Compiler for Standard ML (ZS, AWA), pp. 116–129.
LFP-1994-ShaoA
Space-Efficient Closure Representations (ZS, AWA), pp. 150–161.
LFP-1994-ShaoRA
Unrolling Lists (ZS, JHR, AWA), pp. 185–195.
PLDI-1994-AppelM #compilation #ml #standard
Separate Compilation for Standard ML (AWA, DBM), pp. 13–23.
POPL-1993-ShaoA
Smartest Recompilation (ZS, AWA), pp. 439–450.
ASPLOS-1991-AppelL #memory management #source code
Virtual Memory Primitives for User Programs (AWA, KL), pp. 96–107.
PLILP-1991-AppelM #ml #standard
Standard ML of New Jersey (AWA, DBM), pp. 1–13.
LFP-1990-TolmachA #debugging #ml #reverse engineering #standard
Debugging Standard ML Without Reverse Engineering (APT, AWA), pp. 1–12.
POPL-1989-AppelJ #continuation
Continuation-Passing, Closure-Passing Style (AWA, TJ), pp. 293–302.
Best-of-PLDI-1988-Appel #concurrent #multi #realtime
Real-time concurrent collection on stock multiprocessors (with retrospective) (AWA), pp. 205–216.
PLDI-1988-AppelEL #concurrent #multi #realtime
Real-Time Concurrent Collection on Stock Multiprocessors (AWA, JRE, KL), pp. 11–20.
FPCA-1987-AppelM #compilation #ml #standard
A Standard ML compiler (AWA, DBM), pp. 301–324.
POPL-1985-Appel #code generation #semantics
Semantics-Directed Code Generation (AWA), pp. 315–324.
OOPSLA-2017-ManskyAN
A verified messaging system (WM, AWA, AN), p. 28.
PPDP-2017-BelangerA #exclamation #performance
Shrink fast correctly! (OSB, AWA), pp. 49–60.

Bibliography of Software Language Engineering in Generated Hypertext (BibSLEIGH) is created and maintained by Dr. Vadim Zaytsev.
Hosted as a part of SLEBOK on GitHub.