The Coq mailing list

[Bruno Barras <bruno.barras AT inria.fr>]

On 02/14/2012 05:23 PM, Andrej Bauer wrote:
> > 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).

As far as I can tell, modified realizability has the property that the 
termination of realizers is known "a priori": originally, they were 
simply-typed lambda-terms. The point is that you can use the realizer 
outside its specification (but within its domain type!) without losing 
termination or type-safety.
In Coq, you could prove correct a division algorithm which extracted 
term loops when the divisor is 0. This is related to the difficulty to 
remove __ that Stéphane mentioned. In general, the trouble comes in when 
using singleton elimination or fixpoints with informative codomain and 
non-informative recursive argument.

Bruno.

--
Bruno Barras                    Typical team - INRIA Saclay
LIX - Ecole Polytechnique       91128 Palaiseau Cedex - France
Tel: +33 1 69 33 40 57          Fax: +33 1 69 33 30 14