Computability in Europe 2008
Logic and Theory of Algorithms

Print current page  Print this page

Special Session Talk:
Extraction in Coq: an Overview

Edit abstract data

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:

  • (almost) complete support of any Coq development, even with advanced 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.

websites: Arnold Beckmann 2007-11-12 Valid HTML 4.01! Valid CSS!