Marking Techniques for Extraction
Frederic Prost, 69 - Lyon (France). Lab. de l'Informatique du Parallelisme Centre National de la Recherche Scientifique (CNRS), 69 (France). Lab. de l'Informatique du Parallelisme Lyon-1 Univ., 69 (France). Lab. de l'Informatique du Parallelisme Ecole Normale Superieure de Lyon · 1995
Constructive logic can be used to consider program specifications as logical formulas. The advantage of this approach is to generate programs which are certified with respect to some given specifications. The programs created in such a way are not efficient because they may contain large parts with no computational meaning. The elimination of these parts is an important issue. Many attempts to solve this problem have been already done. We call this extracting procedure. In this work we present a new way to understand the extraction problem. This is the marking technique. This new point of view enables us, thanks to a high abstraction level, to unify what was previously done on the subject. It enables also to extend to higher--order languages some pruning techniques developed by Berardi and Boerio, which were only used in first and second order language. Keywords: Program Verification, Type Theory, Logic, Program proof, Extraction, Marking. R'esum'e La logique constructive peut etre u...