publications:
- title: "Mechanisms for secure modular programming in Java"
  author:
  - name: "Lujo Bauer"
    link: "https://researchr.org/alias/lujo-bauer"
  - name: "Andrew W. Appel"
    link: "http://www.cs.princeton.edu/~appel/"
  - name: "Edward W. Felten"
    link: "https://researchr.org/alias/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"
  kind: "article"
  key: "BauerAF03"
- title: "Modern Compiler Implementation in ML"
  author:
  - name: "Andrew W. Appel"
    link: "http://www.cs.princeton.edu/~appel/"
  year: "1998"
  tags:
  - "compiler"
  researchr: "https://researchr.org/publication/Appel1998ml"
  cites: 0
  citedby: 0
  publisher: "Cambridge University Press"
  isbn: "0-521-58274-1"
  kind: "book"
  key: "Appel1998ml"
- title: "Compositional CompCert"
  author:
  - name: "Gordon Stewart"
    link: "https://researchr.org/alias/gordon-stewart"
  - name: "Lennart Beringer"
    link: "https://researchr.org/alias/lennart-beringer"
  - name: "Santiago Cuellar"
    link: "https://researchr.org/alias/santiago-cuellar"
  - name: "Andrew W. Appel"
    link: "http://www.cs.princeton.edu/~appel/"
  year: "2015"
  doi: "http://doi.acm.org/10.1145/2676726.2676985"
  links:
    doi: "http://doi.acm.org/10.1145/2676726.2676985"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/popl/StewartBCA15"
  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:
  - name: "Sriram K. Rajamani"
    link: "https://researchr.org/alias/sriram-k.-rajamani"
  - name: "David Walker"
    link: "https://researchr.org/alias/david-walker"
  publisher: "ACM"
  isbn: "978-1-4503-3300-9"
  kind: "inproceedings"
  key: "StewartBCA15"
- title: "Debugging Standard ML Without Reverse Engineering"
  author:
  - name: "Andrew P. Tolmach"
    link: "http://www.cs.pdx.edu/~apt"
  - name: "Andrew W. Appel"
    link: "http://www.cs.princeton.edu/~appel/"
  year: "1990"
  doi: "http://doi.acm.org/10.1145/91556.91564"
  links:
    doi: "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"
  kind: "inproceedings"
  key: "TolmachA90"
- title: "Verified Compilation for Shared-Memory C"
  author:
  - name: "Lennart Beringer"
    link: "https://researchr.org/alias/lennart-beringer"
  - name: "Gordon Stewart"
    link: "https://researchr.org/alias/gordon-stewart"
  - name: "Robert Dockins"
    link: "https://researchr.org/alias/robert-dockins"
  - name: "Andrew W. Appel"
    link: "http://www.cs.princeton.edu/~appel/"
  year: "2014"
  doi: "http://dx.doi.org/10.1007/978-3-642-54833-8_7"
  links:
    doi: "http://dx.doi.org/10.1007/978-3-642-54833-8_7"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/esop/BeringerSDA14"
  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:
  - name: "Zhong Shao"
    link: "https://researchr.org/alias/zhong-shao"
  volume: "8410"
  series: "Lecture Notes in Computer Science"
  publisher: "Springer"
  isbn: "978-3-642-54832-1"
  kind: "inproceedings"
  key: "BeringerSDA14"
- title: "Modern Compiler Implementation in ML: Basic Techniques"
  author:
  - name: "Andrew W. Appel"
    link: "http://www.cs.princeton.edu/~appel/"
  year: "1997"
  tags:
  - "compiler"
  researchr: "https://researchr.org/publication/Appel1997ml"
  cites: 0
  citedby: 0
  publisher: "Cambridge University Press"
  isbn: "0-521-58775-1"
  kind: "book"
  key: "Appel1997ml"
- title: "A Certificate Infrastructure for Machine-Checked Proofs of Conditional Information Flow"
  author:
  - name: "Torben Amtoft"
    link: "https://researchr.org/alias/torben-amtoft"
  - name: "Josiah Dodds"
    link: "https://researchr.org/alias/josiah-dodds"
  - name: "Zhi Zhang"
    link: "https://researchr.org/alias/zhi-zhang"
  - name: "Andrew W. Appel"
    link: "http://www.cs.princeton.edu/~appel/"
  - name: "Lennart Beringer"
    link: "https://researchr.org/alias/lennart-beringer"
  - name: "John Hatcliff"
    link: "https://researchr.org/alias/john-hatcliff"
  - name: "Xinming Ou"
    link: "https://researchr.org/alias/xinming-ou"
  - name: "Andrew Cousino"
    link: "https://researchr.org/alias/andrew-cousino"
  year: "2012"
  doi: "http://dx.doi.org/10.1007/978-3-642-28641-4_20"
  links:
    doi: "http://dx.doi.org/10.1007/978-3-642-28641-4_20"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/post/AmtoftDZABHOC12"
  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:
  - name: "Pierpaolo Degano"
    link: "https://researchr.org/alias/pierpaolo-degano"
  - name: "Joshua D. Guttman"
    link: "https://researchr.org/alias/joshua-d.-guttman"
  volume: "7215"
  series: "Lecture Notes in Computer Science"
  publisher: "Springer"
  isbn: "978-3-642-28640-7"
  kind: "inproceedings"
  key: "AmtoftDZABHOC12"
- title: "A Fresh Look at Separation Algebras and Share Accounting"
  author:
  - name: "Robert Dockins"
    link: "https://researchr.org/alias/robert-dockins"
  - name: "Aquinas Hobor"
    link: "https://researchr.org/alias/aquinas-hobor"
  - name: "Andrew W. Appel"
    link: "http://www.cs.princeton.edu/~appel/"
  year: "2009"
  doi: "http://springerlink.metapress.com/content/rp5547377166x21j/"
  links:
    doi: "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:
  - name: "Zhenjiang Hu"
    link: "http://research.nii.ac.jp/~hu/"
  volume: "5904"
  series: "Lecture Notes in Computer Science"
  publisher: "Springer"
  isbn: "978-3-642-10671-2"
  kind: "inproceedings"
  key: "DockinsHA09"
- title: "Empirical and Analytic Study of Stack Versus Heap Cost for Languages with Closures"
  author:
  - name: "Andrew W. Appel"
    link: "http://www.cs.princeton.edu/~appel/"
  - name: "Zhong Shao"
    link: "https://researchr.org/alias/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"
  kind: "article"
  key: "AppelS96"
- title: "Verified Correctness and Security of OpenSSL HMAC"
  author:
  - name: "Lennart Beringer"
    link: "https://researchr.org/alias/lennart-beringer"
  - name: "Adam Petcher"
    link: "https://researchr.org/alias/adam-petcher"
  - name: "Katherine Q. Ye"
    link: "https://researchr.org/alias/katherine-q.-ye"
  - name: "Andrew W. Appel"
    link: "http://www.cs.princeton.edu/~appel/"
  year: "2015"
  doi: "https://www.usenix.org/conference/usenixsecurity15/technical-sessions/presentation/beringer"
  links:
    doi: "https://www.usenix.org/conference/usenixsecurity15/technical-sessions/presentation/beringer"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/uss/BeringerPYA15"
  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:
  - name: "Jaeyeon Jung"
    link: "https://researchr.org/alias/jaeyeon-jung"
  - name: "Thorsten Holz"
    link: "https://researchr.org/alias/thorsten-holz"
  publisher: "USENIX Association"
  kind: "inproceedings"
  key: "BeringerPYA15"
- title: "A provably sound TAL for back-end optimization"
  author:
  - name: "Juan Chen"
    link: "https://researchr.org/alias/juan-chen"
  - name: "Dinghao Wu"
    link: "https://researchr.org/alias/dinghao-wu"
  - name: "Andrew W. Appel"
    link: "http://www.cs.princeton.edu/~appel/"
  - name: "Hai Fang"
    link: "https://researchr.org/alias/hai-fang"
  year: "2003"
  doi: "http://doi.acm.org/10.1145/781131.781155"
  links:
    doi: "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"
  kind: "inproceedings"
  key: "ChenWAF03"
- title: "Polymorphic Lemmas and Definitions in lambda-Prolog and Twelf"
  author:
  - name: "Andrew W. Appel"
    link: "http://www.cs.princeton.edu/~appel/"
  - name: "Amy P. Felty"
    link: "https://researchr.org/alias/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"
  kind: "article"
  key: "AppelF04:0"
