Olivier Danvy, Belmina Dzafic, Frank Pfenning: On proving syntactic properties of CPS programs. HOOTS 1999: 21-33