License: Creative Commons Attribution 3.0 Unported license (CC BY 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.FSCD.2016.1
URN: urn:nbn:de:0030-drops-59680
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2016/5968/
Go to the corresponding LIPIcs Volume Portal

Ahmed, Amal

Compositional Compiler Verification for a Multi-Language World

pdf-format:
LIPIcs-FSCD-2016-1.pdf (0.2 MB)

Abstract

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.

BibTeX - Entry

@InProceedings{ahmed:LIPIcs:2016:5968,
  author =	{Amal Ahmed},
  title =	{{Compositional Compiler Verification for a Multi-Language World}},
  booktitle =	{1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016)},
  pages =	{1:1--1:1},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-010-1},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{52},
  editor =	{Delia Kesner and Brigitte Pientka},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2016/5968},
  URN =		{urn:nbn:de:0030-drops-59680},
  doi =		{10.4230/LIPIcs.FSCD.2016.1},
  annote =	{Keywords: verified compilation; compositional compiler correctness, multi-language semantics, typed low-level languages}
}

Keywords: verified compilation; compositional compiler correctness, multi-language semantics, typed low-level languages
Collection: 1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016)
Issue Date: 2016
Date of publication: 17.06.2016

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI