\chapter{今後の課題}

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

今後の課題は、CodeGear、DataGear をベースにした Hoare Logic を Agda で実装する。
また、その Hoare Logic を使い、いくつかの証明を実際に記述する。