文献

J-GLOBAL ID：201202245140471160   整理番号：12A0581826

双模倣性とKripke論理関係の結婚

The Marriage of Bisimulations and Kripke Logical Relations

著者 (4件)： HUR Chung-Kil (Max Planck Inst. Software Systems (MPI-SWS)) ,  DREYER Derek (Max Planck Inst. Software Systems (MPI-SWS)) ,  NEIS Georg (Max Planck Inst. Software Systems (MPI-SWS)) ,  VAFEIADIS Viktor (Max Planck Inst. Software Systems (MPI-SWS))
資料名： ACM SIGPLAN Notices (Association for Computing Machinery. Special Interest Group on Programming Languages)  (ACM SIGPLAN Notices (Association for Computing Machinery. Special Interest Group on Programming Languages))
巻： 47  号： 1  ページ： 59-72  発行年： 2012年01月 
JST資料番号： D0915A  ISSN： 0362-1340  資料種別： 逐次刊行物 (A)
記事区分： 原著論文  発行国： アメリカ合衆国 (USA)  言語： 英語 (EN)

抄録/ポイント： プログラミング言語意味論における壮大な挑戦課題の1つはプログラムの観察上の等価性についての推論用のスケーラブルな技法を検出する事である。本論文において,筆者らは関係遷移システム(RTS)と呼ばれるML類似プログラムの等価性提供用の新規の手法を開発した。本手法ではKripke論理関係,環境的双模倣性及び正規形式双模倣性の幾つかの最良の面を組み合わせた。その祖先の補足的利点の有用な合成の提供に加えて,本手法が異なった言語間の等価性についての推論の方法として有望である事を,1)言語間推論を妨げる”構文”装置の回避,2)RTS等価性証明の遷移的組立て可能性のおかげで示した。筆者らはここで単純な設定において遷移性の証明を簡潔に概観し,来たるべき論文中で完全な遷移性結果を報告する予定である。

シソーラス用語： *論理 ,  *遷移システム ,  文脈 ,  等価性 ,  推論 ,  状態 ,  抽象 ,  型
準シソーラス用語： *Kripkeモデル ,  ML【プログラミング言語】 ,  *関係 ,  双模倣性

分類 (1件)： 応用プログラミング言語  (JD03052Y)

タイトルに関連する用語 (3件)： 模倣 ,  論理 ,  結婚