文章基本信息

标题：A Higher-Order Colon Translation
本地全文：下载
作者：Olivier Danvy ; Lasse R. Nielsen
期刊名称：BRICS Report Series
印刷版ISSN：0909-0878
出版年度：2000
卷号：7
期号：33
出版社：Aarhus University
摘要：A lambda-encoding such as the CPS transformation gives rise to administrative redexes. In his seminal article "Call-by-name, call-by-value and the lambda-calculus", 25 years ago, Plotkin tackled administrative reductions using a so-called colon translation. In "Representing control, a study of the CPS transformation", 15 years later, Danvy and Filinski integrated administrative reductions in the CPS transformation, making it operate in one pass. This one-pass transformation is higher-order, and can be used for other lambda-encodings, but we do not see its associated proof technique used in practice - instead, Plotkin's colon translation appears to be favored. Therefore, in an attempt to link the higher-order transformation and Plotkin's proof technique, we recast Plotkin's proof of Indifference and Simulation in a higher-order setting. To this end, we extend the colon translation from first order to higher order. Keywords: Call by name, call by value, lambda-calculus, continuation-passing style (CPS), CPS transformation, administrative reductions, colon translation, one- pass CPS transformation, Indifference, Simulation.