A Higher-Order Colon Translation

Abstract

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.