The Coq mailing list

[Adam Chlipala <adamc AT hcoop.net>]

Andrej Bauer wrote:
> I have always wondered about the mathematical background behind
> extraction, and it seems like a good opportunity to ask. Is there a
> place where I could read about the mathematical theory that supports
> Coq's extraction mechanisms? I suppose it's a kind of realizability
> interpretation of Coq's language, right?
>   

My understanding is that it's much simpler than that.  CIC is already a 
programming language, so there's no need for any deep "interpretation of 
proofs as programs."  Extraction is just optimization plus translation 
to a different language.  There are two things going on that are 
completely disjoint in principle:

1. Replace every type of type [Prop] with [unit].  Replace every proof 
(i.e., value of one of these types) with [tt].
2. Translate to OCaml or Haskell, using "unsafe" casts where needed to 
make up for less expressive type systems, but otherwise doing no 
theoretically interesting work.

Someone more familiar with the details of extraction implementation and 
theory might have a more refined perspective.