Curry-Howard

メモ 読む

とりあえずはメモだけ

このような「型＝命題，プログラム＝証明」という対応のことを，カリー・ハワードの対応（Curry-Howard correspondence）という

http://itpro.nikkeibp.co.jp/article/COLUMN/20070909/281498/

http://www.kmonos.net/wlog/61.html#_0538060508
http://pkturner.org/programming/Curry-Howard.html