Skip to Main content Skip to Navigation

Marking techniques for extraction.

Abstract : 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.
Document type :
Complete list of metadata

Cited literature [12 references]  Display  Hide  Download
Contributor : Colette ORANGE Connect in order to contact the contributor
Submitted on : Wednesday, April 17, 2019 - 9:13:15 AM
Last modification on : Saturday, September 11, 2021 - 3:19:15 AM


Files produced by the author(s)


  • HAL Id : hal-02102062, version 1



Frederic Prost. Marking techniques for extraction.. [Research Report] LIP RR-1995-47, Laboratoire de l'informatique du parallélisme. 1995, 2+35p. ⟨hal-02102062⟩



Record views


Files downloads