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