Monograph: Type Theory and Functional Programming

To: logic, types
Subject: Monograph: Type Theory and Functional Programming
From: sjt@ukc.ac.uk
Date: Fri, 2 Aug 1991 05:36:58 -0400
Sender: meyer@theory.lcs.mit.edu
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