Explicitly Typed lambda µ-Calculus for Polymorphism an Call-by-Value
Explicitly Typed lambda µ-Calculus for Polymorphism an Call-by-Value
复制标题
用于多态性和按值调用的显式类型 lambda µ 演算
DOI：
10.1007/3-540-48959-2_13
复制
发表时间：
1999
期刊：
影响因子：
--
通讯作者：
Ken
中科院分区：
文献类型：
--
作者：
Ken
我们引入了一个显式类型的按值调用的λμ演算作为二阶Church风格的简写。我们的动机来自于这样的观察：在Curry风格的多态演算中，控制操作符（如callcc或μ-operator）通常不能处理控制操作符左侧的项。在延续语义的基础上，我们还讨论了经典系统中的值概念，并提出了一种扩展的值形式。证明了CPS-平移关于λ2（二阶λ-演算）是合理的.接下来，我们给出了一个带有μ算子的显式和隐式Damas-Milner系统.最后，我们给出了与标准ML加callcc的简要比较，并讨论了一种自然的方法来避免ML与callcc的不合理性。
We introduce an explicitly typed λμ-calculus of call-by-value as a short-hand for the 2nd order Church-style. Our motivation comes from the observation that in Curry-style polymorphic calculi, control operators such as callcc orμ-operators cannot, in general, treat the terms placed on the control operator’s left. Following the continuation semantics, we also discuss the notion of values in classical system, and propose an extended form of values. It is shown that the CPS-translation is sound with respect to λ2 (2nd order λ-calculus). Next, we provide an explicitly and an implicitly typed Damas-Milner systems withμ-operators. Finally, we give a brief comparison with standard ML plus callcc, and discuss a natural way to avoid the unsoundness of ML with callcc.