定理証明支援系Coq を用いたプログラム運算

修士論文 定理証明支援系 Coq を用いた プログラム運算 48086225 橋本 英樹 指導教員 武市 正人 教授 2010 年 1 月 東京大学大学院情報理工学系研究科数理情報学専攻 Copyright c⃝ 2010, Hideki Hashimoto. 概要 プログラム運算は，プログラムを，その意味を変えない運算定理を用いて，より効率のよい プログラムに書き換えていくプログラミング手法である．運算前のプログラムが自明に正しい プログラムであれば，運算後のプログラムも意味を保存しているため検証が不要であり，正し く効率のよいプログラム開発に貢献すると期待される．しかし，支援システムがなければ正し い運算は難しいにもかかわらず，支援システム開発のコストの高さなどから，広く使われてい る支援システムは少ない． 本研究で，我々は定理証明支援系 Coq のライブラリによってプログラム運算を