Type theory is a fast-evolving field at the crossroads of logic,
computer science and mathematics. This gentle step-by-step
introduction is ideal for graduate students and researchers who
need to understand the ins and outs of the mathematical machinery,
the role of logical rules therein, the essential contribution of
definitions and the decisive nature of well-structured proofs. The
authors begin with untyped lambda calculus and proceed to several
fundamental type systems culminating in the well-known and powerful
Calculus of Constructions. The book also covers the essence of
proof checking and proof development, and the use of dependent type
theory to formalize mathematics. The only prerequisites are a good
knowledge of undergraduate algebra and analysis. Carefully chosen
examples illustrate the theory throughout. Each chapter ends with a
summary of the content, some historical context, suggestions for
further reading and a selection of exercises to help readers
familiarize themselves with the material.
General
Is the information for this product incomplete, wrong or inappropriate?
Let us know about it.
Does this product have an incorrect or missing image?
Send us a new image.
Is this product missing categories?
Add more categories.
Review This Product
No reviews yet - be the first to create one!