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 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 Simon Peyton Jones, David Lester - 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.
by Bill Hails
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.
by Keijo Ruohonen - Tampere University of Technology
In these notes the classical Chomskian formal language theory is fairly fully dealt with, omitting however much of automata constructs and computability issues. Surveys of Lindenmayer system theory and the mathematical theory of codes are given.