Type Theory and Functional Programming
by Simon Thompson
Publisher: Addison-Wesley 1999
Number of pages: 378
The book can be thought of as giving both a first and a second course in type theory. It begins with introductory material on logic and functional programming, and follow this by presenting the system of type theory itself, together with many examples. As well as this, this book goes further, looking at the system from a mathematical perspective, thus elucidating a number of its important properties. This book then takes a critical look at the profusion of suggestions in the literature about why and how type theory could be augmented. In doing this, this book is aiming at a moving target; it must be the case that further developments will have been made before the book reaches the press. Nonetheless, such an survey can give the reader a much more developed sense of the potential of type theory, as well as giving the background of what is to come.
Home page url
Download or read it online for free here:
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.
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.
by Herman Geuvers - Radboud University Nijmegen
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).
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.