Natural Proofs Versus Program Optimization in the calculus of Inductive Constructions

This paper presents how to automatically prove that an "optimized " program is correct with respect to a set of given properties that is a specification. Proofs of specifications contain logical and computational parts. Programs can be seen as computational parts of proofs. They can thus be extracted from proofs and be certified to be correct. The inverse problem can be solved: it is possible to reconstruct proof obligations from a program and its specification [18, 19]. The framework is a type theory where a proof can be represented as a typed -term [2, 14] and, particularly, the Calculus of Inductive Constructions [7]. This paper shows how programs can be simplified in order to be written in a much closer way to the ML one's. Indeed, proofs structures are often much more heavy than programs structures. The problem is consequently to consider natural programs (in a ML sense) and see how to retrieve natural structures of proofs from them. This research was partly supported by ESPRIT ..