Marking techniques for extraction.

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.La logique constructive peut être utilisée pour produire des programmes en les considérant comme des formules de la logique. L'avantage d'une telle méthodologie est de produire des programmes dont on est sûr qu'ils vérifient certaines spécifications. Les programmes générés par ces méthodes sont en général peu efficaces car ils comportent de larges parts qui ne servent pas au calcul final. Pour les repérer et les effacer, de nombreuses techniques ont déjà été développées. On parle de technique d'extraction. Dans ce travail nous donnons une nouvelle manière d'approcher ce problème. Il s'agit du marquage. Ce nouvel angle de vision permet, grâce à un niveau d'abstraction élevé, d'unifier les connaissances relatives à l'extraction. Il permet aussi l'extension aux ordres supérieurs des techniques de taillage exploitées par Berardi et Boerio, qui n'étaient valables qu'aux premier et au second ordre