A Higher-Order Colon Translation

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

  • 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
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 year2001
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

    Research areas

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

See relations at Aarhus University Citationformats

ID: 281570