Type-Based Allocation Analysis for Co-recursion in Lazy Functional Languages
Type-Based Allocation Analysis for Co-recursion in Lazy Functional Languages
复制标题
惰性函数语言中基于类型的共递归分配分析
DOI：
10.1007/978-3-662-46669-8_32
复制
发表时间：
2015
期刊：
影响因子：
--
通讯作者：
K. Hammond
中科院分区：
文献类型：
--
作者：
Pedro B. Vasconcelos;Steffen Jost;Mário Florido;K. Hammond
本文在一种简单的惰性求值函数语言中提出了一种预测共递归定义的内存分配成本上界的新型类型-效果分析方法。我们针对Launchbury的惰性评估语义的仪器化变体（作为正式的成本模型）展示了该系统的可靠性。我们的可靠性证明需要使用间接的中间语义。因此，我们提供的这些语义之间的对应证明是这项工作的关键部分。
This paper presents a novel type-and-effect analysis for predicting upper-bounds on memory allocation costs for co-recursive definitions in a simple lazily-evaluated functional language. We show the soundness of this system against an instrumented variant of Launchbury’s semantics for lazy evaluation which serves as a formal cost model. Our soundness proof requires an intermediate semantics employing indirections. Our proof of correspondence between these semantics that we provide is thus a crucial part of this work.