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.
This report has now been superseded by ECS-LFCS-92-242.
Previous | Index | Next An error occured whilst processing this directive