Existing verified compilers are proved correct under a closed-world assumption, i.e., that the compiler will only be used to compile whole programs. We present a new methodology for verifying correct compilation of program components, while formally allowing linking with target code of arbitrary provenance. To demonstrate our methodology, we present a two-pass type-preserving open compiler and prove that compilation preserves semantics. The central novelty of our approach is that we define a combined language that embeds the source, intermediate, and target languages and formalizes a semantics of interoperability between them, using boundaries in the style of Matthews and Findler. Compiler correctness is stated as contextual equivalence in the combined language. Note to reader: We use blue, red, and purple to typeset terms in various languages. This paper will be difficult to follow unless read/printed in color. © 2014 Springer-Verlag.
CITATION STYLE
Perconti, J. T., & Ahmed, A. (2014). Verifying an open compiler using multi-language semantics. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 8410 LNCS, pp. 128–148). Springer Verlag. https://doi.org/10.1007/978-3-642-54833-8_8
Mendeley helps you to discover research relevant for your work.