2026-07-20T11:57:04Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:5968 2024-03-06T10:37:23Z ddc:004 open_access

Compositional Compiler Verification for a Multi-Language World Ahmed, Amal verified compilation; compositional compiler correctness multi-language semantics typed low-level languages Verified compilers are typically proved correct under severe restrictions on what the compiler's output may be linked with, from no linking at all to linking only with code compiled from the same source language. Such assumptions contradict the reality of how we use these compilers since most software systems today are comprised of components written in different languages compiled by different compilers to a common target, as well as low-level libraries that may be handwritten in the target language. The key challenge in verifying compilers for today's world of multi-language software is how to formally state a compiler correctness theorem that is compositional along two dimensions. First, the theorem must guarantee correct compilation of components while allowing compiled code to be composed (linked) with target-language components of arbitrary provenance, including those compiled from other languages. Second, the theorem must support verification of multi-pass compilers by composing correctness proofs for individual passes. In this talk, I will describe a methodology for verifying compositional compiler correctness for a higher-order typed language and discuss the challenges that lie ahead. I will argue that compositional compiler correctness is, in essence, a language interoperability problem: for viable solutions in the long term, high-level languages must be equipped with principled foreign-function interfaces that specify safe interoperability between high-level and low-level components, and between more precisely and less precisely typed code. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Amal Ahmed 2016 Is Part Of LIPIcs, Volume 52, 1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.FSCD.2016.1 urn:nbn:de:0030-drops-59680 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2016.1 eng https://creativecommons.org/licenses/by/3.0/legalcode