構成的プログラミングと型理論

構成的プログラミングと型理論についてのコミュです。

構成的プログラミングの基礎　林 晋・小林 聡　共著
http://www2.odn.ne.jp/yuseisha/oyohoka/koseiteki-c.htm

Programming in Martin-Loef's Type Theory
http://www.cs.chalmers.se/Cs/Research/Logic/book/

１０年前の
http://www.jssst.or.jp/plan/type-const-tutorial.html
この講演を聴いたとか、ここいらの分野専攻していますとか、とりあえず(型理論or構成的プログラミング)本読んでみていますな方（自分）大歓迎です。
自己紹介とかは全然強制してないです。お気軽に参加ください。
トピは自由に立ててください。

ちなみに、管理人は何にもよくわかっていないです。

--検索用--
関数型言語 cvFL lzFL
Martin-Loef type theory
category theory 内包 外延
システム検証 spin NuSMV 仕様記述言語Promela
古典論理 型理論 継続 例外処理 並列プロセス計算
Curry-Howard Isomorphism