@article{oai:ipsj.ixsq.nii.ac.jp:00016625,
 author = {清水, 亮 and 西崎, 真也 and Ryo, Shimizu and Shin-ya, Nishizaki},
 issue = {SIG6(PRO25)},
 journal = {情報処理学会論文誌プログラミング（PRO）},
 month = {Apr},
 note = {多相環境計算は，環境をファーストクラスオブジェクトとして扱うことができるλ 計算に，多相型体系を導入したものである．これまでに，ML 多相型体系を持つ環境計算とその型推論アルゴリズムは提案し，その主部簡約定理を得ていたが，強正規化可能性定理はまだ得ていなかった．本論文ではML 多相型体系を包含する，2 階型体系を提案し，その強正規化可能性定理を証明する．この性質は，多相環境計算から多相λ 計算（2 階型付λ 計算）への変換をもちいて，多相環境計算の強正規化可能性を多相λ 計算の強正規化可能性に帰着することによって得られる．, Polymorphic environment calculus is a polymorphic lambda calculus with first-class environments. We proposed environment calculus with ML-polymorphic type system and its type inference algorithm and proved principal type theorem with respect to the type system. In this paper, we propose second-order type system for the environment calculs, which includes the ML-polymorphic type system and prove strong normalization theorem with respect to the second-order type system. The theorem is proved by using transformation of the environment calculus to the polymorphic lambda calculus.},
 pages = {35--46},
 title = {多相環境計算における強正規化可能性},
 volume = {46},
 year = {2005}
}