- title: "Virtual Memory Primitives for User Programs"
  author:
  - name: "Andrew W. Appel"
    link: "http://www.cs.princeton.edu/~appel/"
  - name: "Kai Li"
    link: "https://researchr.org/alias/kai-li"
  year: "1991"
  researchr: "https://researchr.org/publication/AppelL91"
  cites: 0
  citedby: 0
  pages: "96-107"
  booktitle: "ASPLOS"
  kind: "inproceedings"
  key: "AppelL91"
- title: "Modern Compiler Implementation in Java"
  author:
  - name: "Andrew W. Appel"
    link: "http://www.cs.princeton.edu/~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"
  kind: "book"
  key: "Appel1998"
- title: "Verification of a cryptographic primitive: SHA-256 (abstract)"
  author:
  - name: "Andrew W. Appel"
    link: "http://www.cs.princeton.edu/~appel/"
  year: "2015"
  doi: "http://doi.acm.org/10.1145/2737924.2774972"
  links:
    doi: "http://doi.acm.org/10.1145/2737924.2774972"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/pldi/Appel15"
  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:
  - name: "David Grove"
    link: "https://researchr.org/alias/david-grove"
  - name: "Steve Blackburn"
    link: "https://researchr.org/alias/steve-blackburn"
  publisher: "ACM"
  isbn: "978-1-4503-3468-6"
  kind: "inproceedings"
  key: "Appel15-0"
- title: "A Type-Based Compiler for Standard ML"
  author:
  - name: "Zhong Shao"
    link: "https://researchr.org/alias/zhong-shao"
  - name: "Andrew W. Appel"
    link: "http://www.cs.princeton.edu/~appel/"
  year: "1995"
  tags:
  - "rule-based"
  - "compiler"
  researchr: "https://researchr.org/publication/ShaoA95"
  cites: 0
  citedby: 0
  pages: "116-129"
  booktitle: "PLDI"
  kind: "inproceedings"
  key: "ShaoA95"
- title: "SAFKASI: a security mechanism for language-based systems"
  author:
  - name: "Dan S. Wallach"
    link: "https://researchr.org/alias/dan-s.-wallach"
  - name: "Andrew W. Appel"
    link: "http://www.cs.princeton.edu/~appel/"
  - name: "Edward W. Felten"
    link: "https://researchr.org/alias/edward-w.-felten"
  year: "2000"
  doi: "http://doi.acm.org/10.1145/363516.363520"
  links:
    doi: "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"
  kind: "article"
  key: "WallachAF00"
- title: "Axiomatic Bootstrapping: A Guide for Compiler Hackers"
  author:
  - name: "Andrew W. Appel"
    link: "http://www.cs.princeton.edu/~appel/"
  year: "1994"
  doi: "http://doi.acm.org/10.1145/197320.197336"
  links:
    doi: "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"
  kind: "article"
  key: "Appel94:0"
- title: "Access Control on the Web Using Proof-carrying Authorization"
  author:
  - name: "Lujo Bauer"
    link: "https://researchr.org/alias/lujo-bauer"
  - name: "Michael A. Schneider"
    link: "https://researchr.org/alias/michael-a.-schneider"
  - name: "Edward W. Felten"
    link: "https://researchr.org/alias/edward-w.-felten"
  - name: "Andrew W. Appel"
    link: "http://www.cs.princeton.edu/~appel/"
  year: "2003"
  doi: "http://doi.ieeecomputersociety.org/10.1109/DISCEX.2003.1194942"
  links:
    doi: "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"
  kind: "inproceedings"
  key: "BauerSFA03"
- title: "Space-Efficient Closure Representations"
  author:
  - name: "Zhong Shao"
    link: "https://researchr.org/alias/zhong-shao"
  - name: "Andrew W. Appel"
    link: "http://www.cs.princeton.edu/~appel/"
  year: "1994"
  doi: "http://doi.acm.org/10.1145/182409.156783"
  links:
    doi: "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"
  kind: "inproceedings"
  key: "ShaoA94"
- title: "Program Logics - for Certified Compilers"
  author:
  - name: "Andrew W. Appel"
    link: "http://www.cs.princeton.edu/~appel/"
  year: "2014"
  doi: "http://www.cambridge.org/de/academic/subjects/computer-science/programming-languages-and-applied-logic/program-logics-certified-compilers?format=HB"
  links:
    doi: "http://www.cambridge.org/de/academic/subjects/computer-science/programming-languages-and-applied-logic/program-logics-certified-compilers?format=HB"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/books/daglib/0034962"
  researchr: "https://researchr.org/publication/0034962"
  cites: 0
  citedby: 0
  publisher: "Cambridge University Press"
  isbn: "978-1-10-704801-0"
  kind: "book"
  key: "0034962"
- title: "Foundational Proof-Carrying Code"
  author:
  - name: "Andrew W. Appel"
    link: "http://www.cs.princeton.edu/~appel/"
  year: "2001"
  researchr: "https://researchr.org/publication/Appel01"
  cites: 0
  citedby: 0
  pages: "247-256"
  booktitle: "LICS"
  kind: "inproceedings"
  key: "Appel01"
- title: "VeriSmall: Verified Smallfoot Shape Analysis"
  author:
  - name: "Andrew W. Appel"
    link: "http://www.cs.princeton.edu/~appel/"
  year: "2011"
  doi: "http://dx.doi.org/10.1007/978-3-642-25379-9_18"
  links:
    doi: "http://dx.doi.org/10.1007/978-3-642-25379-9_18"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/cpp/Appel11"
  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:
  - name: "Jean-Pierre Jouannaud"
    link: "https://researchr.org/alias/jean-pierre-jouannaud"
  - name: "Zhong Shao"
    link: "https://researchr.org/alias/zhong-shao"
  volume: "7086"
  series: "Lecture Notes in Computer Science"
  publisher: "Springer"
  isbn: "978-3-642-25378-2"
  kind: "inproceedings"
  key: "Appel11-0"
- title: "Generalization of the Sethi-Ullman Algorithm for Register Allocation"
  author:
  - name: "Andrew W. Appel"
    link: "http://www.cs.princeton.edu/~appel/"
  - name: "Kenneth J. Supowit"
    link: "https://researchr.org/alias/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"
  kind: "article"
  key: "AppelS87"
- title: "Separation Logic for Small-step Cminor"
  author:
  - name: "Andrew W. Appel"
    link: "http://www.cs.princeton.edu/~appel/"
  - name: "Sandrine Blazy"
    link: "https://researchr.org/alias/sandrine-blazy"
  year: "2007"
  doi: "http://arxiv.org/abs/0707.4389"
  note: "informal publication"
  links:
    doi: "http://arxiv.org/abs/0707.4389"
  tags:
  - "logic"
  researchr: "https://researchr.org/publication/abs-0707-4389"
  cites: 0
  citedby: 0
  journal: "CoRR"
  volume: "abs/0707.4389"
  kind: "article"
  key: "abs-0707-4389"
- title: "A Semantic Model of Types and Machine Instuctions for Proof-Carrying Code"
  author:
  - name: "Andrew W. Appel"
    link: "http://www.cs.princeton.edu/~appel/"
  - name: "Amy P. Felty"
    link: "https://researchr.org/alias/amy-p.-felty"
  year: "2000"
  doi: "http://doi.acm.org/10.1145/325694.325727"
  links:
    doi: "http://doi.acm.org/10.1145/325694.325727"
  researchr: "https://researchr.org/publication/AppelF00%3A0"
  cites: 0
  citedby: 0
  pages: "243-253"
  booktitle: "POPL"
  kind: "inproceedings"
  key: "AppelF00:0"
- title: "Efficient and safe-for-space closure conversion"
  author:
  - name: "Zhong Shao"
    link: "https://researchr.org/alias/zhong-shao"
  - name: "Andrew W. Appel"
    link: "http://www.cs.princeton.edu/~appel/"
  year: "2000"
  doi: "http://doi.acm.org/10.1145/345099.345125"
  links:
    doi: "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"
  kind: "article"
  key: "ShaoA00"
- title: "A Debugger for Standard ML"
  author:
  - name: "Andrew P. Tolmach"
    link: "http://www.cs.pdx.edu/~apt"
  - name: "Andrew W. Appel"
    link: "http://www.cs.princeton.edu/~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"
  kind: "article"
  key: "TolmachA95"
