@inproceedings{McCreight09,
  title = {Practical Tactics for Separation Logic},
  author = {Andrew McCreight},
  year = {2009},
  doi = {10.1007/978-3-642-03359-9_24},
  url = {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},
}

@article{McCreightS08,
  title = {A Meta Linear Logical Framework},
  author = {Andrew McCreight and Carsten Schürmann},
  year = {2008},
  doi = {10.1016/j.entcs.2007.11.016},
  url = {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},
}

@inproceedings{McCreightSLL07,
  title = {A general framework for certifying garbage collectors and their mutators},
  author = {Andrew McCreight and Zhong Shao and Chunxiao Lin and Long Li},
  year = {2007},
  doi = {10.1145/1250734.1250788},
  url = {http://doi.acm.org/10.1145/1250734.1250788},
  researchr = {https://researchr.org/publication/McCreightSLL07},
  cites = {0},
  citedby = {0},
  pages = {468-479},
  booktitle = {PLDI},
}

@inproceedings{MenonGMMSAP06,
  title = {A verifiable SSA program representation for aggressive compiler optimization},
  author = {Vijay Menon and Neal Glew and Brian R. Murphy and Andrew McCreight and Tatiana Shpeisman and Ali-Reza Adl-Tabatabai and Leaf Petersen},
  year = {2006},
  doi = {10.1145/1111037.1111072},
  url = {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},
}

@inproceedings{McCreightCT10,
  title = {A certified framework for compiling and executing garbage-collected languages},
  author = {Andrew McCreight and Tim Chevalier and Andrew P. Tolmach},
  year = {2010},
  doi = {10.1145/1863543.1863584},
  url = {http://doi.acm.org/10.1145/1863543.1863584},
  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},
}

@inproceedings{LinMSCG07,
  title = {Foundational Typed Assembly Language with Certified Garbage Collection},
  author = {Chunxiao Lin and Andrew McCreight and Zhong Shao and Yiyun Chen and Yu Guo},
  year = {2007},
  doi = {10.1109/TASE.2007.28},
  url = {http://doi.ieeecomputersociety.org/10.1109/TASE.2007.28},
  researchr = {https://researchr.org/publication/LinMSCG07},
  cites = {0},
  citedby = {0},
  pages = {326-338},
  booktitle = {tase},
}