Lectures on the Curry-Howard Isomorphism
by Morten Heine B. Sorensen, Pawel Urzyczyn
Publisher: Elsevier Science 2006
Number of pages: 273
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:
by Noah D. Goodman, Andreas Stuhlmüller - dippl.org
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.
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.
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.