文章基本信息

标题：On proving syntactic properties of CPS programs
本地全文：下载
作者：Olivier Danvy ; Belmina Dzafic ; Frank Pfenning 等
期刊名称：BRICS Report Series
印刷版ISSN：0909-0878
出版年度：1999
卷号：6
期号：23
出版社：Aarhus University
摘要：Higher-order program transformations raise new challenges for proving properties of their output, since they resist traditional, first-order proof techniques. In this work, we consider (1) the "one-pass" continuation-passing style (CPS) transformation, which is second-order, and (2) the occurrences of parameters of continuations in its output. To this end, we specify the one-pass CPS transformation relationally and we use the proof technique of logical relations.