文献

J-GLOBAL ID：201802248296811932   整理番号：18A1484212

Coqにおける精密化計算の埋め込み【JST・京大機械翻訳】

Embedding the refinement calculus in Coq

著者 (2件)： Alpuim Joao (University of Hong Kong, Hong Kong) ,  Swierstra Wouter (Universiteit Utrecht, Netherlands)
資料名： Science of Computer Programming  (Science of Computer Programming)
巻： 164  ページ： 37-48  発行年： 2018年 
JST資料番号： H0806A  ISSN： 0167-6423  CODEN： SCPGD4  資料種別： 逐次刊行物 (A)
記事区分： 原著論文  発行国： オランダ (NLD)  言語： 英語 (EN)

抄録/ポイント： 精密化計算とタイプ理論は,プログラムの仕様と検証をサポートする両方のフレームワークである。本論文では,相互作用定理証明器Coqにおける精密化計算の埋め込みを示し,2つの間の関係を明らかにした。結果として,Coqにおいて精密化計算を実行することができ,それらの仕様から形式的に検証されたプログラムの相互作用計算を可能にした。Copyright 2018 Elsevier B.V., Amsterdam. All rights reserved. Translated from English into Japanese by JST.【JST・京大機械翻訳】

シソーラス用語： *精密化 ,  型理論 ,  定理証明 ,  相互作用

著者キーワード (5件)： 精密化計算 ,  Coq ,  述語変圧器 ,  自由モナド ,  依存型

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

タイトルに関連する用語 (3件)： 精密化 ,  計算 ,  埋め込み