文献

J-GLOBAL ID：201902228262284381   整理番号：19A1540175

有効な正規形バイシミュレーション【JST・京大機械翻訳】

Effectful Normal Form Bisimulation

著者 (4件)： Dal Lago Ugo (University of Bologna, Bologna, Italy) ,  Dal Lago Ugo (Inria Sophia Antipolis, Sophia Antipolis Cedex, France) ,  Gavazzo Francesco (University of Bologna, Bologna, Italy) ,  Gavazzo Francesco (Inria Sophia Antipolis, Sophia Antipolis Cedex, France)
資料名： Lecture Notes in Computer Science  (Lecture Notes in Computer Science)
巻： 11423  ページ： 263-292  発行年： 2019年 
JST資料番号： H0078D  ISSN： 0302-9743  資料種別： 会議録 (C)
記事区分： 原著論文  発行国： ドイツ (DEU)  言語： 英語 (EN)

抄録/ポイント： オープンバイシミュレーションとしても知られている正規形バイシミュレーションは,プログラムがそれらの基本的に無限の木状正規形,すなわちBohmまたはLevy-Longo木において見ることにより比較される高次プログラム等価性のための共帰納的手法である。この手法は,[数式:原文を参照]-計算とそれらの意味論に関するメタ定理を証明するだけでなく,用語の具体的な例を見るときにも有用であることが示されている。本論文では,代数的効果,la Plotkinおよび電力を計算するために,正規形バイシミュレーションを一般化する方法があることを示した。筆者らは,効果的な応用的双類似性を保証することが既に示されているモナドとリレータに関するいくつかの穏やかな条件は,有効な正規形双類似性と呼ぶ双類似性の得られた概念が一致関係であり,文脈的等価性に対して音であることを証明するのに十分であることを示した。さらに,応用的双類似性とは対照的に,正規形式双類似性は,双シミュレーション証明法の強化を可能にし,したがって,効果的プログラミング言語のための強力な推論原理を証明した。Copyright 2019 The Author(s) Translated from English into Japanese by JST.【JST・京大機械翻訳】

シソーラス用語： 等価性 ,  プログラミング言語 ,  音響 ,  電力 ,  意味論 ,  代数学 ,  *正準形式 ,  類似性
準シソーラス用語： モナド ,  *バイシミュレーション , 【Automatic Indexing@JST】

分類 (2件)： 図形・画像処理一般  (JE04010I) ,  人工知能  (JE08000Z)

タイトルに関連する用語 (1件)： バイシミュレーション