Koji Okuma, Yasuhiko Minamide: Executing Verified Compiler Specification. APLAS 2003: 178-194