文章基本信息

标题：A First-Order One-Pass CPS Transformation
本地全文：下载
作者：Olivier Danvy ; Lasse R. Nielsen
期刊名称：BRICS Report Series
印刷版ISSN：0909-0878
出版年度：2001
卷号：8
期号：49
出版社：Aarhus University
摘要：We present a new transformation of call-by-value lambda-terms into continuation-passing style (CPS). This transformation operates in one pass and is both compositional and first-order. Because it operates in one pass, it directly yields compact CPS programs that are comparable to what one would write by hand. Because it is compositional, it allows proofs by structural induction. Because it is first-order, reasoning about it does not require the use of a logical relation. This new CPS transformation connects two separate lines of research. It has already been used to state a new and simpler correctness proof of a direct-style transformation, and to develop a new and simpler CPS transformation of control-flow information.