文献

J-GLOBAL ID：202202272051150833   整理番号：22A0691444

骨格意味論のための認証抽象機械【JST・京大機械翻訳】

Certified abstract machines for skeletal semantics

著者 (3件)： Ambal Guillaume (University of Rennes, France) ,  Lenglet Sergueie (University of Lorraine, France) ,  Schmitt Alan (Inria, France)
資料名： ACM Proceedings  (ACM Proceedings)
号： CPP 2022  ページ： 55-67  発行年： 2022年 
JST資料番号： D0698C  資料種別： 会議録 (C)
記事区分： 原著論文  発行国： アメリカ合衆国 (USA)  言語： 英語 (EN)

抄録/ポイント： 骨格意味論はプログラミング言語の意味を記述するフレームワークである。骨格意味論で書かれた任意の言語に対する認証OCaml解釈者の自動生成を提案した。この目的のために,2つの新しい解釈,すなわち,非決定論的および決定論的抽象マシンの形で,骨格意味論の形式的意味を導入した。これらのマシンは,機能的対応を用いた骨格意味論の通常の大ステップ解釈から導出され,大ステップ評価者から抽象マシンへの標準変換である。これらの解釈はすべてCoq証明支援で定式化され,それらの健全性を証明した。最後に,CoqからOCamlへの抽出を用いて,認証された解釈者を得た。Please refer to this article’s citation page on the publisher website for specific rights information. Translated from English into Japanese by JST.【JST・京大機械翻訳】

シソーラス用語： *意味論 ,  言語 ,  プログラミング言語 ,  証明 ,  変換 ,  機能 ,  定式化 ,  *計算モデル ,  操作的意味論 ,  *認証 ,  健全性 ,  フレームワーク【ソフトウェア開発】
準シソーラス用語： *抽象機械 ,  自動生成 ,  決定論 , 【Automatic Indexing@JST】

著者キーワード (4件)： 抽象機械 ,  認証された解釈 ,  操作的意味論 ,  骨格意味論

分類 (2件)： 計算理論  (JB02000A) ,  言語プロセッサ  (JD03040F)

タイトルに関連する用語 (4件)： 骨格 ,  意味論 ,  認証 ,  抽象機械