%0 Journal Article
%T Two Values Passing CPS Transformation for Call-by-Name Calculus with Constants<br>传名调用演算的二值传递CPS变换
%A YU Gang
%A LIU Xin-Xin
%A <br>喻 钢
%A 柳欣欣
%J 软件学报
%D 2008
%I 
%X In this paper, a new CPS (continuation-passing-style) transformation for Plotkin's call-by-name ( calculus with constants is proposed. It is based on evaluation contexts transformation and the features that two values, instead of one, are passed to the continuation every time. With encodings, a CPS language is introduced. Then, Plotkin's simulation theorem is proved by establishing 1-to-1 correspondence between the source language and CPS language. Compared with Plotkin's work, a reduction closed CPS language is defined in which all continuations are explicitly expressed as functional encodings and it is simpler to prove both the soundness and completeness directions of simulation theorem.
%K programming calculi
%K formal semantics
%K call-by-name
%K CPS(continuation-passing-style)
%K reduction<br>程序演算
%K 形式语义
%K 传名调用
%K CPS(continuation-passing-style)
%K 归约
%U http://www.alljournals.cn/get_abstract_url.aspx?pcid=5B3AB970F71A803DEACDC0559115BFCF0A068CD97DD29835&cid=8240383F08CE46C8B05036380D75B607&jid=7735F413D429542E610B3D6AC0D5EC59&aid=7ABB24DFB662E64278A41230DC9AACDC&yid=67289AFF6305E306&vid=2A8D03AD8076A2E3&iid=F3090AE9B60B7ED1&sid=BABEC404D527B47C&eid=71E51BD3D819EC5A&journal_id=1000-9825&journal_name=软件学报&referenced_num=0&reference_num=15