Lectures on the Curry-Howard Isomorphism
by Morten Heine B. Sorensen, Pawel Urzyczyn
Publisher: Elsevier Science 2006
ISBN/ASIN: 0444520775
Number of pages: 273
Description:
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. This book give 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.
Download or read it online for free here:
Download link
(1.3MB, PDF)
Similar books

by Joey Paquet, Serguei A. Mokhov - arXiv
Lecture notes for the Comparative Studies of Programming Languages course. These notes include a compiled book of primarily related articles from the Wikipedia, as well as Comparative Programming Languages book and other resources.
(9526 views)

- Wikibooks
This book is an attempt to describe a bit of the programming languages zoo. We use each of the particular languages to introduce fundamental notions related to the design and the implementation of general purpose programming languages.
(9299 views)

by Neal Ziring
The Dictionary of Programming Languages is an online compendium of computer coding methods assembled to provide information and aid your appreciation for computer science history. The dictionary currently has over 120 entries.
(13091 views)

by Robert Harper
Provides an account of the role of type theory in programming language design and implementation. The stress is on the use of types as a tool for analyzing programming language features and studying their implementation.
(15886 views)