Recursive programming with proofs

摘要: There has been a lot of work based on the paradigm “proofs as programs”, leading to sophisticated realizations (see e.g. [2,4, 133). An expected benefit is development correct programs, but, so far, no programming language in current use came from these works. The difficulty apparent distance between proofs and programs: are often complicated extracted programs have not always behaviour (in terms complexity, for instance). only but also contain conceptual parts explaining why result what it is. One needs, therefore, distinguish algorithmic content content. distinction can be done at different levels: logical operators. propositional connectives an content, whereas quantifiers considered having role (the universal quantifier indicates degree generality). ~ dejnition objects. iterative recursive definitions data types do same (they correspond access data). themsehes. are, instance, ways doing by induction; termination require computations which really necessary compute result. choices made each levels crucial design proofs. We explain remaining part this introductory section particular we construct experimental called PROPRE (for PROgrammation avec des PREuves).