2005-06-09 Proofs are Programs: 19th Century Logic and 21st Century Computing logic functionals Philip Wadler ! 15p.目次。 Gentzen's natural deducation Charch's lambda calculus Typed lambda calculus The Curry-Howard correspondence Conclusions http://homepages.inf.ed.ac.uk/wadler/papers/frege/frege.pdf