@misc{oai:uec.repo.nii.ac.jp:00008466,
 author = {木下, 大輔},
 month = {2017-03-13},
 note = {2016, プログラムの任意の性質を保証し，バグのないプログラムを開発するために，Coqなどの証明支援系と呼ばれるソフトウェアを用いる方法がある．Coqを用いて性質を保証したプログラムを開発する方法には，2通りの方法がある．1つ目はCoq上にプログラムを直接記述し，証明を行い，他言語へ変換する方法．2つ目は他言語で記述されたプログラムをCoqプログラムへ変換し，証明を行う方法である．しかし，どちらの方法であっても単方向の変換のみ行うため，前者の方法では他言語を直接変更できないため仕様が決定できず，後者の方法では証明を行いやすいようにCoq上でプログラムへ変更を加えることができない，という問題点がある．
　本研究では，この問題を解決するため，OCamlプログラムとCoqプログラムの双方向の変換を可能とするシステムを提案する．これにより，OCamlプログラムの変更をCoqプログラムへ反映することで，OCaml側で仕様が決定できると同時に，証明を行いやすくするためにCoq側でプログラムに加えた変更を，OCamlプログラムへ反映することができる．さらに，変更前のCoqプログラムを利用し，差分の小さいCoqプログラムを生成することで，以前の証明を部分的に再利用できることが期待される．また，OCamlのListモジュールを本システムで変換することで，Coqで扱うことのできる構文に変換されるOCamlプログラムに対し，対応していることを示した．},
 title = {部分的なプログラムの変更を考慮した証明支援},
 year = {},
 yomi = {キノシタ, ダイスケ}
}