|
Abstract : |
machine instead of lambda-terms. Thus, we get a framework to compile correctly programs extracted from proof by translating their proof in our system and then extracting the code. Moreover, we will see that we can associate programs to classical proofs. 1 Introduction. The proof as program paradigm, using the Curry-Howard isomorphism [4], gives a way to associate a program to an intuitionistic proof. This program is almost always a functional program (in general a lambda-term [1]) which has to be compiled before being executed [11]., |
