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: Appel:Andrew_W=
Facilitated 1 volumes:
EdContributed to:
20152015
2014
2012201120102010
201020082007
200620042004
20032003
2003
2002
2002200120012001
20002000
199919971996
19951995
199419941993
1991199119901989198819881987198520172017Wrote 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.