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 :
Reports
Complete list of metadatas

Cited literature [12 references]  Display  Hide  Download

https://hal-lara.archives-ouvertes.fr/hal-02102062
Contributor : Colette Orange <>
Submitted on : Wednesday, April 17, 2019 - 9:13:15 AM
Last modification on : Wednesday, November 20, 2019 - 2:51:58 AM

File

RR1995-47.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : hal-02102062, version 1

Collections

Citation

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

Share

Metrics

Record views

10

Files downloads

11