Programming in


Martin-Löf's Type Theory

An Introduction



Bengt Nordström

Kent Petersson

Jan M. Smith







Department of Computing Sciences
University of Göteborg / Chalmers
S-412 96 Göteborg
Sweden






This book was published by Oxford University Press in 1990. It is now out of print. This version is available from www.cs.chalmers.se/Cs/Research/Logic/book.

Table of contents in Postscript.
The whole book (200 pages) in Postscript (1.5 Mb) and in pdf (1 Mb).