The classical extraction module for Coq enriches the Coq proof assistant (version 8.2 or higher) with a set of commands to extract programs from classical proofs built in the Coq environment.
The target language of the extraction mechanism is the λc-calculus, an extension of λ-calculus with control primitives introduced by Jean-Louis Krivine to realize provable formulae of classical logic.
Extracted programs are stored in lambda-calculus object files (.lco) that can be inspected, loaded and evaluated using the Jivaro toplevel.
The manual of the classical extraction module for Coq is
browsable on-line.
It also exists as a
PDF file.
Current version of the classical extraction module for Coq is 0.9; it can be downloaded here.
The classical extraction module for Coq can be compiled in two different ways: either as a statically linked module rooted in the Coq toplevel (static install), or as a separatedly compiled module that can be dynamically loaded in the Coq toplevel using the command Require ClassicalExtraction (dynamic install).
For the exact installation procedure, see the file INSTALL in the archive.