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

**The Design and Implementation of Probabilistic Programming Languages**

by

**Noah D. Goodman, Andreas Stuhlmüller**-

**dippl.org**

This book explains how to implement PPLs by lightweight embedding into a host language. We illustrate this by designing WebPPL, a small PPL embedded in Javascript. We show how to implement several algorithms for universal probabilistic inference.

(

**1582**views)

**Programming Languages: Application and Interpretation**

by

**Shriram Krishnamurthi**-

**Lulu.com**

The textbook for a programming languages course, taken primarily by advanced undergraduate and beginning graduate students. This book assumes that students have modest mathematical maturity, and are familiar with the existence of the Halting Problem.

(

**7977**views)

**Denotational Semantics: A Methodology for Language Development**

by

**David Schmidt**-

**Kansas State University**

Denotational semantics is a methodology for giving mathematical meaning to programming languages and systems. This book was written to make denotational semantics accessible to a wider audience and to update existing texts in the area.

(

**7244**views)

**Computational Category Theory**

by

**D.E. Rydeheard, R.M. Burstall**

The book is a bridge-building exercise between computer programming and category theory. Basic constructions of category theory are expressed as computer programs. It is a first attempt at connecting the abstract mathematics with concrete programs.

(

**13278**views)