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

摘要

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