文献

J-GLOBAL ID：202002230710931629   整理番号：20A1865068

ReLoC 細粒並行性のための機械化関係論理【JST・京大機械翻訳】

ReLoC A Mechanised Relational Logic for Fine-Grained Concurrency

著者 (3件)： Frumin Dan (Radboud University) ,  Krebbers Robbert (Delft University of Technology) ,  Birkedal Lars (Aarhus University)
資料名： ACM Proceedings  (ACM Proceedings)
号： LICS ’18  ページ： 442-451  発行年： 2018年 
JST資料番号： D0698C  資料種別： 会議録 (C)
記事区分： 原著論文  発行国： アメリカ合衆国 (USA)  言語： 英語 (EN)

抄録/ポイント： ReLoC:高次状態,細粒同時性,多型および再帰型を持つ言語におけるプログラムの精密化を証明するための論理を示した。この論理のコアは判断e<e’:τであり,プログラムはタイプτでプログラムeを精密化する。高次状態および同時性を有する言語の精密化に関する以前の研究とは対照的に,ReLoCはこの判断を操作するためのタイプおよび構造指向ルールを提供するが,以前に,そのような証明は,モデルにおけるその定義への判断を展開することによって行われた。これらのより抽象的な証明規則は,精密化証明を実行するのに簡単である。さらに,論理的に原子関係仕様を導入する:時間において単一瞬間で効果を取る化合物表現のための関係仕様の新しいアプローチ。ReLoCにおけるそのような関係仕様を形式化し,証明する方法を示し,よりモジュール的な証明を可能にした。ReLoCは表現的同時分離論理Irisのトップに構築され,不変やゴースト状態のようなIrisの特徴を活用できる。Coqにおける著者らの論理の機械化を提供し,それは,健全性の証明だけでなく,インタラクティブに精密化証明を実行するための戦術も含めた。これらの戦術を用いて,いくつかの事例を機械化し,論理の実用性とモジュール性を示した。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】

著者キーワード (5件)： 虹彩 ,  分離論理 ,  原子性 ,  細粒度 ,  論理関係

分類 (2件)： 汎用プログラミング言語  (JD03051H) ,  数理言語学  (JB05000V)

タイトルに関連する用語 (4件)： 細粒 ,  並行 ,  機械化 ,  論理