#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.

本章は、CIC用語にわたる私たちの抽出関数Eのプレゼンテーションに専念します。さしあたり、この機能は、ここで古い抽出中のFωの1つに似ている役割を果たす中間の理論的な言語namd CIC□(untyped)の中の用語を返すでしょう。その後、次の章は、最終言語への、およびこの言語で抽出されたコードをタイプする問題を備えた項目中の翻訳に対処します。

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:

この関数Eのプレゼンテーションに加えて、この理論的な研究が2部に分割されるので、本章はさらにEの正確さ証拠、あるいはやや正確さ証拠を含んでいます: 

- 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](ref#55), themselves inspired by [54](ref#54)

- 私たちは、使用される厳密な戦略か遅延評価戦略にかかわらず、抽出された用語のどんな縮小も成功するだろうということを最初のやや構文的な研究によって保証することができます。この部分は54までに励起されて、それら自身55に示された結果の改訂版です。 

- 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,

- 直ちに、時間と私たちは、実現可能性によって励起された意味的なアプローチの使用により、オリジナルのCoq仕様書に関してセクション2.4にこれらの抽出された用語の正確さを確立するでしょう、 

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.

C.Paulin(それは私たちにEの現行版を構築させた)の古い関数Eの制限の詳述により最初にスタートしましょう。 

- [2.1 The difficulties in the removal of logical parts](2/2.1)