Series: Penn State Logic Seminar

Date: Wednesday, August 4, 2004

Time: 11:10 AM - 12:25 PM

Place: 317 Boucke Building

Speaker: David H. King, Penn State, Computer Science

Title: The Curry-Howard Isomorphism

Abstract:

  In computer science, effective functions are a major object of
  interest; in logic, proofs of formulas are equally as important.
  The Curry-Howard Isomorphism gives a connection between these two
  areas of study.  Types in the lambda calculus correspond to
  formulas, while terms correspond to proofs in intuitionistic logic.
  I will introduce two systems and give a proof of the Curry-Howard
  Isomorphism between them, as well as discuss some applications of
  the isomorphism in the theory of programming languages.