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

This book was published by Oxford University Press in 1990. It is now out of print. This version is available from

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