[Prev][Next][Index][Thread]
Book: Simon Thompson, "Type Theory and Functional Programming"
Date: Thu, 01 Aug 91 09:42:50 +0100
Type Theory and Functional Programming
Simon Thompson
Addison-Wesley Publishers 1991, 387 pp. ISBN 0-201-41667-0
Constructive type theory is a formal system which is simul-
taneously a logic and a functional programming language.
This means that within the same system can be developed
functional programs and proofs of their correctness. In
addition to this, because of the constructive nature of the
logic, programs can be extracted from proofs written in the
logic.
This book provides an introduction to all aspects of
type theory, but places a stronger emphasis on the func-
tional programming interpretation than in other expositions.
Ideas are illustrated with examples as they are introduced,
and a number of larger case studies are examined in more
depth.
As well as introducing the system, many of its proper-
ties (such as confluence and termination) are discussed in a
thoroughgoing way. The core system, due to the logician
Martin-Lof, has been augmented in many ways by various
authors; in the final part of the book these additions are
discussed and evaluated: some of the features are seen to
add complications or to have undesirable side-effects on the
remainder of the system.
At the start of the text are introductions to the
natural deduction style of logic, functional programming in
the lambda calculus and the basics of constructive mathemat-
ics - these are used to establish terminology and to orient
the reader. The text is concluded with a survey of the foun-
dations of the system itself, together with an examination
of other related systems. Each section of the text contains
exercises which range from the routine to the challenging,
and a comprehensive bibliography is included.
It is expected that the audience will be experienced
undergraduate or postgraduate students in computer science
and mathematics, as well as research staff and teachers in
these fields.
Contents
Preface
Introduction
Chapter 1 Introduction to Logic
Chapter 2 Functional Programming and lambda-Calculi
Chapter 3 Constructive Mathematics
Chapter 4 Introduction to Type Theory
Chapter 5 Exploring Type Theory
Chapter 6 Applying Type Theory
Chapter 7 Augmenting Type Theory
Chapter 8 Foundations
Chapter 9 Conclusions
Bibliography
Appendix - Rule Tables
Index