publications:
- title: "Practical Tactics for Separation Logic"
  author:
  - name: "Andrew McCreight"
    link: "http://web.cecs.pdx.edu/~mccreigh/"
  year: "2009"
  doi: "http://dx.doi.org/10.1007/978-3-642-03359-9_24"
  links:
    doi: "http://dx.doi.org/10.1007/978-3-642-03359-9_24"
  tags:
  - "logic"
  researchr: "https://researchr.org/publication/McCreight09"
  cites: 0
  citedby: 0
  pages: "343-358"
  booktitle: "tphol"
  kind: "inproceedings"
  key: "McCreight09"
- title: "A Meta Linear Logical Framework"
  author:
  - name: "Andrew McCreight"
    link: "http://web.cecs.pdx.edu/~mccreigh/"
  - name: "Carsten Schürmann"
    link: "https://researchr.org/alias/carsten-sch%C3%BCrmann"
  year: "2008"
  doi: "http://dx.doi.org/10.1016/j.entcs.2007.11.016"
  links:
    doi: "http://dx.doi.org/10.1016/j.entcs.2007.11.016"
  tags:
  - "meta-model"
  - "Meta-Environment"
  - "meta-objects"
  researchr: "https://researchr.org/publication/McCreightS08"
  cites: 0
  citedby: 0
  journal: "ENTCS"
  volume: "199"
  pages: "129-147"
  kind: "article"
  key: "McCreightS08"
- title: "A general framework for certifying garbage collectors and their mutators"
  author:
  - name: "Andrew McCreight"
    link: "http://web.cecs.pdx.edu/~mccreigh/"
  - name: "Zhong Shao"
    link: "https://researchr.org/alias/zhong-shao"
  - name: "Chunxiao Lin"
    link: "https://researchr.org/alias/chunxiao-lin"
  - name: "Long Li"
    link: "https://researchr.org/alias/long-li"
  year: "2007"
  doi: "http://doi.acm.org/10.1145/1250734.1250788"
  links:
    doi: "http://doi.acm.org/10.1145/1250734.1250788"
  researchr: "https://researchr.org/publication/McCreightSLL07"
  cites: 0
  citedby: 0
  pages: "468-479"
  booktitle: "PLDI"
  kind: "inproceedings"
  key: "McCreightSLL07"
- title: "A verifiable SSA program representation for aggressive compiler optimization"
  author:
  - name: "Vijay Menon"
    link: "https://researchr.org/alias/vijay-menon"
  - name: "Neal Glew"
    link: "https://researchr.org/alias/neal-glew"
  - name: "Brian R. Murphy"
    link: "https://researchr.org/alias/brian-r.-murphy"
  - name: "Andrew McCreight"
    link: "http://web.cecs.pdx.edu/~mccreigh/"
  - name: "Tatiana Shpeisman"
    link: "https://researchr.org/alias/tatiana-shpeisman"
  - name: "Ali-Reza Adl-Tabatabai"
    link: "https://researchr.org/alias/ali-reza-adl-tabatabai"
  - name: "Leaf Petersen"
    link: "https://researchr.org/alias/leaf-petersen"
  year: "2006"
  doi: "http://doi.acm.org/10.1145/1111037.1111072"
  links:
    doi: "http://doi.acm.org/10.1145/1111037.1111072"
  tags:
  - "optimization"
  - "compiler"
  - "program optimization"
  researchr: "https://researchr.org/publication/MenonGMMSAP06"
  cites: 0
  citedby: 0
  pages: "397-408"
  booktitle: "POPL"
  kind: "inproceedings"
  key: "MenonGMMSAP06"
- title: "A certified framework for compiling and executing garbage-collected languages"
  author:
  - name: "Andrew McCreight"
    link: "http://web.cecs.pdx.edu/~mccreigh/"
  - name: "Tim Chevalier"
    link: "https://researchr.org/alias/tim-chevalier"
  - name: "Andrew P. Tolmach"
    link: "http://www.cs.pdx.edu/~apt"
  year: "2010"
  doi: "http://doi.acm.org/10.1145/1863543.1863584"
  abstract: "We describe the design, implementation, and use of a machine-certified framework for correct compilation and execution of programs in garbage-collected languages. Our framework extends Leroy's Coq-certified Compcert compiler and Cminor intermediate language. We add: (i) a new intermediate language, GCminor, that includes primitives for allocating memory in a garbage-collected heap and for specifying GC roots; (ii) a precise, low-level specification for a Cminor library for garbage collection; and (iii) a proven semantics-preserving translation from GCminor to Cminor plus the GC library. GCminor neatly encapsulates the interface between mutator and collector code, while remaining simple and flexible enough to be used with a wide variety of source languages and collector styles. Front ends targeting GCminor can be implemented using any compiler technology and any desired degree of verification, including full semantics preservation, type preservation, or informal trust. As an example application of our framework, we describe a compiler for Haskell that translates the Glasgow Haskell Compiler's Core intermediate language to GCminor. To support a simple but useful memory safety argument for this compiler, the front end uses a novel combination of type preservation and runtime checks, which is of independent interest. "
  links:
    doi: "http://doi.acm.org/10.1145/1863543.1863584"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/icfp/McCreightCT10"
  tags:
  - "programming languages"
  - "semantics"
  - "translation"
  - "application framework"
  - "program verification"
  - "language design"
  - "Haskell"
  - "source-to-source"
  - "type checking"
  - "compiler"
  - "design"
  - "open-source"
  researchr: "https://researchr.org/publication/McCreightCT10"
  cites: 37
  citedby: 0
  pages: "273-284"
  booktitle: "ICFP"
  kind: "inproceedings"
  key: "McCreightCT10"
- title: "Foundational Typed Assembly Language with Certified Garbage Collection"
  author:
  - name: "Chunxiao Lin"
    link: "https://researchr.org/alias/chunxiao-lin"
  - name: "Andrew McCreight"
    link: "http://web.cecs.pdx.edu/~mccreigh/"
  - name: "Zhong Shao"
    link: "https://researchr.org/alias/zhong-shao"
  - name: "Yiyun Chen"
    link: "https://researchr.org/alias/yiyun-chen"
  - name: "Yu Guo"
    link: "https://researchr.org/alias/yu-guo"
  year: "2007"
  doi: "http://doi.ieeecomputersociety.org/10.1109/TASE.2007.28"
  links:
    doi: "http://doi.ieeecomputersociety.org/10.1109/TASE.2007.28"
  researchr: "https://researchr.org/publication/LinMSCG07"
  cites: 0
  citedby: 0
  pages: "326-338"
  booktitle: "tase"
  kind: "inproceedings"
  key: "LinMSCG07"