- title: "Hierarchical modularity"
  author:
  - name: "Matthias Blume"
    link: "https://researchr.org/alias/matthias-blume"
  - name: "Andrew W. Appel"
    link: "http://www.cs.princeton.edu/~appel/"
  year: "1999"
  doi: "http://doi.acm.org/10.1145/325478.325518"
  abstract: "To cope with the complexity of very large systems, it is not sufficient to divide them into simple pieces because the pieces themselves will either be too numerous or too large. A hierarchical modular structure is the natural solution. In this article we explain how that approach can be applied to software. Our compilation manager provides a language for specifying where individual modules fit into a hierarchy and how they are related semantically. We pay particular attention to the structure of the global name space of program identifiers that are used for module linkage because any potential for name clashes between otherwise unrelated parts of a program can negatively affect modularity. We discuss the theoretical issues in building software hierarchically, and we describe our implementation of CM, the compilation manager for Standard ML of New Jersey."
  links:
    doi: "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"
  kind: "article"
  key: "BlumeA99"
- title: "Formal Verification of Coalescing Graph-Coloring Register Allocation"
  author:
  - name: "Sandrine Blazy"
    link: "https://researchr.org/alias/sandrine-blazy"
  - name: "Benoît Robillard"
    link: "https://researchr.org/alias/beno%C3%A3%C2%AEt-robillard"
  - name: "Andrew W. Appel"
    link: "http://www.cs.princeton.edu/~appel/"
  year: "2010"
  doi: "http://dx.doi.org/10.1007/978-3-642-11957-6_9"
  links:
    doi: "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:
  - name: "Andrew D. Gordon"
    link: "http://research.microsoft.com/en-us/um/people/adg/"
  volume: "6012"
  series: "Lecture Notes in Computer Science"
  publisher: "Springer"
  isbn: "978-3-642-11956-9"
  kind: "inproceedings"
  key: "BlazyRA10"
- title: "Modern Compiler Implementation in C: Basic Techniques"
  author:
  - name: "Andrew W. Appel"
    link: "http://www.cs.princeton.edu/~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"
  kind: "book"
  key: "Appel1997c"
- title: "Continuation-Passing, Closure-Passing Style"
  author:
  - name: "Andrew W. Appel"
    link: "http://www.cs.princeton.edu/~appel/"
  - name: "Trevor Jim"
    link: "https://researchr.org/alias/trevor-jim"
  year: "1989"
  researchr: "https://researchr.org/publication/AppelJ89"
  cites: 0
  citedby: 0
  pages: "293-302"
  booktitle: "POPL"
  kind: "inproceedings"
  key: "AppelJ89"
- title: "The Zephyr Abstract Syntax Description Language"
  author:
  - name: "Daniel C. Wang"
    link: "https://researchr.org/alias/daniel-c.-wang"
  - name: "Andrew W. Appel"
    link: "http://www.cs.princeton.edu/~appel/"
  - name: "Jeffrey L. Korn"
    link: "https://researchr.org/alias/jeffrey-l.-korn"
  - name: "Christopher S. Serra"
    link: "https://researchr.org/alias/christopher-s.-serra"
  year: "1997"
  doi: "http://www.usenix.org/publications/library/proceedings/dsl97/wang.html"
  links:
    doi: "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"
  kind: "inproceedings"
  key: "WangAKS97"
- title: "Verified Correctness and Security of mbedTLS HMAC-DRBG"
  author:
  - name: "Katherine Q. Ye"
    link: "https://researchr.org/alias/katherine-q.-ye"
  - name: "Matthew Green"
    link: "https://researchr.org/alias/matthew-green"
  - name: "Naphat Sanguansin"
    link: "https://researchr.org/alias/naphat-sanguansin"
  - name: "Lennart Beringer"
    link: "https://researchr.org/alias/lennart-beringer"
  - name: "Adam Petcher"
    link: "https://researchr.org/alias/adam-petcher"
  - name: "Andrew W. Appel"
    link: "http://www.cs.princeton.edu/~appel/"
  year: "2017"
  doi: "http://doi.acm.org/10.1145/3133956.3133974"
  links:
    doi: "http://doi.acm.org/10.1145/3133956.3133974"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/ccs/YeGSBPA17"
  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:
  - name: "Bhavani M. Thuraisingham"
    link: "https://researchr.org/alias/bhavani-m.-thuraisingham"
  - name: "David Evans"
    link: "https://researchr.org/alias/david-evans"
  - name: "Tal Malkin"
    link: "https://researchr.org/alias/tal-malkin"
  - name: "Dongyan Xu"
    link: "https://researchr.org/alias/dongyan-xu"
  publisher: "ACM"
  isbn: "978-1-4503-4946-8"
  kind: "inproceedings"
  key: "YeGSBPA17"
- title: "Modern Compiler Implementation in Java: Basic Techniques"
  author:
  - name: "Andrew W. Appel"
    link: "http://www.cs.princeton.edu/~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"
  kind: "book"
  key: "Appel1997"
- title: "Modular Verification for Computer Security"
  author:
  - name: "Andrew W. Appel"
    link: "http://www.cs.princeton.edu/~appel/"
  year: "2016"
  doi: "http://doi.ieeecomputersociety.org/10.1109/CSF.2016.8"
  links:
    doi: "http://doi.ieeecomputersociety.org/10.1109/CSF.2016.8"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/csfw/Appel16"
  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"
  kind: "inproceedings"
  key: "Appel16"
- title: "A Critique of Standard ML"
  author:
  - name: "Andrew W. Appel"
    link: "http://www.cs.princeton.edu/~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"
  kind: "article"
  key: "Appel93"
- title: "Creating and preserving locality of java applications at allocation and garbage collection times"
  author:
  - name: "Yefim Shuf"
    link: "https://researchr.org/alias/yefim-shuf"
  - name: "Manish Gupta"
    link: "https://researchr.org/alias/manish-gupta"
  - name: "Hubertus Franke"
    link: "https://researchr.org/alias/hubertus-franke"
  - name: "Andrew W. Appel"
    link: "http://www.cs.princeton.edu/~appel/"
  - name: "Jaswinder Pal Singh"
    link: "https://researchr.org/alias/jaswinder-pal-singh"
  year: "2002"
  doi: "http://doi.acm.org/10.1145/582419.582422"
  links:
    doi: "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"
  kind: "inproceedings"
  key: "ShufGFAS02"
- title: "A verified messaging system"
  author:
  - name: "William Mansky"
    link: "https://researchr.org/alias/william-mansky"
  - name: "Andrew W. Appel"
    link: "http://www.cs.princeton.edu/~appel/"
  - name: "Aleksey Nogin"
    link: "https://researchr.org/alias/aleksey-nogin"
  year: "2017"
  doi: "http://doi.acm.org/10.1145/3133911"
  links:
    doi: "http://doi.acm.org/10.1145/3133911"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/journals/pacmpl/ManskyAN17"
  researchr: "https://researchr.org/publication/ManskyAN17"
  cites: 0
  citedby: 0
  journal: "Proceedings of the ACM on Programming Languages"
  volume: "1"
  number: "OOPSLA"
  kind: "article"
  key: "ManskyAN17"
- title: "Verified heap theorem prover by paramodulation"
  author:
  - name: "Gordon Stewart"
    link: "https://researchr.org/alias/gordon-stewart"
  - name: "Lennart Beringer"
    link: "https://researchr.org/alias/lennart-beringer"
  - name: "Andrew W. Appel"
    link: "http://www.cs.princeton.edu/~appel/"
  year: "2012"
  doi: "http://doi.acm.org/10.1145/2364527.2364531"
  links:
    doi: "http://doi.acm.org/10.1145/2364527.2364531"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/icfp/StewartBA12"
  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:
  - name: "Peter Thiemann"
    link: "https://researchr.org/alias/peter-thiemann"
  - name: "Robby Bruce Findler"
    link: "https://researchr.org/alias/robby-bruce-findler"
  publisher: "ACM"
  isbn: "978-1-4503-1054-3"
  kind: "inproceedings"
  key: "StewartBA12"
- title: "SSA is Functional Programming"
  author:
  - name: "Andrew W. Appel"
    link: "http://www.cs.princeton.edu/~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"
  kind: "article"
  key: "Appel88:0"
- title: "Simulating digital circuits with one bit per wire"
  author:
  - name: "Andrew W. Appel"
    link: "http://www.cs.princeton.edu/~appel/"
  year: "1988"
  doi: "http://doi.ieeecomputersociety.org/10.1109/43.7796"
  links:
    doi: "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"
  kind: "article"
  key: "Appel88:1"
