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.