Verifying the CPS Transformation in Isabelle/HOL. - Yasuhiko Minamide; Koji Okuma (APLAS, 2001)

Executing Verified Compiler Specification. - Koji Okuma; Yasuhiko Minamide (APLAS, 2003)

Verifying CPS transformations in Isabelle/HOL. - Yasuhiko Minamide; Koji Okuma (MERLIN, 2003)