Yasuhiko Minamide, Koji Okuma: Verifying the CPS Transformation in Isabelle/HOL. APLAS 2001: 29-37