2008/07/02

Church Encoding!

Max 講了新內容 second-order intuitionistic propositional logic。雖然沒講很多,可是最後一張投影片馬上吸引我的目光:

稍微多看一眼,algebra 的 type 就浮出來了 ─ 又是 Church encoding!再跟 Agda 的經驗對照一下就更清楚了 :D。

--
不過我還是先不要貼到 Lambdawan 上吧,Curry-Howard correspondence 要留給 Max XD。

Labels:

<< 回到主頁