Summary of Philip Walder’s "Proofs are Programs"

Posted on June 19, 2015 by Kwang Yul Seo

This is my short summary of Philip Wadler’s Proofs are Programs: 19th Century Logic and 21st Century Computing.

Proofs and programs are the same thing. But it took a century of efforts to recognize the relationship.

So it took more than 30 years to recognize the correspondence between Gentzen’s natural deduction and Church’s typed lambda calculus. They are the same thing! Proofs and programs. This correspondence is called Curry-Howard Isomorphism.

Logicians and computer scientists have discovered exactly the same type systems!