Strictly capturing non-strict closures
Strictly capturing non-strict closures
复制标题
严格捕获非严格闭包
DOI：
10.1145/3441296.3441398
复制
发表时间：
2021
期刊：
影响因子：
--
通讯作者：
Ariola, Zena M.
中科院分区：
文献类型：
--
作者：
Sullivan, Zachary J.;Downen, Paul;Ariola, Zena M.
所有函数式语言都需要闭包。闭包转换是一种编译器转换，它将静态代码嵌入到程序中以创建和操作闭包，从而避免了对特殊运行时闭包支持的需要。对于按值调用语言，闭包转换一直是关于正确性（例如类型保持和上下文等价）和性能（例如空间使用）的广泛研究的焦点。不幸的是，非严格语言在这些研究中被忽视了。本文旨在填补这一空白。我们开始与调用的名称和调用的需要源语言的语义自动生成闭包在运行时。接下来，我们给出了这两种非严格语言到低级目标语言的类型保持闭包转换，而无需在运行时生成闭包。尽管我们的源语言是非严格的，但我们表明必须急切地创建闭包，这需要目标语言中严格的产品概念。我们扩展了逻辑关系技术，用于证明编译器的正确性调用的值的语言，适用于非严格的语言。在这样做的时候，我们确定了一些重要的属性，推理记忆与堆。
All functional languages need closures. Closure-conversion is a compiler transformation that embeds static code into the program for creating and manipulating closures, avoiding the need for special run-time closure support. For call-by-value languages, closure-conversion has been the focus of extensive studies concerning correctness, such as type preservation and contextual equivalence, and performance, such as space usage. Unfortunately, non-strict languages have been neglected in these studies. This paper aims to fill this gap.We begin with both a call-by-name and a call-by-need source language whose semantics automatically generates closures at run-time. Next, we give type-preserving closure-conversions for these two non-strict languages into a lower-level target languagewithoutautomatic closure generation at run-time. Despite the fact that our source languages are non-strict, we show that closures must be created eagerly, which requires a strict notion of product in the target language. We extend logical relation techniques used to prove compiler correctness for call-by-value languages, to apply to non-strict languages too. In doing so, we identify some important properties for reasoning about memoization with a heap.
登录
查看更多内容
DOI：
--
发表时间：
2004
期刊：
影响因子：
--
作者：
Thomas Johnsson;T. S. Badhusgatan
通讯作者：
T. S. Badhusgatan
带控制的类型化按需调用 λ 演算的可实现性解释和规范化
DOI：
--
发表时间：
2018
期刊：
Foundations of Software Science and Computation Structure
影响因子：
--
作者：
Étienne Miquey;Hugo Herbelin
通讯作者：
Hugo Herbelin
DOI：
--
发表时间：
2018
期刊：
ACM-SIGPLAN Symposium on Programming Language Design and Implementation
影响因子：
--
作者：
W. J. Bowman;Amal J. Ahmed
通讯作者：
Amal J. Ahmed
闭合转换对于空间来说是安全的
DOI：
--
发表时间：
2019
期刊：
Proc. ACM Program. Lang.
影响因子：
--
作者：
Zoe Paraskevopoulou;A. Appel
通讯作者：
A. Appel
延续传递、闭包传递风格
DOI：
10.1145/75277.75303
发表时间：
1989
期刊：
Proceedings Design, Automation and Test in Europe. Conference and Exhibition 2001
影响因子：
--
作者：
A. Appel;T. Jim
通讯作者：
T. Jim