# HG changeset patch # User atton # Date 1487384137 -32400 # Node ID 9ef69d1147813f682532322e4aa9572ed99d4e0c # Parent 7903c02fe6868710de60687c65122e67602e6360 Add report.txt diff -r 7903c02fe686 -r 9ef69d114781 document/report.txt --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/document/report.txt Sat Feb 18 11:15:37 2017 +0900 @@ -0,0 +1,14 @@ +学位(修士)の申請に対し,学位論文の審査及び最終試験を終了したので,下記のとおり報告します。 + +審査要旨(500字以内) + + + +所属研究室で開発しているプログラミング言語 Continuation based C(CbC) に対して2種類の信頼性向上手法を提案していた。 +一つはモデル検査的手法であり、総当たりで赤黒木の仕様を検証するメタ計算ライブラリを実装、評価していた。 +もう片方は定理証明的な手法であり、CbC を Agda 上に定義して言語の形式的な定義を得ることで、CbCで記述されたプログラムの証明を可能にしていた。 + +予備審査において、証明手法に関する解説が不足しており、証明とプログラムの関係が不透明であることを指摘した。 +最終試験時には修士論文上に指摘した部分の解説が追加されていた。 + +よってこの論文を修士の論文として適切であると認める。