文献

J-GLOBAL ID：202002272914602367   整理番号：20A1034664

EMTST:Metaのエンジニアリング-セッションタイプの理論【JST・京大機械翻訳】

EMTST: Engineering the Meta-theory of Session Types

著者 (3件)： Castro David (Imperial College London, London, UK) ,  Ferreira Francisco (Imperial College London, London, UK) ,  Yoshida Nobuko (Imperial College London, London, UK)
資料名： Lecture Notes in Computer Science  (Lecture Notes in Computer Science)
巻： 12079  ページ： 278-285  発行年： 2020年 
JST資料番号： H0078D  ISSN： 0302-9743  資料種別： 会議録 (C)
記事区分： 原著論文  発行国： ドイツ (DEU)  言語： 英語 (EN)

抄録/ポイント： セッションタイプは構造化相互作用のための原理的プログラミング分野を提供する。それらは同時性のためのタイプシステムの広いスペクトルを表す。従って,それらのタイプの安全性は非常に重要である。EMTSTは,Coq証明支援におけるセッションタイプに関する定理の表現と検証を支援するツールである。本論文では,これらの証明書はしばしばtrickで,誤りが起こりやすい。証明支援において,それらは典型的に長く,証明するのが難しい。本研究では,証明支援におけるセッション型計算の理論を検証する助けとなるライブラリーを提案した。事例研究として,著者らは,最も使用されている二値セッション型システムの2つを研究した:[数式:原文を参照]-等価表現における最初のシステムを表現することの不可能性を示し,再訪問システムに対するタイプ保存を証明した。著者らは,Coq証明支援における著者らのツールを開発し,線形タイピング環境の取り扱いを単純化するために,結合剤と小規模反射に対して局所的に命名することを用いた。Copyright The Author(s) 2020 Translated from English into Japanese by JST.【JST・京大機械翻訳】

シソーラス用語： 相互作用 ,  *簡素化 ,  同時性 ,  スペクトル ,  計算理論 ,  線形性 ,  事例研究
準シソーラス用語： 証明書 ,  型システム , 【Automatic Indexing@JST】

著者キーワード (4件)： 並行性 ,  アシスタントの証明 ,  メタ理論 ,  セッション型

分類 (3件)： 計算理論  (JB02000A) ,  計算機システム開発  (JD02010R) ,  汎用プログラミング言語  (JD03051H)

タイトルに関連する用語 (4件)： エンジニアリング ,  セッション ,  タイプ ,  理論