Actris2.0:分離論理における非同期セッション型ベース推論【JST・京大機械翻訳】

Hinrichsen Jonas Kastberg; Bengtson Jesper; Krebbers Robbert

プレプリント

J-GLOBAL ID：202202208844160555 整理番号：21P0057520

Actris2.0:分離論理における非同期セッション型ベース推論【JST・京大機械翻訳】

Actris 2.0: Asynchronous Session-Type Based Reasoning in Separation Logic

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

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

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

※このプレプリント論文は学術誌に掲載済みです。なお、学術誌掲載の際には一部内容が変更されている可能性があります。

メッセージ通過は同時プログラムを実行するための有用な抽象である。しかしながら,実世界システムでは,高次関数,可変状態,共有メモリ同時性,およびロックのような,他のプログラミングや同時性パラダイムとしばしば結合された。Actris:前述の特徴の組み合わせを用いるプログラムの機能的正当性を証明するための論理を示した。Actrisは,現代の同時分離論理の電力を,他の同時性パラダイムの存在におけるメッセージパッシングに関する推論のために,セッションタイプに基づく最初のクラスプロトコル機構と結びつける。Actrisは,簡潔な仕様を用いて,チャネルベースマージソート,チャネルベース負荷バランスマッパー,およびマップ縮小モデルの変種を含む,多様な例の機能的正当性を証明することにより,抽象化の適切なレベルを提供することを示した。Actrisは既に会議論文(POPL’20)で提示されたが,本論文は事前のプレゼンテーションを著しく拡大した。さらに,それは,セッション型サブタイピングに基づくサブプロトコールの概念で,ActrisをActris2.0に拡張して,チャネルエンドポイントを構成するとき,付加的柔軟性を許容し,そして,Actrisにおけるメッセージパッシングの非同期意味論を完全に利用した。Irisフレームワークにおけるプロトコル機構のモデルを用いて,Actris2.0の健全性を証明した。Coq証明支援において,論文のすべての例と同様に,カスタム戦術と共に,Actrisの理論を機械化した。【JST・京大機械翻訳】

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

人工知能 , 数理言語学 , 計算機システム開発

, , ,

前のページに戻る