view document/report.txt @ 128:9ef69d114781

Add report.txt
author atton <atton@cr.ie.u-ryukyu.ac.jp>
date Sat, 18 Feb 2017 11:15:37 +0900
parents
children
line wrap: on
line source

学位(修士)の申請に対し,学位論文の審査及び最終試験を終了したので,下記のとおり報告します。

審査要旨(500字以内)



所属研究室で開発しているプログラミング言語 Continuation based C(CbC) に対して2種類の信頼性向上手法を提案していた。
一つはモデル検査的手法であり、総当たりで赤黒木の仕様を検証するメタ計算ライブラリを実装、評価していた。
もう片方は定理証明的な手法であり、CbC を Agda 上に定義して言語の形式的な定義を得ることで、CbCで記述されたプログラムの証明を可能にしていた。

予備審査において、証明手法に関する解説が不足しており、証明とプログラムの関係が不透明であることを指摘した。
最終試験時には修士論文上に指摘した部分の解説が追加されていた。

よってこの論文を修士の論文として適切であると認める。