カリーハワード同型対応についてのまとめ - きしだのHatena昨日のエントリでカリーハワード同型対応について触れました。 関数を扱えることはどのようにプログラミング言語の能力をあげるか - きしだのはてな ついでに、このエントリを書くのに調べたカリーハワード同型対応の資料をまとめておきます。 この記事では、カリーハワード同型対応で、どのような型がどのような論理命題に対応するかを解説してあります。 数理科学的バグ撲滅方法論のすすめ - 第14回 型＝命題，プログラム＝証明：ITpro こちらのほうが、ちょっとくだけてるかな？ Curry-Howard Isomorphism - d.y.d. カリーハワード同型対応での山場は、排中律がSchemeのcall/ccに対応するというところで、gotoなどもだいたいこれにあてはまるようです。 排中律、つまり「a または not a」という命題です。これは証明としてはアヤシイので、古典論理からはずしましょうとな
Photo Tourism: Microsoft Research, Interactive Visual Media Group
