Polymorphic computation systems: Theory and practice of confluence with call-by-value
Polymorphic computation systems: Theory and practice of confluence with call-by-value
复制标题
多态计算系统：按值调用融合的理论与实践
DOI：
10.1016/j.scico.2019.102322
复制
发表时间：
2020
影响因子：
1.3
通讯作者：
Kentaro Kikuchi
中科院分区：
文献类型：
--
作者：
Makoto Hamana;Tatsuya Abe;Kentaro Kikuchi
我们提出了一个新的框架，多态计算规则，可以容纳值和非值之间的区别。它适用于分析程序设计语言的基本演算。我们开发了一个类型推理算法和新的标准来检查合流性质。这些技术，然后在我们的自动汇流检查工具PolySOL中实现。它的有效性是通过检查各种演算，包括按需调用的计算演算，莫吉的计算演算，和斜monoidal类别。
We present a new framework of polymorphic computation rules that can accommodate a distinction between values and non-values. It is suitable for analysing fundamental calculi of programming languages. We develop a type inference algorithm and new criteria to check the confluence property. These techniques are then implemented in our automated confluence checking tool PolySOL. Its effectiveness is demonstrated through examination of various calculi, including the call-by-need lambda-calculus, Moggi's computational lambda-calculus, and skew-monoidal categories.