Back to direct style. Danvy, O. In ESOP '92, of Lecture Notes in Computer Science, pages 130–150, 1992. Springer, Berlin, Heidelberg. Citation Key Alias: danvy1992b
Back to direct style [link]Paper  doi  abstract   bibtex   
While a great deal of attention has been devoted to transforming direct-style (DS) functional programs into continuation-passing style (CPS), to the best of our knowledge, the transformation of CPS programs into direct style has not been investigated. This paper describes the mapping of continuation-passing λ-terms to their applicative-order direct style counterpart. We set up foundations and outline applications of the direct style transformation.We derive the direct style transformer from a non-standard denotational semantics of the untyped λυ-calculus, that we prove congruent to the standard one.Under precise conditions (linear occurrences of continuation parameters and no first-class use of continuations due to control operators such as call/cc), we show the DS and the CPS transformations to be inverse.The direct style transformation can be used in partial evaluation, based on the fact that semantics-based program manipulation performs better when source programs are first transformed into CPS. As a result, specialized programs are expressed in CPS as well. The DS transformation maps them back to direct style.
@inproceedings{danvy_back_1992,
	series = {Lecture {Notes} in {Computer} {Science}},
	title = {Back to direct style},
	isbn = {978-3-540-46803-5},
	url = {http://link.springer.com/10.1007/3-540-55253-7_8},
	doi = {10.1007/3-540-55253-7_8},
	abstract = {While a great deal of attention has been devoted to transforming direct-style (DS) functional programs into continuation-passing style (CPS), to the best of our knowledge, the transformation of CPS programs into direct style has not been investigated. This paper describes the mapping of continuation-passing λ-terms to their applicative-order direct style counterpart. We set up foundations and outline applications of the direct style transformation.We derive the direct style transformer from a non-standard denotational semantics of the untyped λυ-calculus, that we prove congruent to the standard one.Under precise conditions (linear occurrences of continuation parameters and no first-class use of continuations due to control operators such as call/cc), we show the DS and the CPS transformations to be inverse.The direct style transformation can be used in partial evaluation, based on the fact that semantics-based program manipulation performs better when source programs are first transformed into CPS. As a result, specialized programs are expressed in CPS as well. The DS transformation maps them back to direct style.},
	language = {en},
	urldate = {2018-06-12},
	booktitle = {{ESOP} '92},
	publisher = {Springer, Berlin, Heidelberg},
	author = {Danvy, Olivier},
	year = {1992},
	note = {Citation Key Alias: danvy1992b},
	pages = {130--150}
}

Downloads: 0