Fundamentals of Software Engineering - 7th International Conference, FSEN 2017, Tehran, Iran, April 26-28, 2017, Revised Selected Papers
Fundamentals of Software Engineering - 7th International Conference, FSEN 2017, Tehran, Iran, April 26-28, 2017, Revised Selected Papers
复制标题
软件工程基础 - 第七届国际会议，FSEN 2017，伊朗德黑兰，2017 年 4 月 26-28 日，修订后的精选论文
DOI：
10.1007/978-3-319-68972-2_1
复制
发表时间：
2017
期刊：
影响因子：
--
通讯作者：
Accattoli B
中科院分区：
文献类型：
--
作者：
Accattoli B
按值调用演算的理论依赖于弱评估和封闭项，这是编程语言研究中的自然假设。然而，为了对证明助手进行建模，需要强有力的评估和开放条款。开放值调用是开放项弱求值的中间设置，在此基础上，Grégoire 和 Leroy 设计了 Coq 抽象机。本文提供了一种用于开放式按值调用的抽象机理论。文献中包含的机器要么简单但效率低下，因为它们具有指数级的开销，要么高效但笨重，因为它们依赖于环境标签和技术优化。我们引入了一种简单而高效的机器：它不使用标签，并且在双线性开销内实现开放的按值调用。此外，我们对不同的优化如何影响开销的复杂性提供了新的精细理解。
The theory of the call-by-value-calculus relies on weak evaluation and closed terms, that are natural hypotheses in the study of programming languages. To model proof assistants, however, strong evaluation and open terms are required. Open call-by-value is the intermediate setting of weak evaluation with open terms, on top of which Grégoire and Leroy designed the abstract machine of Coq. This paper provides a theory of abstract machines for open call-by-value. The literature contains machines that are either simple but inefficient, as they have an exponential overhead, or efficient but heavy, as they rely on a labelling of environments and a technical optimization. We introduce a machine that is simple and efficient: it does not use labels and it implements open call-by-value within a bilinear overhead. Moreover, we provide a new fine understanding of how different optimizations impact on the complexity of the overhead.