**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

**Programming Languages: Theory and Practice**

by

**Robert Harper**-

**Carnegie Mellon University**

What follows is a working draft of a planned book that seeks to strike a careful balance between developing the theoretical foundations of programming languages and explaining the pragmatic issues involved in their design and implementation.

(

**7340**views)

**Programming and Programming Languages**

by

**Shriram Krishnamurthi**-

**Brown University**

Many people would regard this as being two books in one. One book is an introduction to programming, teaching you basic concepts of organizing data and the programs that operate over them. The other book is an introduction to programming languages.

(

**4204**views)

**Formal Syntax and Semantics of Programming Languages**

by

**Kenneth Slonneger, Barry L. Kurtz**-

**Addison Wesley Longman**

The book presents the typically difficult subject of formal methods in an informal, easy-to-follow manner. Readers with a basic grounding in discreet mathematics will be able to understand the practical applications of these difficult concepts.

(

**11660**views)

**A Practical Theory of Programming**

by

**Eric C.R. Hehner**-

**Springer**

Understanding programming languages requires knowledge of the underlying theoretical model. This book explores aspects of programming that are amenable to mathematical proof. It describes a simple and comprehensive theory.

(

**10403**views)