Lambda Mu Calculus and Duality: Call-by-Name and Call-by-Value
Lambda Mu Calculus and Duality: Call-by-Name and Call-by-Value
复制标题
Lambda Mu 演算和对偶性：按名称调用和按值调用
DOI：
--
复制
发表时间：
2005
期刊：
影响因子：
--
通讯作者：
J. Rocheteau
中科院分区：
文献类型：
--
作者：
J. Rocheteau
在Curry-Howard对应于经典逻辑的推广下，Gentzen的NK和LK系统分别可以看作Parigot的Lambda Mu演算和Curien-Herbelin的Lambda Bar Mu Mu Tidle演算的简单类型的语法导向系统。我们的目的是显示它们的计算等价性。我们定义这些演算之间的平移。我们证明了模拟定理的无向评价，以及呼叫的名称和呼叫的值的评价。
Under the extension of Curry-Howard's correspondence to classical logic, Gentzen's NK and LK systems can be seen as syntax-directed systems of simple types respectively for Parigot's Lambda Mu Calculus and Curien-Herbelin's Lambda Bar Mu Mu Tidle Calculus. We aim at showing their computational equivalence. We define translations between these calculi. We prove simulation theorems for an undirected evaluation as well as for call-by-name and call-by-value evaluations.