An operational approach to program extraction in the Calculus of Constructions

Abstract

The Theory of Specifications is an extension of the Calculus of Constructions where the specification of a problem, the derivation of a program, and its correctness proof, can all be done within the same formalism. An operational semantics describes the process of extracting a program from a proof its specification. This has several advantages: from the user's point of view, it simplifies the task of developing correct programs, since it is sufficient to know just one system in order to be able to specify, develop and prove the correction of a program; from the implementation point of view, the fact that extraction procedure is part of the system. In this paper we continue the study of the Theory of Specificiations and propose a solution to restore subject reduction and strong normalization. Counterexamples for subject reduction and strong normalization for this theory have been shownin [RS02].