研究者情報 | 神奈川大学

タケヤマ　マコト Takeyama Makoto 武山　誠所属神奈川大学理学部情報科学科神奈川大学大学院理学研究科理学専攻（情報科学領域）職種教授
言語種別	英語
発行・発表の年月	1999
形態種別	学術雑誌
査読	査読あり
標題	Syntactic Control of Interference Revisited
執筆形態	共著
掲載誌名	Theoretical Computer Science,vol228
掲載区分	国外
巻・号・頁	pp.211-252
著者・共著者	P.W. O'Hearn, A.J. Power, M. Takeyama, R.D. Tennent
概要	In "syntactic control of interference" (POPL, 1978), J.C. Reynolds proposes three design principles intended to constrain the scope of imperative state effects in Algol-like languages. ... Reynolds points out that the "obvious" syntax for interference control has the unfortunate property that beta-reductions do not always preserve typings. Reynolds has subsequently presented a solution to this problem (ICALP, 1989), but it is fairly complicated and requires intersection types in the type system. Here, we present a much simpler solution which does not require intersection types. We first describe a new type system inspired in part by linear logic and verify that reductions preserve typings. We then define a class of "bireflective" models, which provide a categorical analysis of structure underlying the new typing rules; ... Finally, we describe a concrete model for an illustrative programming language based on the new type system; ...