Programming in Martin-Löf's Type Theory: An Introduction

by Bengt Nordström, Kent Petersson, Jan M. Smith

In recent years, several formalisms for program construction have appeared. One such formalism is the type theory developed by Per Martin-L f. 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. This book contains a thorough introduction to type theory, with information on polymorphic sets, subsets, monomorphic sets, and a full set of helpful examples.

Genres: Mathematics, Computer Science

232 pages, Hardcover

First published July 19, 1990

Reviews

[0xd34df00d · Rating 4 out of 5]

Pros: a very enlightening book, makes you ask a lot of questions that don't arise while reading most other books on TT.

Cons: let's put it this way: not the most accessible book I've ever read. Even Girard's "Proofs and types" seems to be more approachable (considering the level of math in both books). The material sometimes isn't clearly written either. For instance, it took me a while to realize why what the authors describe as equality on the function type is not extensional equality, and the best way to do this was to throw away the textual description and just follow the presentation of the judgements.

Also there are quite some typos, some of which interfere with understanding the material, and no available errata.