# Monograph: 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

```