Monads with Predicate Liftings in Coq
Switch branches/tags
Nothing to show
Clone or download
Fetching latest commit…
Cannot retrieve the latest commit at this time.
Permalink
Failed to load latest commit information.
src
.gitignore
README.md
mpl_scratch.v

README.md

Monads with Predicate Liftings in Coq

モナドを用いて記述されたプログラムについての述語を自然な形で記述するための道具 となるであろう Monads with Predicate LiftingsのCoqにおける実装に関するものを扱います.

資料

解説

  • 分割アンド整理中(06/23) ホーアトリプルを簡単に書けるという部分だけでもライブラリ化できるなぁと思ったので,その作業中です.

  • 以前の 現時点(05/26)では,ソースコードの公開自体が目的の一つです. 自分のスケジュールと照らし合わせ,なるべく早く(7月くらいまでには)解説をつけていきたいと思います.

現時点での知識不足を埋める作業や新しい情報の出現へのフォローも踏まえて,全体的な内容のブラッシュアップも図っていきたいと思います.

参考文献

色々とありますので,おいおい追記していきます.

  • B. Jacobs, Predicate Logic for Functors and Monads, 2010. URL

その他

これは僕の修論のテーマでもありました. そして今でも自分で時間を見つけながら研究を進めています.