CoqExtraction/LetouzeyOverview

原著のダウンロード(PDF)

#Extraction in Coq: an Overview Pierre Letouzey

Laboratoire PPS, Université Paris Diderot - Paris 7 Case 7014, F-75205 Paris Cedex 13, France

letouzey@pps.jussieu.fr

Abstract. The extraction mechanism of Coq allows one to transform Coq proofs and functions into functional programs. We illustrate the behavior of this tool by reviewing several variants of Coq definitions for Euclidean division, as well as some more advanced examples. We then continue with a more general description of this tool: key features, main examples, strengths, limitations and perspectives.

概要. Coqの抽出メカニズムは、1つがCoq証拠および機能を機能的なプログラムに転換することを可能にします。私たちは、幾分もっと進められた例と同様にユークリッドの区分用のCoq 定義のいくつかの変形を調査することにより、このツールの振る舞いを説明します。その後、私たちはこのツールのより多くの概要を継続します:重要な特徴、主な例、強さ、制限および展望。

##Table of contents - 1. Introduction - 2. Extraction in practive : div - 3. Examples beyond ML type system - 4. Key features of extraction - 5. Some significant Coq developments using extraction - 6. Conclusion and future works - Reference