A Higher-Order Colon Translation

Olivier Danvy, Lasse Reichstein Nielsen

    Research output: Contribution to book/anthology/report/proceedingArticle in proceedingsResearchpeer-review


    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
    Title of host publicationFunctional and Logic Programming : 5th International Symposium, FLOPS 2001 Tokyo, Japan, March 7–9, 2001 Proceedings
    EditorsHerbert Kuchen, Kazunori Ueda
    Number of pages14
    Publication date2001
    Publication statusPublished - 2001
    Event5th International Symposium on Functional and Logic Programming (FLOPS 2001) - Tokyo, Japan
    Duration: 7 Mar 20019 Mar 2001
    Conference number: 5


    Conference5th International Symposium on Functional and Logic Programming (FLOPS 2001)
    SeriesLecture Notes in Computer Science


    • Call by name
    • Call by value
    • lambda-calculus
    • continuation-passing style(CPS)
    • CPS transformation
    • administrative reduction
    • one-pass CPS transformation
    • Indifference Simulation


    Dive into the research topics of 'A Higher-Order Colon Translation'. Together they form a unique fingerprint.

    Cite this