The Coq mailing list

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

> 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.

As far as I know, the original realizers were numbers, not
lambda-terms. Kleene used partial recursive functions in the first
version of realizablity.

The original modified realizability (by Kreisel?) is not the best way
to think of realizability for the purposes of extraction. It is better
to use the so-called "typed partial combinatory algebras", see [1] for
one version (if I had to do it again today, I would use assemblies
insetad of pers or modest sets to simplify things _and_ be more
general).

With kind regards,

Andrej

[1] 
http://math.andrej.com/2007/01/21/rz-a-tool-for-bringing-constructive-and-computable-mathematics-closer-to-programming-practice/