Jivaro is a small evaluator for the λc-calculus (an extension of λ-calculus with control operators) that has been designed to execute the programs extracted from classical proofs using the classical extraction module for Coq.
Inside the Jivaro toplevel, you can build and evaluate programs written in the λc-calculus, while defining new instructions and testing them interactively.
Jivaro can also be used in batch mode to compile source files and build libraries, or to inspect the contents of compiled files.
The Jivaro Manual is browsable
on-line.
It also exists as a
PDF file.
Current version of Jivaro is 0.9; it can be downloaded here.