スマート契約のための翻訳認証【JST・京大機械翻訳】

Krijnen Jacco O. G.; Chakravarty Manuel M. T.; Keller Gabriele; Swierstra Wouter

プレプリント

J-GLOBAL ID：202202200313280920 整理番号：22P0027156

スマート契約のための翻訳認証【JST・京大機械翻訳】

Translation Certification for Smart Contracts

出版者サイト {{ this.onShowPLink() }} 複写サービスで全文入手
高度な検索・分析はJDreamⅢで

この文献はプレプリントです。プレプリントについてはこちらをご確認ください。

著者 (4件)： , , ,
資料名：
発行年： 2022年01月13日プレプリントサーバーでの情報更新日： 2022年02月22日
JST資料番号： O7000B 資料種別：プレプリント
記事区分：プレプリント発行国：アメリカ合衆国 (USA) 言語：英語 (EN)

コンパイラ正当性は古い問題であるが,ブロックチェーン上のスマート契約の出現により,問題は新しい光でそれ自身を示す。スマート契約は,広告環境においてしばしば高い財務価値である資産を制御するソフトウェアの自給部品であり,また,ブロックチェーンに一旦参加すると,それらはもはや変更できない。スマート契約は,高レベル契約言語で典型的に開発され,ブロックチェーンに従う前に低レベル仮想マシンコードにコンパイルされる。スマート契約ユーザに対して,ブロックチェーン上の低レベル符号の与えられた部分を信頼するために,それらは(a)それらがマッチングソースコードの所有にあること,および(b)コンパイラがソースコードの意味論を忠実に翻訳するということを確信しなければならない。コンパイラ正当性に対する古典的アプローチは,第2のポイントに取り組む。また,翻訳認証は,最初に対処する。機能的スマート契約言語のためにCoqに実装された新しい翻訳認証フレームワークの証明アーキテクチャについて述べた。モジュール証明手法を容易にし,進化コンパイラ実装の面でロバストである翻訳関係のシーケンスとして編集パイプラインをモデル化できることを示した。【JST・京大機械翻訳】

, , , , , , , , , , ,
, , , , 【Automatic Indexing@JST】

言語プロセッサ , 応用プログラミング言語 , 電話・データ通信・交換一般

, ,

前のページに戻る