23:59 | 1.Types and Programming Languages( http://www.cis.upenn.edu/~bcpierce/tapl/ )TAPLは現実 2.Advanced Topics in Types and Programming Languages( http://www.cis.upenn.edu/~bcpierce/attapl/resources.h 続きを読む
プログラマが読むべき10冊 - Yet Another RanhaCoq | 前からずっと取り組んでいた「Coqで単純型付きラムダ計算を証明してみよう」が一段落しました。 動機let多相の実装はしたから、次は証明だろ 最近、流行っているCoqを覚えたい 扱えるラムダ式型は、Bool型と関数型のみ。 Inductive type : Set := | BoolT : type | FunT : type -\u003e type -\u003e type. 式は、変数参照、真偽値、ラ 続きを読む
Coqでラムダ計算を証明してみた - みずぴー日記