Monae: Coqのためのモナディックエフェクトと等式推論

関数型言語プログラムではモナドを用いて副作用を表すことができます。このようなプログラムに対して等式推論を用いたプログラム検証の方式であるモナディック等式推論は、依存型に基づく定理証明支援系上で様々な試みがなされています。本研究はこの形式化を強化することを目的に、モナディック等式推論のためのCoqライブラリMonaeの改良にとり組みます。

研究室メンバーの斉藤が、産総研のAffeldt博士の指導の下でMonaeプロジェクトに参加しています。