レコードの拡張を許す対話的修正機構

森口 草介; 高橋 和子

論文・著書情報

タイトル

和文:	レコードの拡張を許す対話的修正機構
英文:

著者

和文:	森口草介, 高橋和子.
英文:	Sosuke Moriguchi, 高橋和子.

言語

Japanese

掲載誌/書名

和文:	コンピュータソフトウェア
英文:

巻, 号, ページ

Vol. 33 No. 2 pp. 2_125-2138

出版年月

2016年11月

出版者

和文:	日本ソフトウェア科学会
英文:

会議名称

和文:
英文:

開催地

和文:
英文:

アブストラクト

我々は対話的証明支援系Coqに対して，対話的修正機構という，既存の証明済みの体系に対する拡張をサポートする機構の提案を行った．提案した機構では，宣言した帰納型に対する新しい構成子の追加を可能としていた．しかし，この機構では既存の構成子や型，関数に対する新たなパラメータの追加は不可能であった．
本論文では，レコードに対して新たなフィールドを追加する手法と，その場合のCoqにおける型システムの制限について分析する．この手法は，レコードだけでなく，構築子や関数に対するパラメータの追加も可能とするが，その場合の問題点についても述べる．

Home

各種検索

サポート

T2R2について

関連リンク

論文・著書情報