- title: "Standard ML of New Jersey"
  author:
  - name: "Andrew W. Appel"
    link: "http://www.cs.princeton.edu/~appel/"
  - name: "David B. MacQueen"
    link: "https://researchr.org/alias/david-b.-macqueen"
  year: "1991"
  researchr: "https://researchr.org/publication/AppelM91"
  cites: 0
  citedby: 0
  pages: "1-13"
  booktitle: "PLILP"
  kind: "inproceedings"
  key: "AppelM91"
- title: "Construction of a Semantic Model for a Typed Assembly Language"
  author:
  - name: "Gang Tan"
    link: "https://researchr.org/alias/gang-tan"
  - name: "Andrew W. Appel"
    link: "http://www.cs.princeton.edu/~appel/"
  - name: "Kedar N. Swadi"
    link: "https://researchr.org/alias/kedar-n.-swadi"
  - name: "Dinghao Wu"
    link: "https://researchr.org/alias/dinghao-wu"
  year: "2004"
  doi: "http://springerlink.metapress.com/openurl.asp?genre=article&issn=0302-9743&volume=2937&spage=30"
  links:
    doi: "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:
  - name: "Bernhard Steffen"
    link: "https://researchr.org/alias/bernhard-steffen"
  - name: "Giorgio Levi"
    link: "https://researchr.org/alias/giorgio-levi"
  volume: "2937"
  series: "Lecture Notes in Computer Science"
  publisher: "Springer"
  isbn: "3-540-20803-8"
  kind: "inproceedings"
  key: "TanASW04"
- title: "Is POPL mathematics or science?"
  author:
  - name: "Andrew W. Appel"
    link: "http://www.cs.princeton.edu/~appel/"
  year: "1992"
  doi: "http://doi.acm.org/10.1145/131080.131091"
  links:
    doi: "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"
  kind: "article"
  key: "Appel92"
- title: "Runtime Tags Aren t Necessary"
  author:
  - name: "Andrew W. Appel"
    link: "http://www.cs.princeton.edu/~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"
  kind: "article"
  key: "Appel89"
- title: "Shrink fast correctly!"
  author:
  - name: "Olivier Savary Bélanger"
    link: "https://researchr.org/alias/olivier-savary-b%C3%A9langer"
  - name: "Andrew W. Appel"
    link: "http://www.cs.princeton.edu/~appel/"
  year: "2017"
  doi: "http://doi.acm.org/10.1145/3131851.3131859"
  links:
    doi: "http://doi.acm.org/10.1145/3131851.3131859"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/ppdp/BelangerA17"
  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:
  - name: "Wim Vanhoof"
    link: "https://researchr.org/alias/wim-vanhoof"
  - name: "Brigitte Pientka"
    link: "https://researchr.org/alias/brigitte-pientka"
  publisher: "ACM"
  isbn: "978-1-4503-5291-8"
  kind: "inproceedings"
  key: "BelangerA17"
- title: "Mostly Sound Type System Improves a Foundational Program Verifier"
  author:
  - name: "Josiah Dodds"
    link: "https://researchr.org/alias/josiah-dodds"
  - name: "Andrew W. Appel"
    link: "http://www.cs.princeton.edu/~appel/"
  year: "2013"
  doi: "http://dx.doi.org/10.1007/978-3-319-03545-1_2"
  links:
    doi: "http://dx.doi.org/10.1007/978-3-319-03545-1_2"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/cpp/DoddsA13"
  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:
  - name: "Georges Gonthier"
    link: "https://researchr.org/alias/georges-gonthier"
  - name: "Michael Norrish"
    link: "https://researchr.org/alias/michael-norrish"
  volume: "8307"
  series: "Lecture Notes in Computer Science"
  publisher: "Springer"
  isbn: "978-3-319-03544-4"
  kind: "inproceedings"
  key: "DoddsA13"
- title: "Compiling with Continuations"
  author:
  - name: "Andrew W. Appel"
    link: "http://www.cs.princeton.edu/~appel/"
  year: "1992"
  tags:
  - "compiler"
  researchr: "https://researchr.org/publication/Appel1992"
  cites: 0
  citedby: 0
  publisher: "Cambridge University Press"
  isbn: "0-521-41695-7"
  kind: "book"
  key: "Appel1992"
- title: "Shrinking lambda Expressions in Linear Time"
  author:
  - name: "Andrew W. Appel"
    link: "http://www.cs.princeton.edu/~appel/"
  - name: "Trevor Jim"
    link: "https://researchr.org/alias/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"
  kind: "article"
  key: "AppelJ97"
- title: "Callee-Save Registers in Continuation-Passing Style"
  author:
  - name: "Andrew W. Appel"
    link: "http://www.cs.princeton.edu/~appel/"
  - name: "Zhong Shao"
    link: "https://researchr.org/alias/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"
  kind: "article"
  key: "AppelS92"
- title: "Portable Software Fault Isolation"
  author:
  - name: "Joshua A. Kroll"
    link: "https://researchr.org/alias/joshua-a.-kroll"
  - name: "Gordon Stewart"
    link: "https://researchr.org/alias/gordon-stewart"
  - name: "Andrew W. Appel"
    link: "http://www.cs.princeton.edu/~appel/"
  year: "2014"
  doi: "http://dx.doi.org/10.1109/CSF.2014.10"
  links:
    doi: "http://dx.doi.org/10.1109/CSF.2014.10"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/csfw/KrollSA14"
  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"
  kind: "inproceedings"
  key: "KrollSA14"
- title: "Lightweight Lemmas in lambda-Prolog"
  author:
  - name: "Andrew W. Appel"
    link: "http://www.cs.princeton.edu/~appel/"
  - name: "Amy P. Felty"
    link: "https://researchr.org/alias/amy-p.-felty"
  year: "1999"
  tags:
  - "Prolog"
  researchr: "https://researchr.org/publication/AppelF99"
  cites: 0
  citedby: 0
  pages: "411-425"
  booktitle: "ICLP"
  kind: "inproceedings"
  key: "AppelF99"
- title: "A Logical Mix of Approximation and Separation"
  author:
  - name: "Aquinas Hobor"
    link: "https://researchr.org/alias/aquinas-hobor"
  - name: "Robert Dockins"
    link: "https://researchr.org/alias/robert-dockins"
  - name: "Andrew W. Appel"
    link: "http://www.cs.princeton.edu/~appel/"
  year: "2010"
  doi: "http://dx.doi.org/10.1007/978-3-642-17164-2_30"
  links:
    doi: "http://dx.doi.org/10.1007/978-3-642-17164-2_30"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/aplas/HoborDA10"
  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:
  - name: "Kazunori Ueda"
    link: "https://researchr.org/alias/kazunori-ueda"
  volume: "6461"
  series: "Lecture Notes in Computer Science"
  publisher: "Springer"
  isbn: "978-3-642-17163-5"
  kind: "inproceedings"
  key: "HoborDA10-0"
- title: "A List-machine Benchmark for Mechanized Metatheory: (Extended Abstract)"
  author:
  - name: "Andrew W. Appel"
    link: "http://www.cs.princeton.edu/~appel/"
  - name: "Xavier Leroy"
    link: "http://pauillac.inria.fr/~xleroy/"
  year: "2007"
  doi: "http://dx.doi.org/10.1016/j.entcs.2007.01.020"
  links:
    doi: "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"
  kind: "article"
  key: "AppelL07"
- title: "Vectorized garbage collection"
  author:
  - name: "Andrew W. Appel"
    link: "http://www.cs.princeton.edu/~appel/"
  - name: "Aage Bendiksen"
    link: "https://researchr.org/alias/aage-bendiksen"
  year: "1989"
  doi: "http://dx.doi.org/10.1007/BF00127826"
  links:
    doi: "http://dx.doi.org/10.1007/BF00127826"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/journals/tjs/AppelB89"
  researchr: "https://researchr.org/publication/AppelB89"
  cites: 0
  citedby: 0
  journal: "The Journal of Supercomputing"
  volume: "3"
  number: "3"
  pages: "151-160"
  kind: "article"
  key: "AppelB89"
