@article{oai:ipsj.ixsq.nii.ac.jp:00096955,
 author = {廣田, 知子 and 浅井, 健一 and Noriko, Hirota and Kenichi, Asai},
 issue = {4},
 journal = {情報処理学会論文誌プログラミング（PRO）},
 month = {Dec},
 note = {Danvyにより提案された型主導部分評価器（TDPE）は，与えられた項を正規形に評価する関数であり，Filinskiによってcall-by-nameおよびcall-by-valueの単純型付きλ計算におけるTDPEの正当性が示されている．一方，Tsushimaらは，限定継続命令shift/reset付きに拡張されたcall-by-valueのλ計算に対するTDPEをshift/resetを使って実装している．しかし，その背景にある理論については明らかになっておらず，直感的な説明と実装が与えられているのみであった．本論文では，Tsushimaらによって提案された直接形式のshift/reset付きTDPEを継続渡し形式のshift/reset付きTDPEに変換し，それがKripkeモデルの推論規則に対するcompletenessの証明と対応することを示す．このKripkeモデルの特徴は，構成要素である二項関係が継続渡し形式で定義される点にある．Curry Howard同型の観点において，このKripkeモデルに対するcompletenessの性質とTDPEが対応関係にあるため，completenessの定理を定理証明系Coqで定式化することにより，TDPEプログラムを抽出することができる．得られたプログラムは，継続渡し形式のshift/reset付きTDPEと同じ構造をしていることが見て取れる．, Danvy proposed the type-directed partial evaluator (TDPE for short) that reduces an input term to a normal form. The correctness properties of both call-by-name TDPE and call-by-value TDPE for simply-typed lambda calculus have been proved by Filinski. Subsequently, Tsushima et al. showed a TDPE for the call-by-value lambda calculus with delimited control operators, shift and reset, implemented in terms of shift/reset. However, its underlying theory is not given except for intuitive explanation and implementation. The aim of this paper is to transform the above direct-style definition of TDPE to continuation-passing style (CPS) and to show that this CPS TDPE corresponds to the completeness property of a Kripke model. The binary relation of the Kripke model is defined in a CPS manner. The model is then shown to be complete with respect to normal form construction. Since the completeness of the Kripke model exactly corresponds to the TDPE via Curry Howard isomorphism, we can extract TDPE from the proof of completeness. We have formalized the development in the proof assistant Coq. We observe that the obtained TDPE holds the same structure as the CPS TDPE for shift/reset.},
 pages = {50--64},
 title = {限定継続命令shift/reset付き型主導部分評価器の抽出},
 volume = {6},
 year = {2013}
}