The Coq mailing list

[Jean-Francois Monin <Jean-Francois.Monin AT imag.fr>]

On Fri, Jun 05, 2009 at 02:10:05PM -0400, Adam Chlipala wrote:
> 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.

Sorry, I don't have the time for a detailed answer and I'm not
a specialist. Hope that Pierre Letouzey will provide an up-to-date answer.

Roughly, things are a bit more complicated, e.g. if you consider
termination problems or higher universes.  So yes, realizability is
perfectly relevant.  The theory for Coq was developed in the thesis of
Christine Paulin, in 1989. Pierre Letouzey worked on that topic in the
framework of the current version of Coq, see his thesis (I think that
an english version is available).

Regards,

-- 
Jean-Francois Monin           Univ. Joseph Fourier, GRENOBLE
VERIMAG - Centre Equation     http://www-verimag.imag.fr/~monin/
2 avenue de Vignate           tel (+33 | 0) 4 56 52 04 39
F-38610 GIERES                fax (+33 | 0) 4 56 52 04 46