• Title Lectures on the Curry-Howard Isomorphism
• Author(s): Morten Heine B. Sorensen, Pawel Urzyczyn
• Publisher: Elsevier Science; 1 edition (September 28, 2006); eBook (The Final Draft)
• Hardcover: 456 pages
• eBook: PDF
• Language: English
• ISBN-10: 0444520775
• ISBN-13: 978-0444520777
• Share This:  

Book Description

This book gives an introduction to parts of proof theory and related aspects of type theory relevant for the Curry-Howard isomorphism. It can serve as an introduction to any or both of typed lambda-calculus and intuitionistic logic.

The Curry-Howard isomorphism states an amazing correspondence between systems of formal logic as encountered in proof theory and computational calculi as found in type theory.

For instance, minimal propositional logic corresponds to simply typed lambda-calculus, first-order logic corresponds to dependent types, second-order logic corresponds to polymorphic types, sequent calculus is related to explicit substitution, etc.

• N/A

• Amazon

• Mathematical Logic - Set Theory, Model Theory, Computability, etc
• Theory of Programming Languages
• Theory of Computation
• Introduction to Computer Science

• Lectures on the Curry-Howard Isomorphism (M. H. Sorensen, et al)

• Book of Proof, 2nd Edition (Richard H. Hammack)
• An Introduction to Set Theory (William A. R. Weiss)
• A Friendly Introduction to Mathematical Logic (Chris Leary)
• Introduction to Mathematical Logic (Vilnis Detlovs, et al)