研究者情報 | 神奈川大学

キノシタ　ヨシキ Kinoshita Yoshiki 木下　佳樹所属神奈川大学情報学部計算機科学科神奈川大学大学院理学研究科理学専攻（情報科学領域）職種教授
言語種別	日本語
発行・発表の年月	1997/09
形態種別	学術雑誌
査読	査読あり
標題	An axiomatic approach to binary logical relations with applications to data refinement
執筆形態	共著
掲載誌名	Lecture Notes in Computer Science (Springer-Verlag)
巻・号・頁	1281,191-212頁
著者・共著者	Yoshiki Kinoshita, Peter W.O'Hearn, John A.Power, Makoto Takeyama and Robert D.Tennent
概要	We introduce an axiomatic approach to logical relations and data refinement. We consider a programming language and the monad on the category of small categories generated by it. We identify abstract data types for the language with sketches for the associated monad, and define an axiomatic notion of "relation" between models of such a sketch in a semantic category. We then prove three results: (i) such models lift to the whole language together with the sketch; (ii) any such relation satisfies a soundness condition; and (iii) such relations compose. We do this for both equality of data representations and for an ordered version. Finally, we compare our formulation of data refinement with that of Hoare.