Write a Blog >>
ICFP 2019
Sun 18 - Fri 23 August 2019 Berlin, Germany
Mon 19 Aug 2019 14:37 - 15:00 at Aurora Borealis - Verified Compilation Chair(s): Ralf Jung

Compiler correctness is an old problem, with results stretching back beyond the last half-century. Founding the field, John McCarthy and James Painter set out to build a “completely trustworthy compiler”. And yet, until quite recently, even despite truly impressive verification efforts, the theorems being proved were only about the compilation of whole programs, a theoretically quite appealing but practically unrealistic simplification. For a compiler correctness theorem to assure complete trust, the theorem must reflect the reality of how the compiler will be used.

While there’s been much recent work on more realistic “compositional” compiler correctness, the variety of theorems, stated in remarkably different ways, raises questions about what researchers even mean by a “compiler is correct.”
In this pearl, we develop a new framework with which to understand compiler correctness theorems in the presence of linking, and apply it to understanding and comparing this diversity of results. In doing so, not only are we better able to assess their relative strengths and weaknesses, but gain insight into what we as a community should expect from compiler correctness theorems of the future.

Mon 19 Aug
Times are displayed in time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

13:30 - 15:00: Verified CompilationResearch Papers at Aurora Borealis
Chair(s): Ralf JungMPI-SWS
13:30 - 13:52
Narcissus: Correct-By-Construction Derivation of Decoders and Encoders from Binary Formats
Research Papers
Benjamin DelawarePurdue University, Sorawit Suriyakarn, Clément Pit-ClaudelMIT CSAIL, Qianchuan YePurdue University, Adam ChlipalaMassachusetts Institute of Technology
Link to publication DOI Authorizer link
13:52 - 14:15
Closure Conversion is Safe for Space
Research Papers
Zoe ParaskevopoulouPrinceton University, Andrew AppelPrinceton
14:15 - 14:37
Linear capabilities for fully abstract compilation of separation-logic-verified code
Research Papers
Thomas Van StrydonckKULeuven, Frank PiessensKU Leuven, Dominique DevrieseVrije Universiteit Brussel
14:37 - 15:00
The Next 700 Compiler Correctness Theorems. A Functional Pearl.
Research Papers
Daniel PattersonNortheastern University, Amal AhmedNortheastern University, USA