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

We formally prove that closure conversion with flat environments for CPS lambda calculus is correct (preserves semantics) and safe for time and space, meaning that produced code preserves the time and space required for the execution of the source program.

We give a cost model to pre- and post-closure-conversion code by formalizing profiling semantics that keep track of the time and space resources needed for the execution of a program, taking garbage collection into account. To show preservation of time and space we set up a general, "garbage-collection compatible'', binary logical relation that establishes invariants on resource consumption of the related programs, along with functional correctness. Using this framework, we show semantics preservation and space and time safety for terminating source programs, and divergence preservation and space safety for diverging source programs.

This is the first formal proof of space-safety of a closure-conversion transformation. The transformation and the proof are parts of a compiler pipeline. Our results are mechanized in the Coq proof assistant.

Conference Day
Mon 19 Aug

Displayed 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
22m
Talk
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
22m
Talk
Closure Conversion is Safe for Space
Research Papers
Zoe ParaskevopoulouPrinceton University, Andrew AppelPrinceton
14:15
22m
Talk
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
22m
Talk
The Next 700 Compiler Correctness Theorems. A Functional Pearl.
Research Papers
Daniel PattersonNortheastern University, Amal AhmedNortheastern University, USA