Terms and Conditions:

Bengt Nordström wrote: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 Excerpts:

Several formalisms for program construction have been introduced. One such formalism is the type theory developed by Per Martin-Löf. It is well suited as a theory for program construction since it is possible to express both specifications and programs within the same formalism. Furthermore, the proof rules can be used to derive a correct program from a specification as well as to verify that a given program has a certain property. This book contains an introduction to type theory as a theory for program construction.

As a programming language, type theory is similar to typed functional languages such as Hope and ML, but a major difference is that the evaluation of a well-typed program always terminates. In type theory it is also possible to write specifications of programming tasks as well as to develop provably correct programs. Type theory is therefore more than a programming language and it should not be compared with programming languages, but with formalized programming logics such as LCF and PL/CV.

One of the main differences between the type theory presentation in this book and the one in Per Martin-Löf's Constructive Mathematics and Computer Programming is that this book uses a uniform notation for expressions. Per Martin-Löf has formulated a theory of mathematical expressions in general, which is presented in chapter 3. This book describes how arbitrary mathematical expressions are formed and introduces an equality between expressions. This book also shows how defined constants can be introduced as abbreviations of more complicated expressions.

Intended Audience:

This book is intended for researchers and graduate students with an interest in the foundations of computing science, and it is mathematically self-contained.