Sciweavers

APLAS
2003
ACM

Executing Verified Compiler Specification

13 years 7 months ago
Executing Verified Compiler Specification
Abstract. Much work has been done in verifying a compiler specification, both in hand-written and mechanical proofs. However, there is still a gap between a correct compiler specification and a correct compiler implementation. To fill this gap and obtain a correct compiler implementation, we take the approach of generating a compiler from its specification. We verified the correctness of a compiler specification with the theorem prover Isabelle/HOL, and generated a Standard ML code corresponding to the specification with Isabelle's code generation facility. The generated compiler can be executed with some hand-written codes, and it compiles a small functional programming language into the Java virtual machine with several program transformations.
Koji Okuma, Yasuhiko Minamide
Added 23 Aug 2010
Updated 23 Aug 2010
Type Conference
Year 2003
Where APLAS
Authors Koji Okuma, Yasuhiko Minamide
Comments (0)