## Deliverables: an approach to program development in the
Calculus of Constructions

**R. Burstall and J. McKinna**
*Abstract:* We propose a methodology for developing
programs in the Extended Calculus of Constructions. Using
predicates for input-output specifications, we define a
*deliverable* as a program-proof pair. We then define
operations such as composition, exponentiation and iteration on
these pairs, enabling us to build a larger program with its proof
from a collection of smaller such pairs. The operations define a
cartesian closed category. We sketch an extension to relational
specifications.

*LFCS report ECS-LFCS-91-133*

This report has now been superseded by ECS-LFCS-92-242.

Previous |

Index |

Next