Computability in Europe 2006
Logical Approaches to Computational Barriers


Special Session Talk:
Extraction in Coq: an Overview


Speaker: Pierre Letouzey

Abstract

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