A Higher-Order Colon Translation

Research output: Contribution to journal/Conference contribution in journal/Contribution to newspaperJournal articleResearch

  • Department of Computer Science
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.'' 10 years ago, Danvy and Filinski integrated administrative reductions in the CPS transformation, making it operate in one pass. The technique applies to other lambda-encodings (e.g., variants of CPS), but we do not see it used in practice--instead, Plotkin's colon translation appears to be favored. Therefore, in an attempt to link both techniques, we recast Plotkin's proof of Indifference and Simulation to the higher-order specification of the one-pass CPS transformation. To this end, we extend his colon translation from first order to higher order
Original languageEnglish
Book seriesB R I C S Report Series
IssueRS-00-33
Number of pages17
ISSN0909-0878
Publication statusPublished - 2000

See relations at Aarhus University Citationformats

ID: 36062714