Formalizing a correctness property of a type-directed partial evaluator. - Noriko Hirota; Kenichi Asai (PLPV, 2014)