Computability in Europe 2006
Logical Approaches to Computational Barriers

Special Session Talk:
Extraction in Coq: an Overview

Speaker: Pierre Letouzey


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:

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.

websites: Arnold Beckmann 2007-11-12