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

Several formalisms for program construction have appeared. One such formalism is the type theory developed by Per Martin-Lof. Well suited as a theory for program construction, it makes possible the expression of 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.

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.

This book contains a thorough introduction to type theory, with information on polymorphic sets, subsets, monomorphic sets, and a full set of helpful examples.

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.