Program construction in intuitionistic Type Theory

This talk is an introduction to the Type Theoretical approach to the Mathematics of Program Construction.

The basic idea of this approach can be summarized briefly. It was realized by Bishop (1967) that a constructive proof of an existential statement is an algorithm for computing a witness of this statement. Furthermore, a specification of a functional program can be thought of as an existential proposition which may have parameters. The potential of these remarks for the problem of Program Construction is the following: to constructively prove such a proposition can be seen as a systematic and elegant way to achieve a “hand-in-hand” development of programs together with a proof that they satisfy their specification.

Type Theory is a particular formal language designed by P. Martin-Löf to express proofs in constructive mathematics. Type Theory has strong connections with functional programming and it is thus a natural candidate for actualizing this approach of Program Construction on computers.

We survey the recent development in this field and base the presentation on a particular implementation of Type Theory that emphasizes these connections. Type Theory is there seen as a functional programming language with dependent types, and proofs are functional programs.

We present some implemented examples where this type theoretical approach is particularly elegant, among others a representation of constructive geometry due to J. von Plato (Helsinki). We also compare it on one example with constructive (or transformational) programming.

Authors and Affiliations

1. Computer Science Department, Chalmers Technical University and University of Göteborg, S-41296, Göteborg, Sweden

   Thierry Coquand

Reprints and permissions

© 1995 Springer-Verlag Berlin Heidelberg

Policies and ethics