**Introduction to Type Theory**

by Herman Geuvers

**Publisher**: Radboud University Nijmegen 2011**Number of pages**: 57

**Description**:

The author gives an introductory overview of type theory for PhD students. He focuses on the use of type theory for compile-time checking of functional programs and on the use of types in proof assistants (theorem provers).

Download or read it online for free here:

**Download link**

(350KB, PDF)

## Similar books

**Programming in Martin-Lof's Type Theory: An Introduction**

by

**Bengt Nordstrom, Kent Petersson, Jan M. Smith**-

**Oxford University Press**

This book contains a thorough introduction to type theory, with information on polymorphic sets, subsets, and monomorphic sets. Martin-Lof's type theory makes possible the expression of both specifications and programs within the same formalism.

(

**8960**views)

**Homotopy Type Theory**

by

**Peter Aczel, et al.**-

**Institute for Advanced Study**

The present work has its origins in our collective attempts to develop a new style of 'informal type theory' that can be read and understood by a human being, as a complement to a formal proof that can be checked by a machine.

(

**6271**views)

**Intuitionistic Type Theory**

by

**Per Martin-Loef**

Contents: Propositions and judgements; Explanations of the forms of judgement; Propositions; Rules of equality; Hypothetical judgements and substitution rules; Judgements with more than one assumption and contexts; Sets and categories; etc.

(

**6932**views)

**Type Theory and Functional Programming**

by

**Simon Thompson**-

**Addison-Wesley**

The book is a course in type theory. It includes introduction to logic and functional programming, the type theory with many examples, the system from a mathematical perspective, and a number of important properties of the theory.

(

**10988**views)