- title: "Separate Compilation for Standard ML"
  author:
  - name: "Andrew W. Appel"
    link: "http://www.cs.princeton.edu/~appel/"
  - name: "David B. MacQueen"
    link: "https://researchr.org/alias/david-b.-macqueen"
  year: "1994"
  abstract: " Languages that support abstraction and modular structure, such as Standard ML, Modula, Ada, and (more or less) C++, may have deeply nested dependency hierarchies among source files. In ML the problem is particularly severe because ML's powerful parameterized module (functor) facility entails dependencies among implementation modules, not just among interfaces.To efficiently compile individual modules in such languages, it is useful (in ML, necessary) to infer, digest, and cache the static environment resulting from the compilation of each module. Our system provides a simple model of compilation and linkage that supports incremental recompilation (a restricted form of separate compilation) with type-safe linkage. This model is made available to user programs in the form of a set of internal compiler modules, a feature that we call the “visible compiler”. The chief client of this interface is the IRM incremental recompilation manager from CMU. "
  researchr: "https://researchr.org/publication/AppelM94"
  cites: 0
  citedby: 0
  pages: "13-23"
  booktitle: "PLDI"
  kind: "inproceedings"
  key: "AppelM94"
- title: "Polymorphic lemmas and definitions in Lambda Prolog and Twelf"
  author:
  - name: "Andrew W. Appel"
    link: "http://www.cs.princeton.edu/~appel/"
  - name: "Amy P. Felty"
    link: "https://researchr.org/alias/amy-p.-felty"
  year: "2004"
  doi: "http://arxiv.org/abs/cs.LO/0403010"
  note: "informal publication"
  links:
    doi: "http://arxiv.org/abs/cs.LO/0403010"
  tags:
  - "Prolog"
  researchr: "https://researchr.org/publication/cs-LO-0403010"
  cites: 0
  citedby: 0
  journal: "CoRR"
  volume: "cs.LO/0403010"
  kind: "article"
  key: "cs-LO-0403010"
- title: "Iterated Register Coalescing"
  author:
  - name: "Lal George"
    link: "https://researchr.org/alias/lal-george"
  - name: "Andrew W. Appel"
    link: "http://www.cs.princeton.edu/~appel/"
  year: "1996"
  doi: "http://doi.acm.org/10.1145/229542.229546"
  links:
    doi: "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"
  kind: "article"
  key: "GeorgeA96:0"
- title: "Foundational proof checkers with small witnesses"
  author:
  - name: "Dinghao Wu"
    link: "https://researchr.org/alias/dinghao-wu"
  - name: "Andrew W. Appel"
    link: "http://www.cs.princeton.edu/~appel/"
  - name: "Aaron Stump"
    link: "https://researchr.org/alias/aaron-stump"
  year: "2003"
  doi: "http://doi.acm.org/10.1145/888251.888276"
  links:
    doi: "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"
  kind: "inproceedings"
  key: "WuAS03"
- title: "Verified Software Toolchain"
  author:
  - name: "Andrew W. Appel"
    link: "http://www.cs.princeton.edu/~appel/"
  year: "2012"
  doi: "http://dx.doi.org/10.1007/978-3-642-28891-3_2"
  links:
    doi: "http://dx.doi.org/10.1007/978-3-642-28891-3_2"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/nfm/Appel12"
  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:
  - name: "Alwyn Goodloe"
    link: "https://researchr.org/alias/alwyn-goodloe"
  - name: "Suzette Person"
    link: "https://researchr.org/alias/suzette-person"
  volume: "7226"
  series: "Lecture Notes in Computer Science"
  publisher: "Springer"
  isbn: "978-3-642-28890-6"
  kind: "inproceedings"
  key: "Appel12"
- title: "Using Memory Errors to Attack a Virtual Machine"
  author:
  - name: "Sudhakar Govindavajhala"
    link: "https://researchr.org/alias/sudhakar-govindavajhala"
  - name: "Andrew W. Appel"
    link: "http://www.cs.princeton.edu/~appel/"
  year: "2003"
  doi: "http://csdl.computer.org/comp/proceedings/sp/2003/1940/00/19400154abs.htm"
  links:
    doi: "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"
  kind: "inproceedings"
  key: "GovindavajhalaA03"
- title: "MulVAL: A Logic-based Network Security Analyzer"
  author:
  - name: "Xinming Ou"
    link: "https://researchr.org/alias/xinming-ou"
  - name: "Sudhakar Govindavajhala"
    link: "https://researchr.org/alias/sudhakar-govindavajhala"
  - name: "Andrew W. Appel"
    link: "http://www.cs.princeton.edu/~appel/"
  year: "2005"
  doi: "https://www.usenix.org/conference/14th-usenix-security-symposium/mulval-logic-based-network-security-analyzer"
  links:
    doi: "https://www.usenix.org/conference/14th-usenix-security-symposium/mulval-logic-based-network-security-analyzer"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/uss/OuGA05"
  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:
  - name: "Patrick McDaniel"
    link: "https://researchr.org/alias/patrick-mcdaniel"
  publisher: "USENIX Association"
  kind: "inproceedings"
  key: "OuGA05"
- title: "Smartest Recompilation"
  author:
  - name: "Zhong Shao"
    link: "https://researchr.org/alias/zhong-shao"
  - name: "Andrew W. Appel"
    link: "http://www.cs.princeton.edu/~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"
  kind: "inproceedings"
  key: "ShaoA93"
- title: "Oracle Semantics for Concurrent Separation Logic"
  author:
  - name: "Aquinas Hobor"
    link: "https://researchr.org/alias/aquinas-hobor"
  - name: "Andrew W. Appel"
    link: "http://www.cs.princeton.edu/~appel/"
  - name: "Francesco Zappa Nardelli"
    link: "https://researchr.org/alias/francesco-zappa-nardelli"
  year: "2008"
  doi: "http://dx.doi.org/10.1007/978-3-540-78739-6_27"
  links:
    doi: "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:
  - name: "Sophia Drossopoulou"
    link: "https://researchr.org/alias/sophia-drossopoulou"
  volume: "4960"
  series: "Lecture Notes in Computer Science"
  publisher: "Springer"
  isbn: "978-3-540-78738-9"
  kind: "inproceedings"
  key: "HoborAN08"
- title: "Cache Performance of Fast-Allocating Programs"
  author:
  - name: "Marcelo J. R. Gonçalves"
    link: "https://researchr.org/alias/marcelo-j.-r.-gon%C3%A7alves"
  - name: "Andrew W. Appel"
    link: "http://www.cs.princeton.edu/~appel/"
  year: "1995"
  tags:
  - "caching"
  researchr: "https://researchr.org/publication/GoncalvesA95"
  cites: 0
  citedby: 0
  pages: "293-305"
  booktitle: "FPCA"
  kind: "inproceedings"
  key: "GoncalvesA95"
- title: "Verified Software Toolchain - (Invited Talk)"
  author:
  - name: "Andrew W. Appel"
    link: "http://www.cs.princeton.edu/~appel/"
  year: "2011"
  doi: "http://dx.doi.org/10.1007/978-3-642-19718-5_1"
  links:
    doi: "http://dx.doi.org/10.1007/978-3-642-19718-5_1"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/esop/Appel11"
  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:
  - name: "Gilles Barthe"
    link: "https://researchr.org/alias/gilles-barthe"
  volume: "6602"
  series: "Lecture Notes in Computer Science"
  publisher: "Springer"
  isbn: "978-3-642-19717-8"
  kind: "inproceedings"
  key: "Appel11"
- title: "Machine Instruction Syntax and Semantics in Higher Order Logic"
  author:
  - name: "Neophytos G. Michael"
    link: "https://researchr.org/alias/neophytos-g.-michael"
  - name: "Andrew W. Appel"
    link: "http://www.cs.princeton.edu/~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:
  - name: "David A. McAllester"
    link: "https://researchr.org/alias/david-a.-mcallester"
  volume: "1831"
  series: "Lecture Notes in Computer Science"
  publisher: "Springer"
  isbn: "3-540-67664-3"
  kind: "inproceedings"
  key: "MichaelA00"
- title: "Bringing Order to the Separation Logic Jungle"
  author:
  - name: "Qinxiang Cao"
    link: "https://researchr.org/alias/qinxiang-cao"
  - name: "Santiago Cuellar"
    link: "https://researchr.org/alias/santiago-cuellar"
  - name: "Andrew W. Appel"
    link: "http://www.cs.princeton.edu/~appel/"
  year: "2017"
  doi: "https://doi.org/10.1007/978-3-319-71237-6_10"
  links:
    doi: "https://doi.org/10.1007/978-3-319-71237-6_10"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/aplas/CaoCA17"
  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:
  - name: "Bor-Yuh Evan Chang"
    link: "https://researchr.org/alias/bor-yuh-evan-chang"
  volume: "10695"
  series: "Lecture Notes in Computer Science"
  publisher: "Springer"
  isbn: "978-3-319-71237-6"
  kind: "inproceedings"
  key: "CaoCA17"
