Extended projection---new method to extract efficient programs from constructive proofs
Yukihide Takayama · 1989
This paper gives a method to extract redundancy free programs from constructive proofs, using the realizability interpretation.The proof trees are analyzed in the style of program analysis, and they are mechanically translated into trees with additional information, called marked proof trees.The program extractor takes marked proof trees as input, and generates programs in a type-free lambda calculus with sequences.the basic mechanism of the program extractor.Also, various techniques, such as proof normalization and Harrop formulas, are used to generate efficient programs [Goad 801 [Bates 791 [Sasaki 861.This paper works on the problem of redundant code, which is one of the main problems in terms of efficient code generation with q-realizability.However, the problem is not always inherent to a particular formulation of realizability.