Proofs and Types
by J. Girard, Y. Lafont, P. Taylor
Publisher: Cambridge University Press 1989
ISBN/ASIN: 0521371813
ISBN-13: 9780521371810
Number of pages: 183
Description:
This little book comes from a short graduate course on typed lambda-calculus given at the Universite Paris. It is not intended to be encyclopedic and the selection of topics was really quite haphazard. Some very basic knowledge of logic is needed, but we will never go into tedious details.
Download or read it online for free here:
Download link
(multiple formats)
Similar books
Programming and Programming Languagesby 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.
(6756 views)
Lecture Notes on the Lambda Calculusby Peter Selinger - Dalhousie University
Topics covered in these notes include the untyped lambda calculus, the Church-Rosser theorem, combinatory algebras, the simply-typed lambda calculus, the Curry-Howard isomorphism, weak and strong normalization, type inference, etc.
(10611 views)
Lectures on the Curry-Howard Isomorphismby Morten Heine B. Sorensen, Pawel Urzyczyn - Elsevier Science
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.
(10212 views)
Introduction 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.
(8477 views)