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.SNAPL.2015.15
URN: urn:nbn:de:0030-drops-50131
Go to the corresponding LIPIcs Volume Portal

Ahmed, Amal

Verified Compilers for a Multi-Language World

3.pdf (0.6 MB)


Though there has been remarkable progress on formally verified compilers in recent years, most of these compilers suffer from a serious limitation: they are proved correct under the assumption that they will only be used to compile whole programs. This is an unrealistic assumption since most software systems today are comprised of components written in different languages - both typed and untyped - compiled by different compilers to a common target, as well as low-level libraries that may be handwritten in the target language.

We are pursuing a new methodology for building verified compilers for today's world of multi-language software. The project has two central themes, both of which stem from a view of compiler correctness as a language interoperability problem. First, to specify correctness of component compilation, we require that if a source component s compiles to target component t, then t linked with some arbitrary target code t' should behave the same as s interoperating with t'. The latter demands a formal semantics of interoperability between the source and target languages. Second, to enable safe interoperability between components compiled from languages as different as ML, Rust, Python, and C, we plan to design a gradually type-safe target language based on LLVM that supports safe interoperability between more precisely typed, less precisely typed, and type-unsafe components. Our approach opens up a new avenue for exploring sensible language interoperability while also tackling compiler correctness.

BibTeX - Entry

  author =	{Amal Ahmed},
  title =	{{Verified Compilers for a Multi-Language World}},
  booktitle =	{1st Summit on Advances in Programming Languages (SNAPL 2015)},
  pages =	{15--31},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-80-4},
  ISSN =	{1868-8969},
  year =	{2015},
  volume =	{32},
  editor =	{Thomas Ball and Rastislav Bodik and Shriram Krishnamurthi and Benjamin S. Lerner and Greg Morrisett},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{},
  URN =		{urn:nbn:de:0030-drops-50131},
  doi =		{10.4230/LIPIcs.SNAPL.2015.15},
  annote =	{Keywords: verified compilation, compositional compiler correctness, multi-language semantics, typed low-level languages, gradual typing}

Keywords: verified compilation, compositional compiler correctness, multi-language semantics, typed low-level languages, gradual typing
Collection: 1st Summit on Advances in Programming Languages (SNAPL 2015)
Issue Date: 2015
Date of publication: 30.04.2015

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