講演抄録/キーワード |
講演名 |
2020-03-05 11:15
継続を基本とする言語CbCでのHoareLogicによる健全性の考察 ○外間政尊・河野真治(琉球大) SS2019-54 |
抄録 |
(和) |
CbC は継続を主とする言語上で、HoareLogicをベースとした検証を提案している。
OSなどの手続き型の記述に対しても有効なものを目指している。
Curry-Howard対応にもとづく証明支援系であるAgdaを用いて検証手法の健全性を示す手法について考察する。 |
(英) |
(Not available yet) |
キーワード |
(和) |
プログラミング言語 / CbC / GearsOS / Agda / 検証 / / / |
(英) |
/ / / / / / / |
文献情報 |
信学技報, vol. 119, no. 451, SS2019-54, pp. 79-85, 2020年3月. |
資料番号 |
SS2019-54 |
発行日 |
2020-02-26 (SS) |
ISSN |
Online edition: ISSN 2432-6380 |
著作権に ついて |
技術研究報告に掲載された論文の著作権は電子情報通信学会に帰属します.(許諾番号:10GA0019/12GB0052/13GB0056/17GB0034/18GB0034) |
PDFダウンロード |
SS2019-54 |