- title: "A very modal model of a modern, major, general type system"
  author:
  - name: "Andrew W. Appel"
    link: "http://www.cs.princeton.edu/~appel/"
  - name: "Paul-André Melliès"
    link: "https://researchr.org/alias/paul-andr%C3%A9-melli%C3%A8s"
  - name: "Christopher D. Richards"
    link: "https://researchr.org/alias/christopher-d.-richards"
  - name: "Jérôme Vouillon"
    link: "https://researchr.org/alias/j%C3%A9r%C3%B4me-vouillon"
  year: "2007"
  doi: "http://doi.acm.org/10.1145/1190216.1190235"
  links:
    doi: "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:
  - name: "Martin Hofmann"
    link: "https://researchr.org/alias/martin-hofmann"
  - name: "Matthias Felleisen"
    link: "http://www.ccs.neu.edu/home/matthias/"
  publisher: "ACM"
  isbn: "1-59593-575-4"
  kind: "inproceedings"
  key: "AppelMRV07"
- title: "Loop Headers in Lambda-Calculus or CPS"
  author:
  - name: "Andrew W. Appel"
    link: "http://www.cs.princeton.edu/~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"
  kind: "article"
  key: "Appel94"
- title: "Compiling with Continuations (corr. version)"
  author:
  - name: "Andrew W. Appel"
    link: "http://www.cs.princeton.edu/~appel/"
  year: "2006"
  links:
    dblp: "http://dblp.uni-trier.de/rec/bibtex/books/daglib/0022396"
  tags:
  - "compiler"
  researchr: "https://researchr.org/publication/0022396"
  cites: 0
  citedby: 0
  publisher: "Cambridge University Press"
  isbn: "978-0-521-03311-4"
  kind: "book"
  key: "0022396"
- title: "VST-Floyd: A Separation Logic Tool to Verify Correctness of C Programs"
  author:
  - name: "Qinxiang Cao"
    link: "https://researchr.org/alias/qinxiang-cao"
  - name: "Lennart Beringer"
    link: "https://researchr.org/alias/lennart-beringer"
  - name: "Samuel Gruetter"
    link: "https://researchr.org/alias/samuel-gruetter"
  - name: "Josiah Dodds"
    link: "https://researchr.org/alias/josiah-dodds"
  - name: "Andrew W. Appel"
    link: "http://www.cs.princeton.edu/~appel/"
  year: "2018"
  doi: "https://doi.org/10.1007/s10817-018-9457-5"
  links:
    doi: "https://doi.org/10.1007/s10817-018-9457-5"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/journals/jar/CaoBGDA18"
  researchr: "https://researchr.org/publication/CaoBGDA18"
  cites: 0
  citedby: 0
  journal: "Journal of Automated Reasoning"
  volume: "61"
  number: "1-4"
  pages: "367-422"
  kind: "article"
  key: "CaoBGDA18"
- title: "Unrolling Lists"
  author:
  - name: "Zhong Shao"
    link: "https://researchr.org/alias/zhong-shao"
  - name: "John H. Reppy"
    link: "http://www.cs.uchicago.edu/people/jhr"
  - name: "Andrew W. Appel"
    link: "http://www.cs.princeton.edu/~appel/"
  year: "1994"
  doi: "http://doi.acm.org/10.1145/182409.182453"
  links:
    doi: "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"
  kind: "inproceedings"
  key: "ShaoRA94"
- title: "A Standard ML compiler"
  author:
  - name: "Andrew W. Appel"
    link: "http://www.cs.princeton.edu/~appel/"
  - name: "David B. MacQueen"
    link: "https://researchr.org/alias/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:
  - name: "Gilles Kahn"
    link: "https://researchr.org/alias/gilles-kahn"
  volume: "274"
  series: "Lecture Notes in Computer Science"
  publisher: "Springer"
  isbn: "3-540-18317-5"
  kind: "inproceedings"
  key: "AppelM87"
- title: "An Advisor for Flexible Working Sets"
  author:
  - name: "Rafael Alonso"
    link: "https://researchr.org/alias/rafael-alonso"
  - name: "Andrew W. Appel"
    link: "http://www.cs.princeton.edu/~appel/"
  year: "1990"
  doi: "http://doi.acm.org/10.1145/98457.98753"
  links:
    doi: "http://doi.acm.org/10.1145/98457.98753"
  researchr: "https://researchr.org/publication/AlonsoA90"
  cites: 0
  citedby: 0
  pages: "153-162"
  booktitle: "SIGMETRICS"
  kind: "inproceedings"
  key: "AlonsoA90"
- title: "Real-time concurrent collection on stock multiprocessors (with retrospective)"
  author:
  - name: "Andrew W. Appel"
    link: "http://www.cs.princeton.edu/~appel/"
  year: "1988"
  doi: "http://doi.acm.org/10.1145/989393.989417"
  links:
    doi: "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:
  - name: "Kathryn S. McKinley"
    link: "https://researchr.org/alias/kathryn-s.-mckinley"
  publisher: "ACM"
  isbn: "1-58113-623-4"
  kind: "inproceedings"
  key: "Appel88"
- title: "Semantics-Directed Code Generation"
  author:
  - name: "Andrew W. Appel"
    link: "http://www.cs.princeton.edu/~appel/"
  year: "1985"
  tags:
  - "semantics"
  - "code generation"
  researchr: "https://researchr.org/publication/Appel85"
  cites: 0
  citedby: 0
  pages: "315-324"
  booktitle: "POPL"
  kind: "inproceedings"
  key: "Appel85"
- title: "Modern Compiler Implementation in C"
  author:
  - name: "Andrew W. Appel"
    link: "http://www.cs.princeton.edu/~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"
  kind: "book"
  key: "Appel1998c"
- title: "Lambda-Splitting: A Higher-Order Approach to Cross-Module Optimizations"
  author:
  - name: "Matthias Blume"
    link: "https://researchr.org/alias/matthias-blume"
  - name: "Andrew W. Appel"
    link: "http://www.cs.princeton.edu/~appel/"
  year: "1997"
  tags:
  - "optimization"
  - "systematic-approach"
  researchr: "https://researchr.org/publication/BlumeA97"
  cites: 0
  citedby: 0
  pages: "112-124"
  booktitle: "ICFP"
  kind: "inproceedings"
  key: "BlumeA97"
- title: "Allocation without Locking"
  author:
  - name: "Andrew W. Appel"
    link: "http://www.cs.princeton.edu/~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"
  kind: "article"
  key: "Appel89a"
- title: "Concurrent Separation Logic for Pipelined Parallelization"
  author:
  - name: "Christian J. Bell"
    link: "https://researchr.org/alias/christian-j.-bell"
  - name: "Andrew W. Appel"
    link: "http://www.cs.princeton.edu/~appel/"
  - name: "David Walker"
    link: "https://researchr.org/alias/david-walker"
  year: "2010"
  doi: "http://dx.doi.org/10.1007/978-3-642-15769-1_10"
  links:
    doi: "http://dx.doi.org/10.1007/978-3-642-15769-1_10"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/sas/BellAW10"
  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:
  - name: "Radhia Cousot"
    link: "https://researchr.org/alias/radhia-cousot"
  - name: "Matthieu Martel"
    link: "https://researchr.org/alias/matthieu-martel"
  volume: "6337"
  series: "Lecture Notes in Computer Science"
  publisher: "Springer"
  isbn: "978-3-642-15768-4"
  kind: "inproceedings"
  key: "BellAW10"
- title: "A List-Machine Benchmark for Mechanized Metatheory"
  author:
  - name: "Andrew W. Appel"
    link: "http://www.cs.princeton.edu/~appel/"
  - name: "Robert Dockins"
    link: "https://researchr.org/alias/robert-dockins"
  - name: "Xavier Leroy"
    link: "http://pauillac.inria.fr/~xleroy/"
  year: "2012"
  doi: "http://dx.doi.org/10.1007/s10817-011-9226-1"
  links:
    doi: "http://dx.doi.org/10.1007/s10817-011-9226-1"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/journals/jar/AppelDL12"
  researchr: "https://researchr.org/publication/AppelDL12"
  cites: 0
  citedby: 0
  journal: "Journal of Automated Reasoning"
  volume: "49"
  number: "3"
  pages: "453-491"
  kind: "article"
  key: "AppelDL12"
