@article{BauerAF03,
  title = {Mechanisms for secure modular programming in Java},
  author = {Lujo Bauer and Andrew W. Appel and Edward W. Felten},
  year = {2003},
  tags = {Java, programming},
  researchr = {https://researchr.org/publication/BauerAF03},
  cites = {0},
  citedby = {0},
  journal = {Software: Practice and Experience},
  volume = {33},
  number = {5},
  pages = {461-480},
}

@book{Appel1998ml,
  title = {Modern Compiler Implementation in ML},
  author = {Andrew W. Appel},
  year = {1998},
  tags = {compiler},
  researchr = {https://researchr.org/publication/Appel1998ml},
  cites = {0},
  citedby = {0},
  publisher = {Cambridge University Press},
  isbn = {0-521-58274-1},
}

@inproceedings{StewartBCA15,
  title = {Compositional CompCert},
  author = {Gordon Stewart and Lennart Beringer and Santiago Cuellar and Andrew W. Appel},
  year = {2015},
  doi = {10.1145/2676726.2676985},
  url = {http://doi.acm.org/10.1145/2676726.2676985},
  researchr = {https://researchr.org/publication/StewartBCA15},
  cites = {0},
  citedby = {0},
  pages = {275-287},
  booktitle = {Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2015, Mumbai, India, January 15-17, 2015},
  editor = {Sriram K. Rajamani and David Walker},
  publisher = {ACM},
  isbn = {978-1-4503-3300-9},
}

@inproceedings{TolmachA90,
  title = {Debugging Standard ML Without Reverse Engineering},
  author = {Andrew P. Tolmach and Andrew W. Appel},
  year = {1990},
  doi = {10.1145/91556.91564},
  url = {http://doi.acm.org/10.1145/91556.91564},
  tags = {reverse engineering, debugging},
  researchr = {https://researchr.org/publication/TolmachA90},
  cites = {0},
  citedby = {0},
  pages = {1-12},
  booktitle = {LISP and Functional Programming},
}

@inproceedings{BeringerSDA14,
  title = {Verified Compilation for Shared-Memory C},
  author = {Lennart Beringer and Gordon Stewart and Robert Dockins and Andrew W. Appel},
  year = {2014},
  doi = {10.1007/978-3-642-54833-8_7},
  url = {http://dx.doi.org/10.1007/978-3-642-54833-8_7},
  researchr = {https://researchr.org/publication/BeringerSDA14},
  cites = {0},
  citedby = {0},
  pages = {107-127},
  booktitle = {Programming Languages and Systems - 23rd European Symposium on Programming, ESOP 2014, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2014, Grenoble, France, April 5-13, 2014, Proceedings},
  editor = {Zhong Shao},
  volume = {8410},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  isbn = {978-3-642-54832-1},
}

@book{Appel1997ml,
  title = {Modern Compiler Implementation in ML: Basic Techniques},
  author = {Andrew W. Appel},
  year = {1997},
  tags = {compiler},
  researchr = {https://researchr.org/publication/Appel1997ml},
  cites = {0},
  citedby = {0},
  publisher = {Cambridge University Press},
  isbn = {0-521-58775-1},
}

@inproceedings{AmtoftDZABHOC12,
  title = {A Certificate Infrastructure for Machine-Checked Proofs of Conditional Information Flow},
  author = {Torben Amtoft and Josiah Dodds and Zhi Zhang and Andrew W. Appel and Lennart Beringer and John Hatcliff and Xinming Ou and Andrew Cousino},
  year = {2012},
  doi = {10.1007/978-3-642-28641-4_20},
  url = {http://dx.doi.org/10.1007/978-3-642-28641-4_20},
  researchr = {https://researchr.org/publication/AmtoftDZABHOC12},
  cites = {0},
  citedby = {0},
  pages = {369-389},
  booktitle = {Principles of Security and Trust - First International Conference, POST 2012, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2012, Tallinn, Estonia, March 24 - April 1, 2012, Proceedings},
  editor = {Pierpaolo Degano and Joshua D. Guttman},
  volume = {7215},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  isbn = {978-3-642-28640-7},
}

@inproceedings{DockinsHA09,
  title = {A Fresh Look at Separation Algebras and Share Accounting},
  author = {Robert Dockins and Aquinas Hobor and Andrew W. Appel},
  year = {2009},
  url = {http://springerlink.metapress.com/content/rp5547377166x21j/},
  tags = { algebra},
  researchr = {https://researchr.org/publication/DockinsHA09},
  cites = {0},
  citedby = {0},
  pages = {161-177},
  booktitle = {Programming Languages and Systems, 7th Asian Symposium, APLAS 2009, Seoul, Korea, December 14-16, 2009. Proceedings},
  editor = {Zhenjiang Hu},
  volume = {5904},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  isbn = {978-3-642-10671-2},
}

@article{AppelS96,
  title = {Empirical and Analytic Study of Stack Versus Heap Cost for Languages with Closures},
  author = {Andrew W. Appel and Zhong Shao},
  year = {1996},
  tags = {empirical},
  researchr = {https://researchr.org/publication/AppelS96},
  cites = {0},
  citedby = {0},
  journal = {Journal of Functional Programming},
  volume = {6},
  number = {1},
  pages = {47-74},
}

@inproceedings{BeringerPYA15,
  title = {Verified Correctness and Security of OpenSSL HMAC},
  author = {Lennart Beringer and Adam Petcher and Katherine Q. Ye and Andrew W. Appel},
  year = {2015},
  url = {https://www.usenix.org/conference/usenixsecurity15/technical-sessions/presentation/beringer},
  researchr = {https://researchr.org/publication/BeringerPYA15},
  cites = {0},
  citedby = {0},
  pages = {207-221},
  booktitle = {24th USENIX Security Symposium, USENIX Security 15, Washington, D.C., USA, August 12-14, 2015},
  editor = {Jaeyeon Jung and Thorsten Holz},
  publisher = {USENIX Association},
}

@inproceedings{ChenWAF03,
  title = {A provably sound TAL for back-end optimization},
  author = {Juan Chen and Dinghao Wu and Andrew W. Appel and Hai Fang},
  year = {2003},
  doi = {10.1145/781131.781155},
  url = {http://doi.acm.org/10.1145/781131.781155},
  tags = {optimization},
  researchr = {https://researchr.org/publication/ChenWAF03},
  cites = {0},
  citedby = {0},
  pages = {208-219},
  booktitle = {Proceedings of the ACM SIGPLAN 2003 Conference on Programming Language Design and Implementation 2003, San Diego, California, USA, June 9-11, 2003},
  publisher = {ACM},
  isbn = {1-58113-662-5},
}

@article{AppelF04:0,
  title = {Polymorphic Lemmas and Definitions in lambda-Prolog and Twelf},
  author = {Andrew W. Appel and Amy P. Felty},
  year = {2004},
  tags = {Prolog},
  researchr = {https://researchr.org/publication/AppelF04%3A0},
  cites = {0},
  citedby = {0},
  journal = {TPLP},
  volume = {4},
  number = {1-2},
  pages = {1-39},
}

@inproceedings{AppelL91,
  title = {Virtual Memory Primitives for User Programs},
  author = {Andrew W. Appel and Kai Li},
  year = {1991},
  researchr = {https://researchr.org/publication/AppelL91},
  cites = {0},
  citedby = {0},
  pages = {96-107},
  booktitle = {ASPLOS},
}

@book{Appel1998,
  title = {Modern Compiler Implementation in Java},
  author = {Andrew W. Appel},
  year = {1998},
  tags = {Java, compiler},
  researchr = {https://researchr.org/publication/Appel1998},
  cites = {0},
  citedby = {0},
  publisher = {Cambridge University Press},
  isbn = {0-521-58388-8},
}

@inproceedings{Appel15-0,
  title = {Verification of a cryptographic primitive: SHA-256 (abstract)},
  author = {Andrew W. Appel},
  year = {2015},
  doi = {10.1145/2737924.2774972},
  url = {http://doi.acm.org/10.1145/2737924.2774972},
  researchr = {https://researchr.org/publication/Appel15-0},
  cites = {0},
  citedby = {0},
  pages = {153},
  booktitle = {Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation, Portland, OR, USA, June 15-17, 2015},
  editor = {David Grove and Steve Blackburn},
  publisher = {ACM},
  isbn = {978-1-4503-3468-6},
}

@inproceedings{ShaoA95,
  title = {A Type-Based Compiler for Standard ML},
  author = {Zhong Shao and Andrew W. Appel},
  year = {1995},
  tags = {rule-based, compiler},
  researchr = {https://researchr.org/publication/ShaoA95},
  cites = {0},
  citedby = {0},
  pages = {116-129},
  booktitle = {PLDI},
}

@article{WallachAF00,
  title = {SAFKASI: a security mechanism for language-based systems},
  author = {Dan S. Wallach and Andrew W. Appel and Edward W. Felten},
  year = {2000},
  doi = {10.1145/363516.363520},
  url = {http://doi.acm.org/10.1145/363516.363520},
  tags = {rule-based, security},
  researchr = {https://researchr.org/publication/WallachAF00},
  cites = {0},
  citedby = {0},
  journal = {ACM Transactions on Software Engineering Methodology},
  volume = {9},
  number = {4},
  pages = {341-378},
}

@article{Appel94:0,
  title = {Axiomatic Bootstrapping: A Guide for Compiler Hackers},
  author = {Andrew W. Appel},
  year = {1994},
  doi = {10.1145/197320.197336},
  url = {http://doi.acm.org/10.1145/197320.197336},
  tags = {compiler},
  researchr = {https://researchr.org/publication/Appel94%3A0},
  cites = {0},
  citedby = {0},
  journal = {ACM Transactions on Programming Languages and Systems},
  volume = {16},
  number = {6},
  pages = {1699-1718},
}

@inproceedings{BauerSFA03,
  title = {Access Control on the Web Using Proof-carrying Authorization},
  author = {Lujo Bauer and Michael A. Schneider and Edward W. Felten and Andrew W. Appel},
  year = {2003},
  doi = {10.1109/DISCEX.2003.1194942},
  url = {http://doi.ieeecomputersociety.org/10.1109/DISCEX.2003.1194942},
  tags = {access control},
  researchr = {https://researchr.org/publication/BauerSFA03},
  cites = {0},
  citedby = {0},
  pages = {117-119},
  booktitle = {3rd DARPA Information Survivability Conference and Exposition (DISCEX-III 2003), 22-24 April 2003, Washington, DC, USA},
  publisher = {IEEE Computer Society},
  isbn = {0-7695-1897-4},
}

@inproceedings{ShaoA94,
  title = {Space-Efficient Closure Representations},
  author = {Zhong Shao and Andrew W. Appel},
  year = {1994},
  doi = {10.1145/182409.156783},
  url = {http://doi.acm.org/10.1145/182409.156783},
  researchr = {https://researchr.org/publication/ShaoA94},
  cites = {0},
  citedby = {0},
  pages = {150-161},
  booktitle = {LISP and Functional Programming},
}

@book{0034962,
  title = {Program Logics - for Certified Compilers},
  author = {Andrew W. Appel},
  year = {2014},
  url = {http://www.cambridge.org/de/academic/subjects/computer-science/programming-languages-and-applied-logic/program-logics-certified-compilers?format=HB},
  researchr = {https://researchr.org/publication/0034962},
  cites = {0},
  citedby = {0},
  publisher = {Cambridge University Press},
  isbn = {978-1-10-704801-0},
}

@inproceedings{Appel01,
  title = {Foundational Proof-Carrying Code},
  author = {Andrew W. Appel},
  year = {2001},
  researchr = {https://researchr.org/publication/Appel01},
  cites = {0},
  citedby = {0},
  pages = {247-256},
  booktitle = {LICS},
}

@inproceedings{Appel11-0,
  title = {VeriSmall: Verified Smallfoot Shape Analysis},
  author = {Andrew W. Appel},
  year = {2011},
  doi = {10.1007/978-3-642-25379-9_18},
  url = {http://dx.doi.org/10.1007/978-3-642-25379-9_18},
  researchr = {https://researchr.org/publication/Appel11-0},
  cites = {0},
  citedby = {0},
  pages = {231-246},
  booktitle = {Certified Programs and Proofs - First International Conference, CPP 2011, Kenting, Taiwan, December 7-9, 2011. Proceedings},
  editor = {Jean-Pierre Jouannaud and Zhong Shao},
  volume = {7086},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  isbn = {978-3-642-25378-2},
}

@article{AppelS87,
  title = {Generalization of the Sethi-Ullman Algorithm for Register Allocation},
  author = {Andrew W. Appel and Kenneth J. Supowit},
  year = {1987},
  researchr = {https://researchr.org/publication/AppelS87},
  cites = {0},
  citedby = {0},
  journal = {Software: Practice and Experience},
  volume = {17},
  number = {6},
  pages = {417-421},
}

@article{abs-0707-4389,
  title = {Separation Logic for Small-step Cminor},
  author = {Andrew W. Appel and Sandrine Blazy},
  year = {2007},
  url = {http://arxiv.org/abs/0707.4389},
  note = {informal publication},
  tags = {logic},
  researchr = {https://researchr.org/publication/abs-0707-4389},
  cites = {0},
  citedby = {0},
  journal = {CoRR},
  volume = {abs/0707.4389},
}

@inproceedings{AppelF00:0,
  title = {A Semantic Model of Types and Machine Instuctions for Proof-Carrying Code},
  author = {Andrew W. Appel and Amy P. Felty},
  year = {2000},
  doi = {10.1145/325694.325727},
  url = {http://doi.acm.org/10.1145/325694.325727},
  researchr = {https://researchr.org/publication/AppelF00%3A0},
  cites = {0},
  citedby = {0},
  pages = {243-253},
  booktitle = {POPL},
}

@article{ShaoA00,
  title = {Efficient and safe-for-space closure conversion},
  author = {Zhong Shao and Andrew W. Appel},
  year = {2000},
  doi = {10.1145/345099.345125},
  url = {http://doi.acm.org/10.1145/345099.345125},
  researchr = {https://researchr.org/publication/ShaoA00},
  cites = {0},
  citedby = {0},
  journal = {ACM Transactions on Programming Languages and Systems},
  volume = {22},
  number = {1},
  pages = {129-161},
}

@article{TolmachA95,
  title = {A Debugger for Standard ML},
  author = {Andrew P. Tolmach and Andrew W. Appel},
  year = {1995},
  tags = {debugging},
  researchr = {https://researchr.org/publication/TolmachA95},
  cites = {0},
  citedby = {0},
  journal = {Journal of Functional Programming},
  volume = {5},
  number = {2},
  pages = {155-200},
}

@article{BlumeA99,
  title = {Hierarchical modularity},
  author = {Matthias Blume and Andrew W. Appel},
  year = {1999},
  doi = {10.1145/325478.325518},
  url = {http://doi.acm.org/10.1145/325478.325518},
  researchr = {https://researchr.org/publication/BlumeA99},
  cites = {0},
  citedby = {0},
  journal = {ACM Transactions on Programming Languages and Systems},
  volume = {21},
  number = {4},
  pages = {813-847},
}

@inproceedings{BlazyRA10,
  title = {Formal Verification of Coalescing Graph-Coloring Register Allocation},
  author = {Sandrine Blazy and Benoît Robillard and Andrew W. Appel},
  year = {2010},
  doi = {10.1007/978-3-642-11957-6_9},
  url = {http://dx.doi.org/10.1007/978-3-642-11957-6_9},
  tags = {graph-rewriting, rewriting},
  researchr = {https://researchr.org/publication/BlazyRA10},
  cites = {0},
  citedby = {0},
  pages = {145-164},
  booktitle = {Programming Languages and Systems, 19th European Symposium on Programming, ESOP 2010, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2010, Paphos, Cyprus, March 20-28, 2010. Proceedings},
  editor = {Andrew D. Gordon},
  volume = {6012},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  isbn = {978-3-642-11956-9},
}

@book{Appel1997c,
  title = {Modern Compiler Implementation in C: Basic Techniques},
  author = {Andrew W. Appel},
  year = {1997},
  tags = {C++, compiler},
  researchr = {https://researchr.org/publication/Appel1997c},
  cites = {0},
  citedby = {0},
  publisher = {Cambridge University Press},
  isbn = {0-521-58653-4},
}

@inproceedings{AppelJ89,
  title = {Continuation-Passing, Closure-Passing Style},
  author = {Andrew W. Appel and Trevor Jim},
  year = {1989},
  researchr = {https://researchr.org/publication/AppelJ89},
  cites = {0},
  citedby = {0},
  pages = {293-302},
  booktitle = {POPL},
}

@inproceedings{WangAKS97,
  title = {The Zephyr Abstract Syntax Description Language},
  author = {Daniel C. Wang and Andrew W. Appel and Jeffrey L. Korn and Christopher S. Serra},
  year = {1997},
  url = {http://www.usenix.org/publications/library/proceedings/dsl97/wang.html},
  tags = {abstract syntax, C++, DSL},
  researchr = {https://researchr.org/publication/WangAKS97},
  cites = {0},
  citedby = {1},
  pages = {213-228},
  booktitle = {Proceedings of the Conference on Domain-Specific Languages, October 15-17, 1997, Santa Barbara, California, USA},
  publisher = {USENIX},
}

@inproceedings{YeGSBPA17,
  title = {Verified Correctness and Security of mbedTLS HMAC-DRBG},
  author = {Katherine Q. Ye and Matthew Green and Naphat Sanguansin and Lennart Beringer and Adam Petcher and Andrew W. Appel},
  year = {2017},
  doi = {10.1145/3133956.3133974},
  url = {http://doi.acm.org/10.1145/3133956.3133974},
  researchr = {https://researchr.org/publication/YeGSBPA17},
  cites = {0},
  citedby = {0},
  pages = {2007-2020},
  booktitle = {Proceedings of the 2017 ACM SIGSAC Conference on Computer and Communications Security, CCS 2017, Dallas, TX, USA, October 30 - November 03, 2017},
  editor = {Bhavani M. Thuraisingham and David Evans and Tal Malkin and Dongyan Xu},
  publisher = {ACM},
  isbn = {978-1-4503-4946-8},
}

@book{Appel1997,
  title = {Modern Compiler Implementation in Java: Basic Techniques},
  author = {Andrew W. Appel},
  year = {1997},
  tags = {Java, compiler},
  researchr = {https://researchr.org/publication/Appel1997},
  cites = {0},
  citedby = {0},
  publisher = {Cambridge University Press},
  isbn = {0-521-58654-2},
}

@inproceedings{Appel16,
  title = {Modular Verification for Computer Security},
  author = {Andrew W. Appel},
  year = {2016},
  doi = {10.1109/CSF.2016.8},
  url = {http://doi.ieeecomputersociety.org/10.1109/CSF.2016.8},
  researchr = {https://researchr.org/publication/Appel16},
  cites = {0},
  citedby = {0},
  pages = {1-8},
  booktitle = {IEEE 29th Computer Security Foundations Symposium, CSF 2016, Lisbon, Portugal, June 27 - July 1, 2016},
  publisher = {IEEE},
  isbn = {978-1-5090-2607-4},
}

@article{Appel93,
  title = {A Critique of Standard ML},
  author = {Andrew W. Appel},
  year = {1993},
  researchr = {https://researchr.org/publication/Appel93},
  cites = {0},
  citedby = {0},
  journal = {Journal of Functional Programming},
  volume = {3},
  number = {4},
  pages = {391-429},
}

@inproceedings{ShufGFAS02,
  title = {Creating and preserving locality of java applications at allocation and garbage collection times},
  author = {Yefim Shuf and Manish Gupta and Hubertus Franke and Andrew W. Appel and Jaswinder Pal Singh},
  year = {2002},
  doi = {10.1145/582419.582422},
  url = {http://doi.acm.org/10.1145/582419.582422},
  tags = {Java},
  researchr = {https://researchr.org/publication/ShufGFAS02},
  cites = {0},
  citedby = {0},
  pages = {13-25},
  booktitle = {OOPSLA},
}

@article{ManskyAN17,
  title = {A verified messaging system},
  author = {William Mansky and Andrew W. Appel and Aleksey Nogin},
  year = {2017},
  doi = {10.1145/3133911},
  url = {http://doi.acm.org/10.1145/3133911},
  researchr = {https://researchr.org/publication/ManskyAN17},
  cites = {0},
  citedby = {0},
  journal = {Proceedings of the ACM on Programming Languages},
  volume = {1},
  number = {OOPSLA},
}

@inproceedings{StewartBA12,
  title = {Verified heap theorem prover by paramodulation},
  author = {Gordon Stewart and Lennart Beringer and Andrew W. Appel},
  year = {2012},
  doi = {10.1145/2364527.2364531},
  url = {http://doi.acm.org/10.1145/2364527.2364531},
  researchr = {https://researchr.org/publication/StewartBA12},
  cites = {0},
  citedby = {0},
  pages = {3-14},
  booktitle = {ACM SIGPLAN International Conference on Functional Programming, ICFP'12, Copenhagen, Denmark, September 9-15, 2012},
  editor = {Peter Thiemann and Robby Bruce Findler},
  publisher = {ACM},
  isbn = {978-1-4503-1054-3},
}

@article{Appel88:0,
  title = {SSA is Functional Programming},
  author = {Andrew W. Appel},
  year = {1998},
  tags = {functional programming, programming},
  researchr = {https://researchr.org/publication/Appel88%3A0},
  cites = {0},
  citedby = {0},
  journal = {SIGPLAN Notices},
  volume = {33},
  number = {4},
  pages = {17-20},
}

@article{Appel88:1,
  title = {Simulating digital circuits with one bit per wire},
  author = {Andrew W. Appel},
  year = {1988},
  doi = {10.1109/43.7796},
  url = {http://doi.ieeecomputersociety.org/10.1109/43.7796},
  researchr = {https://researchr.org/publication/Appel88%3A1},
  cites = {0},
  citedby = {0},
  journal = {IEEE Trans. on CAD of Integrated Circuits and Systems},
  volume = {7},
  number = {9},
  pages = {987-993},
}

@inproceedings{AppelM91,
  title = {Standard ML of New Jersey},
  author = {Andrew W. Appel and David B. MacQueen},
  year = {1991},
  researchr = {https://researchr.org/publication/AppelM91},
  cites = {0},
  citedby = {0},
  pages = {1-13},
  booktitle = {PLILP},
}

@inproceedings{TanASW04,
  title = {Construction of a Semantic Model for a Typed Assembly Language},
  author = {Gang Tan and Andrew W. Appel and Kedar N. Swadi and Dinghao Wu},
  year = {2004},
  url = {http://springerlink.metapress.com/openurl.asp?genre=article&issn=0302-9743&volume=2937&spage=30},
  tags = {modeling language, modeling, language modeling},
  researchr = {https://researchr.org/publication/TanASW04},
  cites = {0},
  citedby = {0},
  pages = {30-43},
  booktitle = {Verification, Model Checking, and Abstract Interpretation, 5th International Conference, VMCAI 2004, Venice, January 11-13, 2004, Proceedings},
  editor = {Bernhard Steffen and Giorgio Levi},
  volume = {2937},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  isbn = {3-540-20803-8},
}

@article{Appel92,
  title = {Is POPL mathematics or science?},
  author = {Andrew W. Appel},
  year = {1992},
  doi = {10.1145/131080.131091},
  url = {http://doi.acm.org/10.1145/131080.131091},
  tags = {e-science},
  researchr = {https://researchr.org/publication/Appel92},
  cites = {0},
  citedby = {0},
  journal = {SIGPLAN Notices},
  volume = {27},
  number = {4},
  pages = {87-89},
}

@article{Appel89,
  title = {Runtime Tags Aren t Necessary},
  author = {Andrew W. Appel},
  year = {1989},
  tags = {tagging},
  researchr = {https://researchr.org/publication/Appel89},
  cites = {0},
  citedby = {0},
  journal = {Higher-Order and Symbolic Computation},
  volume = {2},
  number = {2},
  pages = {153-162},
}

@inproceedings{BelangerA17,
  title = {Shrink fast correctly!},
  author = {Olivier Savary Bélanger and Andrew W. Appel},
  year = {2017},
  doi = {10.1145/3131851.3131859},
  url = {http://doi.acm.org/10.1145/3131851.3131859},
  researchr = {https://researchr.org/publication/BelangerA17},
  cites = {0},
  citedby = {0},
  pages = {49-60},
  booktitle = {Proceedings of the 19th International Symposium on Principles and Practice of Declarative Programming, Namur, Belgium, October 09 - 11, 2017},
  editor = {Wim Vanhoof and Brigitte Pientka},
  publisher = {ACM},
  isbn = {978-1-4503-5291-8},
}

@inproceedings{DoddsA13,
  title = {Mostly Sound Type System Improves a Foundational Program Verifier},
  author = {Josiah Dodds and Andrew W. Appel},
  year = {2013},
  doi = {10.1007/978-3-319-03545-1_2},
  url = {http://dx.doi.org/10.1007/978-3-319-03545-1_2},
  researchr = {https://researchr.org/publication/DoddsA13},
  cites = {0},
  citedby = {0},
  pages = {17-32},
  booktitle = {Certified Programs and Proofs - Third International Conference, CPP 2013, Melbourne, VIC, Australia, December 11-13, 2013, Proceedings},
  editor = {Georges Gonthier and Michael Norrish},
  volume = {8307},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  isbn = {978-3-319-03544-4},
}

@book{Appel1992,
  title = {Compiling with Continuations},
  author = {Andrew W. Appel},
  year = {1992},
  tags = {compiler},
  researchr = {https://researchr.org/publication/Appel1992},
  cites = {0},
  citedby = {0},
  publisher = {Cambridge University Press},
  isbn = {0-521-41695-7},
}

@article{AppelJ97,
  title = {Shrinking lambda Expressions in Linear Time},
  author = {Andrew W. Appel and Trevor Jim},
  year = {1997},
  researchr = {https://researchr.org/publication/AppelJ97},
  cites = {0},
  citedby = {0},
  journal = {Journal of Functional Programming},
  volume = {7},
  number = {5},
  pages = {515-540},
}

@article{AppelS92,
  title = {Callee-Save Registers in Continuation-Passing Style},
  author = {Andrew W. Appel and Zhong Shao},
  year = {1992},
  researchr = {https://researchr.org/publication/AppelS92},
  cites = {0},
  citedby = {0},
  journal = {Higher-Order and Symbolic Computation},
  volume = {5},
  number = {3},
  pages = {191-221},
}

@inproceedings{KrollSA14,
  title = {Portable Software Fault Isolation},
  author = {Joshua A. Kroll and Gordon Stewart and Andrew W. Appel},
  year = {2014},
  doi = {10.1109/CSF.2014.10},
  url = {http://dx.doi.org/10.1109/CSF.2014.10},
  researchr = {https://researchr.org/publication/KrollSA14},
  cites = {0},
  citedby = {0},
  pages = {18-32},
  booktitle = {IEEE 27th Computer Security Foundations Symposium, CSF 2014, Vienna, Austria, 19-22 July, 2014},
  publisher = {IEEE},
}

@inproceedings{AppelF99,
  title = {Lightweight Lemmas in lambda-Prolog},
  author = {Andrew W. Appel and Amy P. Felty},
  year = {1999},
  tags = {Prolog},
  researchr = {https://researchr.org/publication/AppelF99},
  cites = {0},
  citedby = {0},
  pages = {411-425},
  booktitle = {ICLP},
}

@inproceedings{HoborDA10-0,
  title = {A Logical Mix of Approximation and Separation},
  author = {Aquinas Hobor and Robert Dockins and Andrew W. Appel},
  year = {2010},
  doi = {10.1007/978-3-642-17164-2_30},
  url = {http://dx.doi.org/10.1007/978-3-642-17164-2_30},
  researchr = {https://researchr.org/publication/HoborDA10-0},
  cites = {0},
  citedby = {0},
  pages = {439-454},
  booktitle = {Programming Languages and Systems - 8th Asian Symposium, APLAS 2010, Shanghai, China, November 28 - December 1, 2010. Proceedings},
  editor = {Kazunori Ueda},
  volume = {6461},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  isbn = {978-3-642-17163-5},
}

@article{AppelL07,
  title = {A List-machine Benchmark for Mechanized Metatheory: (Extended Abstract)},
  author = {Andrew W. Appel and Xavier Leroy},
  year = {2007},
  doi = {10.1016/j.entcs.2007.01.020},
  url = {http://dx.doi.org/10.1016/j.entcs.2007.01.020},
  tags = {metatheory, abstract machine},
  researchr = {https://researchr.org/publication/AppelL07},
  cites = {0},
  citedby = {0},
  journal = {Electronic Notes in Theoretical Computer Science},
  volume = {174},
  number = {5},
  pages = {95-108},
}

@article{AppelB89,
  title = {Vectorized garbage collection},
  author = {Andrew W. Appel and Aage Bendiksen},
  year = {1989},
  doi = {10.1007/BF00127826},
  url = {http://dx.doi.org/10.1007/BF00127826},
  researchr = {https://researchr.org/publication/AppelB89},
  cites = {0},
  citedby = {0},
  journal = {The Journal of Supercomputing},
  volume = {3},
  number = {3},
  pages = {151-160},
}

@inproceedings{AppelM94,
  title = {Separate Compilation for Standard ML},
  author = {Andrew W. Appel and David B. MacQueen},
  year = {1994},
  researchr = {https://researchr.org/publication/AppelM94},
  cites = {0},
  citedby = {0},
  pages = {13-23},
  booktitle = {PLDI},
}

@article{cs-LO-0403010,
  title = {Polymorphic lemmas and definitions in Lambda Prolog and Twelf},
  author = {Andrew W. Appel and Amy P. Felty},
  year = {2004},
  url = {http://arxiv.org/abs/cs.LO/0403010},
  note = {informal publication},
  tags = {Prolog},
  researchr = {https://researchr.org/publication/cs-LO-0403010},
  cites = {0},
  citedby = {0},
  journal = {CoRR},
  volume = {cs.LO/0403010},
}

@article{GeorgeA96:0,
  title = {Iterated Register Coalescing},
  author = {Lal George and Andrew W. Appel},
  year = {1996},
  doi = {10.1145/229542.229546},
  url = {http://doi.acm.org/10.1145/229542.229546},
  researchr = {https://researchr.org/publication/GeorgeA96%3A0},
  cites = {0},
  citedby = {0},
  journal = {ACM Transactions on Programming Languages and Systems},
  volume = {18},
  number = {3},
  pages = {300-324},
}

@inproceedings{WuAS03,
  title = {Foundational proof checkers with small witnesses},
  author = {Dinghao Wu and Andrew W. Appel and Aaron Stump},
  year = {2003},
  doi = {10.1145/888251.888276},
  url = {http://doi.acm.org/10.1145/888251.888276},
  researchr = {https://researchr.org/publication/WuAS03},
  cites = {0},
  citedby = {0},
  pages = {264-274},
  booktitle = {Proceedings of the 5th International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming, 27-29 August 2003, Uppsala, Sweden},
  publisher = {ACM},
  isbn = {1-58113-705-2},
}

@inproceedings{Appel12,
  title = {Verified Software Toolchain},
  author = {Andrew W. Appel},
  year = {2012},
  doi = {10.1007/978-3-642-28891-3_2},
  url = {http://dx.doi.org/10.1007/978-3-642-28891-3_2},
  researchr = {https://researchr.org/publication/Appel12},
  cites = {0},
  citedby = {0},
  pages = {2},
  booktitle = {NASA Formal Methods - 4th International Symposium, NFM 2012, Norfolk, VA, USA, April 3-5, 2012. Proceedings},
  editor = {Alwyn Goodloe and Suzette Person},
  volume = {7226},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  isbn = {978-3-642-28890-6},
}

@inproceedings{GovindavajhalaA03,
  title = {Using Memory Errors to Attack a Virtual Machine},
  author = {Sudhakar Govindavajhala and Andrew W. Appel},
  year = {2003},
  url = {http://csdl.computer.org/comp/proceedings/sp/2003/1940/00/19400154abs.htm},
  researchr = {https://researchr.org/publication/GovindavajhalaA03},
  cites = {0},
  citedby = {0},
  pages = {154-165},
  booktitle = {2003 IEEE Symposium on Security and Privacy (S&P 2003), 11-14 May 2003, Berkeley, CA, USA},
  publisher = {IEEE Computer Society},
  isbn = {0-7695-1940-7},
}

@inproceedings{OuGA05,
  title = {MulVAL: A Logic-based Network Security Analyzer},
  author = {Xinming Ou and Sudhakar Govindavajhala and Andrew W. Appel},
  year = {2005},
  url = {https://www.usenix.org/conference/14th-usenix-security-symposium/mulval-logic-based-network-security-analyzer},
  researchr = {https://researchr.org/publication/OuGA05},
  cites = {0},
  citedby = {0},
  booktitle = {Proceedings of the 14th USENIX Security Symposium, Baltimore, MD, USA, July 31 - August 5, 2005},
  editor = {Patrick McDaniel},
  publisher = {USENIX Association},
}

@inproceedings{ShaoA93,
  title = {Smartest Recompilation},
  author = {Zhong Shao and Andrew W. Appel},
  year = {1993},
  doi = {10.1145/158511.158702},
  researchr = {https://researchr.org/publication/ShaoA93},
  cites = {0},
  citedby = {0},
  pages = {439-450},
  booktitle = {Proceedings of the 20th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages},
}

@inproceedings{HoborAN08,
  title = {Oracle Semantics for Concurrent Separation Logic},
  author = {Aquinas Hobor and Andrew W. Appel and Francesco Zappa Nardelli},
  year = {2008},
  doi = {10.1007/978-3-540-78739-6_27},
  url = {http://dx.doi.org/10.1007/978-3-540-78739-6_27},
  tags = {semantics, logic},
  researchr = {https://researchr.org/publication/HoborAN08},
  cites = {0},
  citedby = {0},
  pages = {353-367},
  booktitle = {Programming Languages and Systems, 17th European Symposium on Programming, ESOP 2008, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2008, Budapest, Hungary, March 29-April 6, 2008. Proceedings},
  editor = {Sophia Drossopoulou},
  volume = {4960},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  isbn = {978-3-540-78738-9},
}

@inproceedings{GoncalvesA95,
  title = {Cache Performance of Fast-Allocating Programs},
  author = {Marcelo J. R. Gonçalves and Andrew W. Appel},
  year = {1995},
  tags = {caching},
  researchr = {https://researchr.org/publication/GoncalvesA95},
  cites = {0},
  citedby = {0},
  pages = {293-305},
  booktitle = {FPCA},
}

@inproceedings{Appel11,
  title = {Verified Software Toolchain - (Invited Talk)},
  author = {Andrew W. Appel},
  year = {2011},
  doi = {10.1007/978-3-642-19718-5_1},
  url = {http://dx.doi.org/10.1007/978-3-642-19718-5_1},
  researchr = {https://researchr.org/publication/Appel11},
  cites = {0},
  citedby = {0},
  pages = {1-17},
  booktitle = {Programming Languages and Systems - 20th European Symposium on Programming, ESOP 2011, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2011, Saarbrücken, Germany, March 26-April 3, 2011. Proceedings},
  editor = {Gilles Barthe},
  volume = {6602},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  isbn = {978-3-642-19717-8},
}

@inproceedings{MichaelA00,
  title = {Machine Instruction Syntax and Semantics in Higher Order Logic},
  author = {Neophytos G. Michael and Andrew W. Appel},
  year = {2000},
  tags = {semantics, logic},
  researchr = {https://researchr.org/publication/MichaelA00},
  cites = {0},
  citedby = {0},
  pages = {7-24},
  booktitle = {Automated Deduction - CADE-17, 17th International Conference on Automated Deduction, Pittsburgh, PA, USA, June 17-20, 2000, Proceedings},
  editor = {David A. McAllester},
  volume = {1831},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  isbn = {3-540-67664-3},
}

@inproceedings{CaoCA17,
  title = {Bringing Order to the Separation Logic Jungle},
  author = {Qinxiang Cao and Santiago Cuellar and Andrew W. Appel},
  year = {2017},
  doi = {10.1007/978-3-319-71237-6_10},
  url = {https://doi.org/10.1007/978-3-319-71237-6_10},
  researchr = {https://researchr.org/publication/CaoCA17},
  cites = {0},
  citedby = {0},
  pages = {190-211},
  booktitle = {Programming Languages and Systems - 15th Asian Symposium, APLAS 2017, Suzhou, China, November 27-29, 2017, Proceedings},
  editor = {Bor-Yuh Evan Chang},
  volume = {10695},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  isbn = {978-3-319-71237-6},
}

@inproceedings{AppelMRV07,
  title = {A very modal model of a modern, major, general type system},
  author = {Andrew W. Appel and Paul-André Melliès and Christopher D. Richards and Jérôme Vouillon},
  year = {2007},
  doi = {10.1145/1190216.1190235},
  url = {http://doi.acm.org/10.1145/1190216.1190235},
  tags = {type system},
  researchr = {https://researchr.org/publication/AppelMRV07},
  cites = {0},
  citedby = {0},
  pages = {109-122},
  booktitle = {Proceedings of the 34th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2007, Nice, France, January 17-19, 2007},
  editor = {Martin Hofmann and Matthias Felleisen},
  publisher = {ACM},
  isbn = {1-59593-575-4},
}

@article{Appel94,
  title = {Loop Headers in Lambda-Calculus or CPS},
  author = {Andrew W. Appel},
  year = {1994},
  researchr = {https://researchr.org/publication/Appel94},
  cites = {0},
  citedby = {0},
  journal = {Higher-Order and Symbolic Computation},
  volume = {7},
  number = {4},
  pages = {337-343},
}

@book{0022396,
  title = {Compiling with Continuations (corr. version)},
  author = {Andrew W. Appel},
  year = {2006},
  tags = {compiler},
  researchr = {https://researchr.org/publication/0022396},
  cites = {0},
  citedby = {0},
  publisher = {Cambridge University Press},
  isbn = {978-0-521-03311-4},
}

@article{CaoBGDA18,
  title = {VST-Floyd: A Separation Logic Tool to Verify Correctness of C Programs},
  author = {Qinxiang Cao and Lennart Beringer and Samuel Gruetter and Josiah Dodds and Andrew W. Appel},
  year = {2018},
  doi = {10.1007/s10817-018-9457-5},
  url = {https://doi.org/10.1007/s10817-018-9457-5},
  researchr = {https://researchr.org/publication/CaoBGDA18},
  cites = {0},
  citedby = {0},
  journal = {Journal of Automated Reasoning},
  volume = {61},
  number = {1-4},
  pages = {367-422},
}

@inproceedings{ShaoRA94,
  title = {Unrolling Lists},
  author = {Zhong Shao and John H. Reppy and Andrew W. Appel},
  year = {1994},
  doi = {10.1145/182409.182453},
  url = {http://doi.acm.org/10.1145/182409.182453},
  researchr = {https://researchr.org/publication/ShaoRA94},
  cites = {0},
  citedby = {0},
  pages = {185-195},
  booktitle = {LISP and Functional Programming},
}

@inproceedings{AppelM87,
  title = {A Standard ML compiler},
  author = {Andrew W. Appel and David B. MacQueen},
  year = {1987},
  tags = {compiler},
  researchr = {https://researchr.org/publication/AppelM87},
  cites = {0},
  citedby = {0},
  pages = {301-324},
  booktitle = {Functional Programming Languages and Computer Architecture, Portland, Oregon, USA, September 14-16, 1987, Proceedings},
  editor = {Gilles Kahn},
  volume = {274},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  isbn = {3-540-18317-5},
}

@inproceedings{AlonsoA90,
  title = {An Advisor for Flexible Working Sets},
  author = {Rafael Alonso and Andrew W. Appel},
  year = {1990},
  doi = {10.1145/98457.98753},
  url = {http://doi.acm.org/10.1145/98457.98753},
  researchr = {https://researchr.org/publication/AlonsoA90},
  cites = {0},
  citedby = {0},
  pages = {153-162},
  booktitle = {SIGMETRICS},
}

@inproceedings{Appel88,
  title = {Real-time concurrent collection on stock multiprocessors (with retrospective)},
  author = {Andrew W. Appel},
  year = {1988},
  doi = {10.1145/989393.989417},
  url = {http://doi.acm.org/10.1145/989393.989417},
  researchr = {https://researchr.org/publication/Appel88},
  cites = {0},
  citedby = {0},
  pages = {205-216},
  booktitle = {20 Years of the ACM SIGPLAN Conference on Programming Language Design and Implementation 1979-1999, A Selection},
  editor = {Kathryn S. McKinley},
  publisher = {ACM},
  isbn = {1-58113-623-4},
}

@inproceedings{Appel85,
  title = {Semantics-Directed Code Generation},
  author = {Andrew W. Appel},
  year = {1985},
  tags = {semantics, code generation},
  researchr = {https://researchr.org/publication/Appel85},
  cites = {0},
  citedby = {0},
  pages = {315-324},
  booktitle = {POPL},
}

@book{Appel1998c,
  title = {Modern Compiler Implementation in C},
  author = {Andrew W. Appel},
  year = {1998},
  tags = {C++, compiler},
  researchr = {https://researchr.org/publication/Appel1998c},
  cites = {0},
  citedby = {0},
  publisher = {Cambridge University Press},
  isbn = {0-521-58390-X},
}

@inproceedings{BlumeA97,
  title = {Lambda-Splitting: A Higher-Order Approach to Cross-Module Optimizations},
  author = {Matthias Blume and Andrew W. Appel},
  year = {1997},
  tags = {optimization, systematic-approach},
  researchr = {https://researchr.org/publication/BlumeA97},
  cites = {0},
  citedby = {0},
  pages = {112-124},
  booktitle = {ICFP},
}

@article{Appel89a,
  title = {Allocation without Locking},
  author = {Andrew W. Appel},
  year = {1989},
  researchr = {https://researchr.org/publication/Appel89a},
  cites = {0},
  citedby = {0},
  journal = {Software: Practice and Experience},
  volume = {19},
  number = {7},
  pages = {703-705},
}

@inproceedings{BellAW10,
  title = {Concurrent Separation Logic for Pipelined Parallelization},
  author = {Christian J. Bell and Andrew W. Appel and David Walker},
  year = {2010},
  doi = {10.1007/978-3-642-15769-1_10},
  url = {http://dx.doi.org/10.1007/978-3-642-15769-1_10},
  tags = {logic},
  researchr = {https://researchr.org/publication/BellAW10},
  cites = {0},
  citedby = {0},
  pages = {151-166},
  booktitle = {Static Analysis - 17th International Symposium, SAS 2010, Perpignan, France, September 14-16, 2010. Proceedings},
  editor = {Radhia Cousot and Matthieu Martel},
  volume = {6337},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  isbn = {978-3-642-15768-4},
}

@article{AppelDL12,
  title = {A List-Machine Benchmark for Mechanized Metatheory},
  author = {Andrew W. Appel and Robert Dockins and Xavier Leroy},
  year = {2012},
  doi = {10.1007/s10817-011-9226-1},
  url = {http://dx.doi.org/10.1007/s10817-011-9226-1},
  researchr = {https://researchr.org/publication/AppelDL12},
  cites = {0},
  citedby = {0},
  journal = {Journal of Automated Reasoning},
  volume = {49},
  number = {3},
  pages = {453-491},
}

@book{Appel2002,
  title = {Modern Compiler Implementation in Java, 2nd edition},
  author = {Andrew W. Appel},
  year = {2002},
  tags = {Java, compiler},
  researchr = {https://researchr.org/publication/Appel2002},
  cites = {0},
  citedby = {0},
  publisher = {Cambridge University Press},
  isbn = {0-521-82060-X},
}

@article{AppelF04,
  title = {Dependent types ensure partial correctness of theorem provers},
  author = {Andrew W. Appel and Amy P. Felty},
  year = {2004},
  doi = {10.1017/S0956796803004921},
  url = {http://dx.doi.org/10.1017/S0956796803004921},
  researchr = {https://researchr.org/publication/AppelF04},
  cites = {0},
  citedby = {0},
  journal = {Journal of Functional Programming},
  volume = {14},
  number = {1},
  pages = {3-19},
}

@article{Appel15,
  title = {Verification of a Cryptographic Primitive: SHA-256},
  author = {Andrew W. Appel},
  year = {2015},
  doi = {10.1145/2701415},
  url = {http://doi.acm.org/10.1145/2701415},
  researchr = {https://researchr.org/publication/Appel15},
  cites = {0},
  citedby = {0},
  journal = {ACM Transactions on Programming Languages and Systems},
  volume = {37},
  number = {2},
  pages = {7},
}

@article{Appel11-1,
  title = {Security Seals on Voting Machines: A Case Study},
  author = {Andrew W. Appel},
  year = {2011},
  doi = {10.1145/2019599.2019603},
  url = {http://doi.acm.org/10.1145/2019599.2019603},
  researchr = {https://researchr.org/publication/Appel11-1},
  cites = {0},
  citedby = {0},
  journal = {ACM Trans. Inf. Syst. Secur.},
  volume = {14},
  number = {2},
  pages = {18},
}

@inproceedings{Appel04,
  title = {Social processes and proofs of theorems and programs, revisited},
  author = {Andrew W. Appel},
  year = {2004},
  doi = {10.1145/996841.996842},
  url = {http://doi.acm.org/10.1145/996841.996842},
  tags = {social},
  researchr = {https://researchr.org/publication/Appel04},
  cites = {0},
  citedby = {0},
  pages = {170},
  booktitle = {Proceedings of the ACM SIGPLAN 2004 Conference on Programming Language Design and Implementation 2004, Washington, DC, USA, June 9-11, 2004},
  editor = {William Pugh and Craig Chambers},
  publisher = {ACM},
  isbn = {1-58113-807-5},
}

@article{AppelMSV03,
  title = {A Trustworthy Proof Checker},
  author = {Andrew W. Appel and Neophytos G. Michael and Aaron Stump and Roberto Virga},
  year = {2003},
  doi = {10.1023/B:JARS.0000021013.61329.58},
  url = {http://dx.doi.org/10.1023/B:JARS.0000021013.61329.58},
  researchr = {https://researchr.org/publication/AppelMSV03},
  cites = {0},
  citedby = {0},
  journal = {Journal of Automated Reasoning},
  volume = {31},
  number = {3-4},
  pages = {231-260},
}

@article{Appel90,
  title = {A Runtime System},
  author = {Andrew W. Appel},
  year = {1990},
  researchr = {https://researchr.org/publication/Appel90},
  cites = {0},
  citedby = {0},
  journal = {Higher-Order and Symbolic Computation},
  volume = {3},
  number = {4},
  pages = {343-380},
}

@article{Appel89:0,
  title = {Simple Generational Garbage Collection and Fast Allocation},
  author = {Andrew W. Appel},
  year = {1989},
  researchr = {https://researchr.org/publication/Appel89%3A0},
  cites = {0},
  citedby = {0},
  journal = {Software: Practice and Experience},
  volume = {19},
  number = {2},
  pages = {171-183},
}

@inproceedings{AppelF99:0,
  title = {Proof-Carrying Authentication},
  author = {Andrew W. Appel and Edward W. Felten},
  year = {1999},
  doi = {10.1145/319709.319718},
  url = {http://doi.acm.org/10.1145/319709.319718},
  researchr = {https://researchr.org/publication/AppelF99%3A0},
  cites = {0},
  citedby = {0},
  pages = {52-62},
  booktitle = {ACM Conference on Computer and Communications Security},
}

@article{AppelM01,
  title = {An indexed model of recursive types for foundational proof-carrying code},
  author = {Andrew W. Appel and David A. McAllester},
  year = {2001},
  doi = {10.1145/504709.504712},
  url = {http://doi.acm.org/10.1145/504709.504712},
  researchr = {https://researchr.org/publication/AppelM01},
  cites = {0},
  citedby = {0},
  journal = {ACM Transactions on Programming Languages and Systems},
  volume = {23},
  number = {5},
  pages = {657-683},
}

@inproceedings{TolmachA91,
  title = {Debuggable Concurrency Extensions for Standard ML},
  author = {Andrew P. Tolmach and Andrew W. Appel},
  year = {1991},
  tags = {debugging},
  researchr = {https://researchr.org/publication/TolmachA91},
  cites = {0},
  citedby = {0},
  pages = {120-131},
  booktitle = {Workshop on Parallel and Distributed Debugging},
}

@inproceedings{AhmedAV02,
  title = {A Stratified Semantics of General References A Stratified Semantics of General References},
  author = {Amal J. Ahmed and Andrew W. Appel and Roberto Virga},
  year = {2002},
  doi = {10.1109/LICS.2002.1029818},
  url = {http://doi.ieeecomputersociety.org/10.1109/LICS.2002.1029818},
  tags = {semantics},
  researchr = {https://researchr.org/publication/AhmedAV02},
  cites = {0},
  citedby = {0},
  pages = {75},
  booktitle = {17th IEEE Symposium on Logic in Computer Science (LICS 2002), 22-25 July 2002, Copenhagen, Denmark, Proceedings},
  publisher = {IEEE Computer Society},
  isbn = {0-7695-1483-9},
}

@article{DockinsAH08,
  title = {Multimodal Separation Logic for Reasoning About Operational Semantics},
  author = {Robert Dockins and Andrew W. Appel and Aquinas Hobor},
  year = {2008},
  doi = {10.1016/j.entcs.2008.10.002},
  url = {http://dx.doi.org/10.1016/j.entcs.2008.10.002},
  tags = {semantics, operational semantics, logic},
  researchr = {https://researchr.org/publication/DockinsAH08},
  cites = {0},
  citedby = {0},
  journal = {Electronic Notes in Theoretical Computer Science},
  volume = {218},
  pages = {5-20},
}

@inproceedings{AppelG01,
  title = {Optimal Spilling for CISC Machines with Few Registers},
  author = {Andrew W. Appel and Lal George},
  year = {2001},
  researchr = {https://researchr.org/publication/AppelG01},
  cites = {0},
  citedby = {0},
  pages = {243-253},
  booktitle = {PLDI},
}

@inproceedings{AppelGHKRTV09,
  title = {The New Jersey Voting-machine Lawsuit and the AVC Advantage DRE Voting Machine},
  author = {Andrew W. Appel and Maia Ginsburg and Harri Hursti and Brian W. Kernighan and Christopher D. Richards and Gang Tan and Penny Venetis},
  year = {2009},
  url = {https://www.usenix.org/conference/evtwote-09/new-jersey-voting-machine-lawsuit-and-avc-advantage-dre-voting-machine},
  researchr = {https://researchr.org/publication/AppelGHKRTV09},
  cites = {0},
  citedby = {0},
  booktitle = {2009 Electronic Voting Technology Workshop / Workshop on Trustworthy Elections, EVT/WOTE '09, Montreal, Canada, August 10-11, 2009},
  editor = {David Jefferson and Joseph Lorenzo Hall and Tal Moran},
  publisher = {USENIX Association},
}

@inproceedings{TanA06,
  title = {A Compositional Logic for Control Flow},
  author = {Gang Tan and Andrew W. Appel},
  year = {2006},
  doi = {10.1007/11609773_6},
  url = {http://dx.doi.org/10.1007/11609773_6},
  tags = {composition, data-flow, logic},
  researchr = {https://researchr.org/publication/TanA06},
  cites = {0},
  citedby = {0},
  pages = {80-94},
  booktitle = {Verification, Model Checking, and Abstract Interpretation, 7th International Conference, VMCAI 2006, Charleston, SC, USA, January 8-10, 2006, Proceedings},
  editor = {E. Allen Emerson and Kedar S. Namjoshi},
  volume = {3855},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  isbn = {3-540-31139-4},
}

@inproceedings{WangA01,
  title = {Type-preserving garbage collectors},
  author = {Daniel C. Wang and Andrew W. Appel},
  year = {2001},
  doi = {10.1145/360204.360218},
  url = {http://doi.acm.org/10.1145/360204.360218},
  tags = {C++},
  researchr = {https://researchr.org/publication/WangA01},
  cites = {0},
  citedby = {0},
  pages = {166-178},
  booktitle = {Proceedings of the 28th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages},
  series = {POPL},
  publisher = {Association for Computing Machinery},
}

@inproceedings{KornA98,
  title = {Traversal-Based Visualization of Data Structures},
  author = {Jeffrey L. Korn and Andrew W. Appel},
  year = {1998},
  url = {http://dlib.computer.org/conferen/infovis/9093/pdf/90930011.pdf},
  tags = {rule-based, traversal, data-flow},
  researchr = {https://researchr.org/publication/KornA98},
  cites = {0},
  citedby = {0},
  pages = {11-18},
  booktitle = {1998 IEEE Symposium on Information Visualization (InfoVis  98), 19-20 October 1998, Research Triangle Park, NC, USA, Proceedings},
  publisher = {IEEE Computer Society},
  isbn = {0-8186-9093-3},
}

@inproceedings{AppelB07,
  title = {Separation Logic for Small-Step cminor},
  author = {Andrew W. Appel and Sandrine Blazy},
  year = {2007},
  doi = {10.1007/978-3-540-74591-4_3},
  url = {http://dx.doi.org/10.1007/978-3-540-74591-4_3},
  tags = {logic},
  researchr = {https://researchr.org/publication/AppelB07},
  cites = {0},
  citedby = {0},
  pages = {5-21},
  booktitle = {Theorem Proving in Higher Order Logics, 20th International Conference, TPHOLs 2007, Kaiserslautern, Germany, September 10-13, 2007, Proceedings},
  editor = {Klaus Schneider and Jens Brandt},
  volume = {4732},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  isbn = {978-3-540-74590-7},
}

@article{Appel96,
  title = {Intensional Equality ;=) for Continuations},
  author = {Andrew W. Appel},
  year = {1996},
  researchr = {https://researchr.org/publication/Appel96},
  cites = {0},
  citedby = {0},
  journal = {SIGPLAN Notices},
  volume = {31},
  number = {2},
  pages = {55-57},
}

@inproceedings{StewartA11,
  title = {Local actions for a curry-style operational semantics},
  author = {Gordon Stewart and Andrew W. Appel},
  year = {2011},
  doi = {10.1145/1929529.1929535},
  url = {http://doi.acm.org/10.1145/1929529.1929535},
  tags = {semantics,  action semantics, operational semantics},
  researchr = {https://researchr.org/publication/StewartA11},
  cites = {0},
  citedby = {0},
  pages = {31-42},
  booktitle = {Proceedings of the 5th ACM Workshop Programming Languages meets Program Verification, PLPV 2011, Austin, TX, USA, January 29, 2011},
  editor = {Ranjit Jhala and Wouter Swierstra},
  publisher = {ACM},
  isbn = {978-1-4503-0487-0},
}

@inproceedings{HoborDA10,
  title = {A theory of indirection via approximation},
  author = {Aquinas Hobor and Robert Dockins and Andrew W. Appel},
  year = {2010},
  doi = {10.1145/1706299.1706322},
  url = {http://doi.acm.org/10.1145/1706299.1706322},
  researchr = {https://researchr.org/publication/HoborDA10},
  cites = {0},
  citedby = {0},
  pages = {171-184},
  booktitle = {Proceedings of the 37th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2010, Madrid, Spain, January 17-23, 2010},
  editor = {Manuel V. Hermenegildo and Jens Palsberg},
  publisher = {ACM},
  isbn = {978-1-60558-479-9},
}

@article{AppelF00,
  title = {Technological access control interferes with noninfringing scholarship},
  author = {Andrew W. Appel and Edward W. Felten},
  year = {2000},
  doi = {10.1145/348941.348968},
  url = {http://doi.acm.org/10.1145/348941.348968},
  tags = {access control},
  researchr = {https://researchr.org/publication/AppelF00},
  cites = {0},
  citedby = {0},
  journal = {Communications of the ACM},
  volume = {43},
  number = {9},
  pages = {21-23},
}

@article{AhmedARSTW10,
  title = {Semantic foundations for typed assembly languages},
  author = {Amal Ahmed and Andrew W. Appel and Christopher D. Richards and Kedar N. Swadi and Gang Tan and Daniel C. Wang},
  year = {2010},
  doi = {10.1145/1709093.1709094},
  url = {http://doi.acm.org/10.1145/1709093.1709094},
  tags = {C++},
  researchr = {https://researchr.org/publication/AhmedARSTW10},
  cites = {0},
  citedby = {0},
  journal = {ACM Transactions on Programming Languages and Systems},
  volume = {32},
  number = {3},
}

@inproceedings{GeorgeA96,
  title = {Iterated Register Coalescing},
  author = {Lal George and Andrew W. Appel},
  year = {1996},
  doi = {10.1145/237721.237777},
  url = {http://doi.acm.org/10.1145/237721.237777},
  researchr = {https://researchr.org/publication/GeorgeA96},
  cites = {0},
  citedby = {0},
  pages = {208-218},
  booktitle = {POPL},
}

@article{Appel87,
  title = {Garbage Collection can be Faster than Stack Allocation},
  author = {Andrew W. Appel},
  year = {1987},
  researchr = {https://researchr.org/publication/Appel87},
  cites = {0},
  citedby = {0},
  journal = {Inf. Process. Lett.},
  volume = {25},
  number = {4},
  pages = {275-279},
}

@inproceedings{AppelEL88,
  title = {Real-Time Concurrent Collection on Stock Multiprocessors},
  author = {Andrew W. Appel and John R. Ellis and Kai Li},
  year = {1988},
  researchr = {https://researchr.org/publication/AppelEL88},
  cites = {0},
  citedby = {0},
  pages = {11-20},
  booktitle = {PLDI},
}

@inproceedings{LeeA03,
  title = {Policy-enforced linking of untrusted components},
  author = {Eunyoung Lee and Andrew W. Appel},
  year = {2003},
  doi = {10.1145/940071.940124},
  url = {http://doi.acm.org/10.1145/940071.940124},
  researchr = {https://researchr.org/publication/LeeA03},
  cites = {0},
  citedby = {0},
  pages = {371-374},
  booktitle = {Proceedings of the 11th ACM SIGSOFT Symposium on Foundations of Software Engineering 2003 held jointly with 9th European Software Engineering Conference, ESEC/FSE 2003, Helsinki, Finland, September 1-5, 2003},
  publisher = {ACM},
}

@article{AppelJ88,
  title = {The World s Fastest Scrabble Program},
  author = {Andrew W. Appel and Guy J. Jacobson},
  year = {1988},
  researchr = {https://researchr.org/publication/AppelJ88},
  cites = {0},
  citedby = {0},
  journal = {Communications of the ACM},
  volume = {31},
  number = {5},
  pages = {572-578},
}
@proceedings{popl-1999,
  title = {POPL '99, Proceedings of the 26th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, San Antonio, TX, USA, January 20-22, 1999},
  year = {1999},
  url = {http://dl.acm.org/citation.cfm?id=292540},
  researchr = {https://researchr.org/publication/popl-1999},
  cites = {0},
  citedby = {0},
  booktitle = {POPL '99, Proceedings of the 26th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, San Antonio, TX, USA, January 20-22, 1999},
  conference = {POPL},
  editor = {Andrew W. Appel and Alex Aiken},
  publisher = {ACM},
  isbn = {1-58113-095-3},
}