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

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

An introduction to type theory as a theory for program construction. Describes different type theories (theories of types, polymorphic and monomorphic sets, and subsets) from a computing science perspective.

Publication date: 31 Dec 1990

ISBN-10: n/a

ISBN-13: n/a

Paperback: 211 pages

Views: 14,765

Type: N/A

Publisher: Oxford University Press

License: n/a

Post time: 07 Nov 2006 07:11:43

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

Programming in Martin-Löf's Type Theory: An Introduction An introduction to type theory as a theory for program construction. Describes different type theories (theories of types, polymorphic and monomorphic sets, and subsets) from a computing science perspective.
Tag(s): Functional Programming
Publication date: 31 Dec 1990
ISBN-10: n/a
ISBN-13: n/a
Paperback: 211 pages
Views: 14,765
Document Type: N/A
Publisher: Oxford University Press
License: n/a
Post time: 07 Nov 2006 07:11:43
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.




About The Author(s)


No information is available for this author.

Bengt Nordström

No information is available for this author.


No information is available for this author.

Kent Petersson

No information is available for this author.


No information is available for this author.

Jan M. Smith

No information is available for this author.


Book Categories
Sponsors
Icons8, a free icon pack