\chapter{まとめ}

本研究では CodeGear、 DataGear を用いたプログラミング手法を使い、Agda で
Interface を用いたプログラムを実装し、証明を記述した。
これにより、 CbC で記述した時には細かく分かっていなかった Interface の型が明確になった。
また、 Hoare Logic を CodeGear 、 DataGear と対応させることで Hoare Logic ベース
で証明が進められると考えている。
今回の研究中に継続を利用することで得られた知見は、今後の研究で大いに役立つと
考える。

今後の課題としては、CbC 上での RedBlackTree の実装や、 Agda 上での RedBlackTree
の実装と証明がある。また、 CodeGear、DataGear をベースにした Hoare Logic を Agda で実
装する。
Agda 定義した Hoare Logic を使い、いくつかの証明を実際に記述し、書き方を確立するなどが考えられる。
他にも、タスクスケジューラの実装を Agda に移し、 SynchronizedQueue の同期、非同
期の検証などが考えられる。