Logo

Lectures on the Curry-Howard Isomorphism

Large book cover: Lectures on the Curry-Howard Isomorphism

Lectures on the Curry-Howard Isomorphism
by

Publisher: Elsevier Science
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

Book cover: Comparative Studies of Programming LanguagesComparative Studies of Programming Languages
by - 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.
(8504 views)
Book cover: Exploring Programming Language Architecture in PerlExploring Programming Language Architecture in Perl
by
This book presents an informal and friendly introduction to some of the core ideas in modern computer science, using the programming language Perl as its vehicle. The book takes the form of a series of working interpreters for the language PScheme.
(14312 views)
Book cover: Introduction to Programming LanguagesIntroduction to Programming Languages
- 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.
(8281 views)
Book cover: Implementing Functional Languages: a tutorialImplementing Functional Languages: a tutorial
by - Prentice Hall
This book gives a practical approach to understanding implementations of non-strict functional languages using lazy graph reduction. It is intended to be a source of practical material, to help make functional-language implementations come alive.
(11673 views)