The Coq mailing list

[David MENTRE <dmentre AT linux-france.org>]

Hello Cedric,

2013/11/20 Cedric Auger 
<sedrikov AT gmail.com>:
> Still, maybe you wanted to do extraction and have proved programs in OCaml
> thanks to it, simply, this is not the Curry Howard isomorphism, it is some
> other interesting theory (but don’t forget, that once extracted, you cannot
> go back to the proof

Yes, I just wanted to illustrate Coq proof, extraction and proved
programs (Robbert example is nice in that regard). You are right that
I misunderstood that the Curry-Howard isomorphism was used for the
extraction mechanism. I thought the extracted program was issued from
the Coq proof (by interpreting the proof as program through
Curry-Howard) after erasing type annotations.

Now a last question: is the Curry-Howard isomorphism used in Coq
internals or not at all? In other words, is this isomorphism needed in
underlying Coq logic or not?


Thank you for your replies,
Best regards,
david