- title: "Modern Compiler Implementation in Java, 2nd edition"
  author:
  - name: "Andrew W. Appel"
    link: "http://www.cs.princeton.edu/~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"
  kind: "book"
  key: "Appel2002"
- title: "Dependent types ensure partial correctness of theorem provers"
  author:
  - name: "Andrew W. Appel"
    link: "http://www.cs.princeton.edu/~appel/"
  - name: "Amy P. Felty"
    link: "https://researchr.org/alias/amy-p.-felty"
  year: "2004"
  doi: "http://dx.doi.org/10.1017/S0956796803004921"
  links:
    doi: "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"
  kind: "article"
  key: "AppelF04"
- title: "Verification of a Cryptographic Primitive: SHA-256"
  author:
  - name: "Andrew W. Appel"
    link: "http://www.cs.princeton.edu/~appel/"
  year: "2015"
  doi: "http://doi.acm.org/10.1145/2701415"
  links:
    doi: "http://doi.acm.org/10.1145/2701415"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/journals/toplas/Appel15"
  researchr: "https://researchr.org/publication/Appel15"
  cites: 0
  citedby: 0
  journal: "ACM Transactions on Programming Languages and Systems"
  volume: "37"
  number: "2"
  pages: "7"
  kind: "article"
  key: "Appel15"
- title: "Security Seals on Voting Machines: A Case Study"
  author:
  - name: "Andrew W. Appel"
    link: "http://www.cs.princeton.edu/~appel/"
  year: "2011"
  doi: "http://doi.acm.org/10.1145/2019599.2019603"
  links:
    doi: "http://doi.acm.org/10.1145/2019599.2019603"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/journals/tissec/Appel11"
  researchr: "https://researchr.org/publication/Appel11-1"
  cites: 0
  citedby: 0
  journal: "ACM Trans. Inf. Syst. Secur."
  volume: "14"
  number: "2"
  pages: "18"
  kind: "article"
  key: "Appel11-1"
- title: "Social processes and proofs of theorems and programs, revisited"
  author:
  - name: "Andrew W. Appel"
    link: "http://www.cs.princeton.edu/~appel/"
  year: "2004"
  doi: "http://doi.acm.org/10.1145/996841.996842"
  links:
    doi: "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:
  - name: "William Pugh"
    link: "https://researchr.org/alias/william-pugh"
  - name: "Craig Chambers"
    link: "https://researchr.org/alias/craig-chambers"
  publisher: "ACM"
  isbn: "1-58113-807-5"
  kind: "inproceedings"
  key: "Appel04"
- title: "A Trustworthy Proof Checker"
  author:
  - name: "Andrew W. Appel"
    link: "http://www.cs.princeton.edu/~appel/"
  - name: "Neophytos G. Michael"
    link: "https://researchr.org/alias/neophytos-g.-michael"
  - name: "Aaron Stump"
    link: "https://researchr.org/alias/aaron-stump"
  - name: "Roberto Virga"
    link: "https://researchr.org/alias/roberto-virga"
  year: "2003"
  doi: "http://dx.doi.org/10.1023/B:JARS.0000021013.61329.58"
  links:
    doi: "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"
  kind: "article"
  key: "AppelMSV03"
- title: "A Runtime System"
  author:
  - name: "Andrew W. Appel"
    link: "http://www.cs.princeton.edu/~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"
  kind: "article"
  key: "Appel90"
- title: "Simple Generational Garbage Collection and Fast Allocation"
  author:
  - name: "Andrew W. Appel"
    link: "http://www.cs.princeton.edu/~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"
  kind: "article"
  key: "Appel89:0"
- title: "Proof-Carrying Authentication"
  author:
  - name: "Andrew W. Appel"
    link: "http://www.cs.princeton.edu/~appel/"
  - name: "Edward W. Felten"
    link: "https://researchr.org/alias/edward-w.-felten"
  year: "1999"
  doi: "http://doi.acm.org/10.1145/319709.319718"
  links:
    doi: "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"
  kind: "inproceedings"
  key: "AppelF99:0"
- title: "An indexed model of recursive types for foundational proof-carrying code"
  author:
  - name: "Andrew W. Appel"
    link: "http://www.cs.princeton.edu/~appel/"
  - name: "David A. McAllester"
    link: "https://researchr.org/alias/david-a.-mcallester"
  year: "2001"
  doi: "http://doi.acm.org/10.1145/504709.504712"
  links:
    doi: "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"
  kind: "article"
  key: "AppelM01"
- title: "Debuggable Concurrency Extensions for Standard ML"
  author:
  - name: "Andrew P. Tolmach"
    link: "http://www.cs.pdx.edu/~apt"
  - name: "Andrew W. Appel"
    link: "http://www.cs.princeton.edu/~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"
  kind: "inproceedings"
  key: "TolmachA91"
- title: "A Stratified Semantics of General References A Stratified Semantics of General References"
  author:
  - name: "Amal J. Ahmed"
    link: "https://researchr.org/alias/amal-j.-ahmed"
  - name: "Andrew W. Appel"
    link: "http://www.cs.princeton.edu/~appel/"
  - name: "Roberto Virga"
    link: "https://researchr.org/alias/roberto-virga"
  year: "2002"
  doi: "http://doi.ieeecomputersociety.org/10.1109/LICS.2002.1029818"
  links:
    doi: "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"
  kind: "inproceedings"
  key: "AhmedAV02"
- title: "Multimodal Separation Logic for Reasoning About Operational Semantics"
  author:
  - name: "Robert Dockins"
    link: "https://researchr.org/alias/robert-dockins"
  - name: "Andrew W. Appel"
    link: "http://www.cs.princeton.edu/~appel/"
  - name: "Aquinas Hobor"
    link: "https://researchr.org/alias/aquinas-hobor"
  year: "2008"
  doi: "http://dx.doi.org/10.1016/j.entcs.2008.10.002"
  links:
    doi: "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"
  kind: "article"
  key: "DockinsAH08"
- title: "Optimal Spilling for CISC Machines with Few Registers"
  author:
  - name: "Andrew W. Appel"
    link: "http://www.cs.princeton.edu/~appel/"
  - name: "Lal George"
    link: "https://researchr.org/alias/lal-george"
  year: "2001"
  researchr: "https://researchr.org/publication/AppelG01"
  cites: 0
  citedby: 0
  pages: "243-253"
  booktitle: "PLDI"
  kind: "inproceedings"
  key: "AppelG01"
- title: "The New Jersey Voting-machine Lawsuit and the AVC Advantage DRE Voting Machine"
  author:
  - name: "Andrew W. Appel"
    link: "http://www.cs.princeton.edu/~appel/"
  - name: "Maia Ginsburg"
    link: "https://researchr.org/alias/maia-ginsburg"
  - name: "Harri Hursti"
    link: "https://researchr.org/alias/harri-hursti"
  - name: "Brian W. Kernighan"
    link: "https://researchr.org/alias/brian-w.-kernighan"
  - name: "Christopher D. Richards"
    link: "https://researchr.org/alias/christopher-d.-richards"
  - name: "Gang Tan"
    link: "https://researchr.org/alias/gang-tan"
  - name: "Penny Venetis"
    link: "https://researchr.org/alias/penny-venetis"
  year: "2009"
  doi: "https://www.usenix.org/conference/evtwote-09/new-jersey-voting-machine-lawsuit-and-avc-advantage-dre-voting-machine"
  links:
    doi: "https://www.usenix.org/conference/evtwote-09/new-jersey-voting-machine-lawsuit-and-avc-advantage-dre-voting-machine"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/uss/AppelGHKRTV09"
  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:
  - name: "David Jefferson"
    link: "https://researchr.org/alias/david-jefferson"
  - name: "Joseph Lorenzo Hall"
    link: "https://researchr.org/alias/joseph-lorenzo-hall"
  - name: "Tal Moran"
    link: "https://researchr.org/alias/tal-moran"
  publisher: "USENIX Association"
  kind: "inproceedings"
  key: "AppelGHKRTV09"
