A Meta Linear Logical Framework. - Andrew McCreight; Carsten Schürmann (LFM@IJCAR, 2004)

A verifiable SSA program representation for aggressive compiler optimization. - Vijay Menon 002; Neal Glew; Brian R. Murphy; Andrew McCreight; Tatiana Shpeisman; Ali-Reza Adl-Tabatabai; Leaf Petersen (POPL, 2006)

A general framework for certifying garbage collectors and their mutators. - Andrew McCreight; Zhong Shao 001; Chunxiao Lin; Long Li (PLDI, 2007)

Foundational Typed Assembly Language with Certified Garbage Collection. - Chunxiao Lin; Andrew McCreight; Zhong Shao 001; Yiyun Chen; Yu Guo (TASE, 2007)

Practical Tactics for Separation Logic. - Andrew McCreight (TPHOLs, 2009)

A certified framework for compiling and executing garbage-collected languages. - Andrew McCreight; Tim Chevalier; Andrew P. Tolmach (ICFP, 2010)