Edit abstract data
This talk will try to describe the current status of the extraction
mechanism currently available in the Coq proof assistant. Through
real-life extraction examples, we will present key features of this
extraction from the user's perspective, such as:
- (almost) complete support of any Coq development, even with
dependent types or other high-end features of Coq,
- code generation for several programming languages,
- modularity aspects.
We will see the consequences of these key features on the development
of this extraction, and in particular the controlled use of unsafe
aspects of the output languages. We will also discuss the current
remaining limitations of this framework, for instance the relative
lack of fine-grain control on the elimination of useless parts during
extraction. Finally, we will describe ongoing works aiming at
formally certify this extraction framework.