The Coq mailing list

[Andrej Bauer <andrej.bauer AT andrej.com>]

> The extraction currently in Coq does not use a typed realizability model.

Thank you for the explanation. I simply assumed that the extraction
carries the types along. It seems harder to reconstruct the types once
they're thrown away.

It would be interesting to know if one can do "better" by following
more closely an interpretation of types as well as terms.

> I'm not saying that all this could not be related to your way of
> presenting extraction, but I don't consider your way the "primary" one,
> as you seem to assert.

Untyped realizability is a special case of typed realizability (it is
the uni-typed case). So in this sense Scheme seems to be the ideal
target language for Coq extraction.

With kind regards,

Andrej