- title: "A Compositional Logic for Control Flow"
  author:
  - name: "Gang Tan"
    link: "https://researchr.org/alias/gang-tan"
  - name: "Andrew W. Appel"
    link: "http://www.cs.princeton.edu/~appel/"
  year: "2006"
  doi: "http://dx.doi.org/10.1007/11609773_6"
  links:
    doi: "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:
  - name: "E. Allen Emerson"
    link: "https://researchr.org/alias/e.-allen-emerson"
  - name: "Kedar S. Namjoshi"
    link: "https://researchr.org/alias/kedar-s.-namjoshi"
  volume: "3855"
  series: "Lecture Notes in Computer Science"
  publisher: "Springer"
  isbn: "3-540-31139-4"
  kind: "inproceedings"
  key: "TanA06"
- title: "Type-preserving garbage collectors"
  author:
  - name: "Daniel C. Wang"
    link: "https://researchr.org/alias/daniel-c.-wang"
  - name: "Andrew W. Appel"
    link: "http://www.cs.princeton.edu/~appel/"
  year: "2001"
  doi: "http://doi.acm.org/10.1145/360204.360218"
  links:
    doi: "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"
  kind: "inproceedings"
  key: "WangA01"
- title: "Traversal-Based Visualization of Data Structures"
  author:
  - name: "Jeffrey L. Korn"
    link: "https://researchr.org/alias/jeffrey-l.-korn"
  - name: "Andrew W. Appel"
    link: "http://www.cs.princeton.edu/~appel/"
  year: "1998"
  doi: "http://dlib.computer.org/conferen/infovis/9093/pdf/90930011.pdf"
  links:
    doi: "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"
  kind: "inproceedings"
  key: "KornA98"
- title: "Separation Logic for Small-Step cminor"
  author:
  - name: "Andrew W. Appel"
    link: "http://www.cs.princeton.edu/~appel/"
  - name: "Sandrine Blazy"
    link: "https://researchr.org/alias/sandrine-blazy"
  year: "2007"
  doi: "http://dx.doi.org/10.1007/978-3-540-74591-4_3"
  links:
    doi: "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:
  - name: "Klaus Schneider"
    link: "https://researchr.org/alias/klaus-schneider"
  - name: "Jens Brandt"
    link: "http://es.cs.uni-kl.de/people/brandt"
  volume: "4732"
  series: "Lecture Notes in Computer Science"
  publisher: "Springer"
  isbn: "978-3-540-74590-7"
  kind: "inproceedings"
  key: "AppelB07"
- title: "Intensional Equality ;=) for Continuations"
  author:
  - name: "Andrew W. Appel"
    link: "http://www.cs.princeton.edu/~appel/"
  year: "1996"
  researchr: "https://researchr.org/publication/Appel96"
  cites: 0
  citedby: 0
  journal: "SIGPLAN Notices"
  volume: "31"
  number: "2"
  pages: "55-57"
  kind: "article"
  key: "Appel96"
- title: "Local actions for a curry-style operational semantics"
  author:
  - name: "Gordon Stewart"
    link: "https://researchr.org/alias/gordon-stewart"
  - name: "Andrew W. Appel"
    link: "http://www.cs.princeton.edu/~appel/"
  year: "2011"
  doi: "http://doi.acm.org/10.1145/1929529.1929535"
  links:
    doi: "http://doi.acm.org/10.1145/1929529.1929535"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/plpv/StewartA11"
  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:
  - name: "Ranjit Jhala"
    link: "https://researchr.org/alias/ranjit-jhala"
  - name: "Wouter Swierstra"
    link: "https://researchr.org/alias/wouter-swierstra"
  publisher: "ACM"
  isbn: "978-1-4503-0487-0"
  kind: "inproceedings"
  key: "StewartA11"
- title: "A theory of indirection via approximation"
  author:
  - name: "Aquinas Hobor"
    link: "https://researchr.org/alias/aquinas-hobor"
  - name: "Robert Dockins"
    link: "https://researchr.org/alias/robert-dockins"
  - name: "Andrew W. Appel"
    link: "http://www.cs.princeton.edu/~appel/"
  year: "2010"
  doi: "http://doi.acm.org/10.1145/1706299.1706322"
  links:
    doi: "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:
  - name: "Manuel V. Hermenegildo"
    link: "https://researchr.org/alias/manuel-v.-hermenegildo"
  - name: "Jens Palsberg"
    link: "https://researchr.org/alias/jens-palsberg"
  publisher: "ACM"
  isbn: "978-1-60558-479-9"
  kind: "inproceedings"
  key: "HoborDA10"
- title: "Technological access control interferes with noninfringing scholarship"
  author:
  - name: "Andrew W. Appel"
    link: "http://www.cs.princeton.edu/~appel/"
  - name: "Edward W. Felten"
    link: "https://researchr.org/alias/edward-w.-felten"
  year: "2000"
  doi: "http://doi.acm.org/10.1145/348941.348968"
  links:
    doi: "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"
  kind: "article"
  key: "AppelF00"
- title: "Semantic foundations for typed assembly languages"
  author:
  - name: "Amal Ahmed"
    link: "https://researchr.org/alias/amal-ahmed"
  - name: "Andrew W. Appel"
    link: "http://www.cs.princeton.edu/~appel/"
  - name: "Christopher D. Richards"
    link: "https://researchr.org/alias/christopher-d.-richards"
  - name: "Kedar N. Swadi"
    link: "https://researchr.org/alias/kedar-n.-swadi"
  - name: "Gang Tan"
    link: "https://researchr.org/alias/gang-tan"
  - name: "Daniel C. Wang"
    link: "https://researchr.org/alias/daniel-c.-wang"
  year: "2010"
  doi: "http://doi.acm.org/10.1145/1709093.1709094"
  links:
    doi: "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"
  kind: "article"
  key: "AhmedARSTW10"
- title: "Iterated Register Coalescing"
  author:
  - name: "Lal George"
    link: "https://researchr.org/alias/lal-george"
  - name: "Andrew W. Appel"
    link: "http://www.cs.princeton.edu/~appel/"
  year: "1996"
  doi: "http://doi.acm.org/10.1145/237721.237777"
  links:
    doi: "http://doi.acm.org/10.1145/237721.237777"
  researchr: "https://researchr.org/publication/GeorgeA96"
  cites: 0
  citedby: 0
  pages: "208-218"
  booktitle: "POPL"
  kind: "inproceedings"
  key: "GeorgeA96"
- title: "Garbage Collection can be Faster than Stack Allocation"
  author:
  - name: "Andrew W. Appel"
    link: "http://www.cs.princeton.edu/~appel/"
  year: "1987"
  researchr: "https://researchr.org/publication/Appel87"
  cites: 0
  citedby: 0
  journal: "Inf. Process. Lett."
  volume: "25"
  number: "4"
  pages: "275-279"
  kind: "article"
  key: "Appel87"
- title: "Real-Time Concurrent Collection on Stock Multiprocessors"
  author:
  - name: "Andrew W. Appel"
    link: "http://www.cs.princeton.edu/~appel/"
  - name: "John R. Ellis"
    link: "https://researchr.org/alias/john-r.-ellis"
  - name: "Kai Li"
    link: "https://researchr.org/alias/kai-li"
  year: "1988"
  researchr: "https://researchr.org/publication/AppelEL88"
  cites: 0
  citedby: 0
  pages: "11-20"
  booktitle: "PLDI"
  kind: "inproceedings"
  key: "AppelEL88"
- title: "Policy-enforced linking of untrusted components"
  author:
  - name: "Eunyoung Lee"
    link: "https://researchr.org/alias/eunyoung-lee"
  - name: "Andrew W. Appel"
    link: "http://www.cs.princeton.edu/~appel/"
  year: "2003"
  doi: "http://doi.acm.org/10.1145/940071.940124"
  links:
    doi: "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"
  kind: "inproceedings"
  key: "LeeA03"
- title: "The World s Fastest Scrabble Program"
  author:
  - name: "Andrew W. Appel"
    link: "http://www.cs.princeton.edu/~appel/"
  - name: "Guy J. Jacobson"
    link: "https://researchr.org/alias/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"
  kind: "article"
  key: "AppelJ88"
- 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"
  doi: "http://dl.acm.org/citation.cfm?id=292540"
  links:
    doi: "http://dl.acm.org/citation.cfm?id=292540"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/popl/1999"
  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:
  - name: "Andrew W. Appel"
    link: "http://www.cs.princeton.edu/~appel/"
  - name: "Alex Aiken"
    link: "https://researchr.org/alias/alex-aiken"
  publisher: "ACM"
  isbn: "1-58113-095-3"
  kind: "proceedings"
  key: "popl-1999"