Processing ......
FreeComputerBooks.com
Links to Free Computer, Mathematics, Technical Books all over the World

Want to know the elevation (AMSL) at any spot all over world? Try GIS Visualizer.
 Title Lectures on the CurryHoward Isomorphism
 Author(s): Morten Heine B. Sorensen, Pawel Urzyczyn
 Publisher: Elsevier Science; 1 edition (September 28, 2006); eBook (1998)
 Hardcover: 456 pages
 eBook: PDF
 Language: English
 ISBN10: 0444520775
 ISBN13: 9780444520777
 Share This:
Book Description
This book gives an introduction to parts of proof theory and related aspects of type theory relevant for the CurryHoward isomorphism. It can serve as an introduction to any or both of typed lambdacalculus and intuitionistic logic.
The CurryHoward 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 lambdacalculus, firstorder logic corresponds to dependent types, secondorder logic corresponds to polymorphic types, sequent calculus is related to explicit substitution, etc.
About the Author(s) N/A