照井一成「計算と論理」

ここでは、カリー＝ハワード同型対応についての説明がある。
証明とプログラミングは、一般には、違うものであると考えられているが、非常に単純な同型性が見られるというのだ。
詳しいことは、自分ももうちょっと機会があれば、勉強してみてから、書きたい（プログラミングの検証とも関係あるようだ）。参考文献もあるので、見てみてはどうでしょう。

知の教科書　論理の哲学 (講談社選書メチエ)