文献

J-GLOBAL ID：201902260119872300   整理番号：19A2761794

相互再帰によるコール・バイ・ニーズとコール・バイ・名前評価の形式的検証【JST・京大機械翻訳】

Formal Verifications of Call-by-Need and Call-by-Name Evaluations with Mutual Recursion

著者 (2件)： Mizuno Masayuki (Graduate School of Information Sciences, Tohoku University, Sendai, Japan) ,  Sumii Eijiro (Graduate School of Information Sciences, Tohoku University, Sendai, Japan)
資料名： Lecture Notes in Computer Science  (Lecture Notes in Computer Science)
巻： 11893  ページ： 181-201  発行年： 2019年 
JST資料番号： H0078D  ISSN： 0302-9743  資料種別： 会議録 (C)
記事区分： 原著論文  発行国： ドイツ (DEU)  言語： 英語 (EN)

抄録/ポイント： 著者らは,相互に再帰的な結合を有する[数式:原文を参照]-計算のコール毎の評価と(様々な定義の)呼毎の評価の間の対応のCoq証明支援において,新しい証明を提示した。非厳密言語に対しては,高水準仕様と典型的実装の間の等価性が基本的な関心事である。特定のマイルストンは,最近,Breitner(2018)によってIsabell/HOLで定式化された,呼毎の表示意味論に関して,その妥当性の証明と必要性評価のLaunchburyの自然意味論である。Ariolaらによる等化理論は,必要性の他のよく知られた形式化である。相互再帰はその理論にとって特に挑戦的である。すなわち,縮小は依存性の横断によって複雑化される(必要性)関係である。そして,呼ばれると呼ばれない減少の対応は,グラフや無限木のような洗練された構造を必要とする。本論文では,(有限)項と演算意味論に基づく簡単な証明を与えた。これらは,証明書(Coq)を証明するために扱いやすい。著者らの証明は以下のように要約できる。(1)著者らは,2つのヒープ間の十分に(しかしあまりにも)一般的な対応を定義しない,Launchburyのコール毎の意味論とheapベースのコール毎の自然意味論の間の等価性を証明し,また,著者らは,3つの型のcal意味論の間の対応を示した。(1)(1)で用いた自然意味;(ii)情報的にLaunchburyの意味論に対応する閉鎖ベースの自然意味論;(iii)従来の置換ベースの意味論。Copyright 2019 Springer Nature Switzerland AG Translated from English into Japanese by JST.【JST・京大機械翻訳】

シソーラス用語： *意味論 ,  ヒープ ,  言語 ,  定式化 ,  等価性 ,  演算 ,  等化
準シソーラス用語： 証明書 ,  Ariola ,  形式的検証 , 【Automatic Indexing@JST】

分類 (1件)： 人工知能  (JE08000Z)

タイトルに関連する用語 (6件)： コール ,  バイ ,  ニーズ ,  名前 ,  評価 ,  形式的検証