Closure conversion is safe for space

Zoe Paraskevopoulou, Andrew W. Appel

Research output: Contribution to journalArticlepeer-review

7 Scopus citations

Abstract

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 the CertiCoq compiler pipeline from Coq (Gallina) through CompCert Clight to assembly language. Our results are mechanized in the Coq proof assistant.

Original languageEnglish (US)
Article number83
JournalProceedings of the ACM on Programming Languages
Volume3
Issue numberICFP
DOIs
StatePublished - Aug 2019

All Science Journal Classification (ASJC) codes

  • Software
  • Safety, Risk, Reliability and Quality

Keywords

  • Closure conversion
  • Compiler correctness
  • Continuation-passing style
  • Cost models
  • Garbage collection
  • Logical relations

Fingerprint

Dive into the research topics of 'Closure conversion is safe for space'. Together they form a unique fingerprint.

Cite this