ハシモト　マサトモ   Masatomo Hashimoto   橋本　政朋    所属   千葉工業大学  人工知能・ソフトウェア技術研究センター 人工知能・ソフトウェア技術研究センター    職種   主席研究員
言語種別	英語
発行・発表の年月	2001/09
形態種別	学術雑誌
査読	査読あり
標題	A typed context calculus
執筆形態	共著
掲載誌名	Theoretical Computer Science
掲載区分	国外
出版社・発行元	Elsevier
巻・号・頁	266(1-2),pp.249-272
著者・共著者	Masatomo Hashimoto, Atsushi Ohori
概要	This paper develops a typed calculus for contexts i.e., lambda terms with "holes". In addition to ordinary lambda terms, the calculus contains labeled holes, hole abstraction and context application for manipulating first-class contexts. The primary operation for contexts is hole-filling, which captures free variables. This operation conflicts with substitution of the lambda calculus, and a straightforward mixture of the two results in an inconsistent system. We solve this problem by defining a type system that precisely specifies the variable-capturing nature of contexts and that keeps track of bound variable renaming. These mechanisms enable us to define a reduction system that properly integrates beta-reduction and hole-filling. The resulting calculus is Church-Rosser and the type system has the subject reduction property. We believe that the context calculus will serve as a basis for developing a programming language with advanced features that call for manipulation of open terms.
DOI	10.1016/S0304-3975(00)00174-2
researchmap用URL	https://www.sciencedirect.com/science/article/pii/S0304397500001742