Type Theory and Formal Proof: An Introduction

by Herman Geuvers ROB NEDERPELT

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 including 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 formalise mathematics The only prerequisite is a basic knowledge of undergraduate mathematics 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 familiarise themselves with the material

Genres: Mathematics, Computer Science, Logic, Programming, Nonfiction

Paperback

First published August 29, 2014

Reviews

[Matt Parsons · Rating 5 out of 5]

Fantastic introduction to type theory. It is beginner friendly -- they even include a list of Greek letters and pronunciation in the *front* of the book! The math starts out very simple. If you've taken high school algebra courses, then you'll have enough background to get started. They do a fantastic job of introducing terminology and notation.

I would recommend the first half of this book to anyone interested in studying computer science or type theory. It provides the necessary background to dig into more advanced books, like Pierce's "Types and Programming Languages", as well as the current research literature.

[Alex Nelson · Rating 5 out of 5]

For mathematicians, the best introduction to Barendregt's lambda cube (and hence, the best introduction to type theory for the foundations of mathematics) I've seen anywhere. Discusses the three axes of the cube rather than each vertex, and focuses most of the discussion on the Calculus of Construction. Clearly bent towards Martin-Lof's work on the foundations of math.

[allen · Rating 4 out of 5]

Read the first half (up to encoding logical notions in λC). The first three chapters are pretty clear and easy to understand, but once it gets to type dependent on types and terms, they stopped giving syntax rules and things becomes more sloppy, requiring more work from the reader to understand the full implication of the typing system.
Would recommend this to all readers who know a bit of logic, but make sure to at least skim through the exercises and proofs portion of the text, as they become increasingly important.

[Taha Fadhly]

Please

[Thomas · Rating 5 out of 5]

Very functional