@CoqExtraction/Letouzey/2

#The Extraction of Coq terms

This chapter is devoted to the presentation of our extraction function E over CIC terms. For the moment, this function will return terms in an intermediate theoretical language namd CIC□, untyped, which will play here a role similar to the one of Fω in the old extraction. The next chapter then deals with the translation into the final language, and in particular with the problem of typing the code extracted in this language.

In addition to the presentation of this function E, this chapter also contains the correctness proof of E, or rather the correctness proofs, since this theoretical study is divided into two parts:

• a first rather syntactic study enables us to guarantee that any reduction of extracted terms will succeed, regardless of the strict or lazy evaluation strategy used. This part is a revised version of the results presented in 55, themselves inspired by 54

• In a second time, we will establish in section 2.4 the correctness of these extracted terms with respect to the original Coq specifications, by using a semantic approach inspired by realizability,

Let us start first by detailing the limitations of the old function E of C. Paulin, which led us to build the current version of E.

• 2.1 The difficulties in the removal of logical parts