Sat 22 Jun 2019 11:00 - 11:30 at 106B - Compiler Verification Chair(s): Zhong Shao
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
Sat 22 Jun

Displayed time zone: Tijuana, Baja California change

11:00 - 12:30
Compiler VerificationDeepSpec at 106B
Chair(s): Zhong ShaoYale University
11:00
30m
Talk
Closure Conversion is Safe for Space
DeepSpec
Zoe ParaskevopoulouPrinceton University, Andrew AppelPrinceton
11:30
30m
Talk
Fast, Verified Partial Evaluation
DeepSpec
Adam ChlipalaMassachusetts Institute of Technology, USA
12:00
30m
Talk
Stack-Aware CompCert
DeepSpec
Yuting WangYale University