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