The Coq mailing list

[Yevgeniy Makarov <emakarov AT cs.indiana.edu>]

Hello,

I am interested in using Coq for program extraction from classical
proofs. Coq seems suitable for this because it produces nice proof
terms, which are almost programs. So I hope to prove theorems in Coq,
take proof terms and use them by my own programs to replace the
classical rule NNPP by call/cc, eliminate computationally irrelevant
information, normalize, and so on (currently I have a normalizer
written in Scheme). It is quite possible to parse proof terms that are
displayed by Print command, but I am wondering if there is a still
easier way, namely, if I can get an access to the proof term's inner
representation.

Thank you,
Yevgeniy