 The importance of the theorem for foundations cannot be  overstated.[21]  A discussion of its generalizations, of ensuing work on functional interpretations stimulated by the theorem due to Kreisel, Tait, Howard, Feferman and others; its foundational and philosophical significance; and finally its relation particularly to the earlier, informal, proof interpretation, so-called, given by Heyting-Kolmogorov, will not be attempted here. Accordingly the reader is referred to the large literature on the subject, e.g., the abovementioned Troelstra 1986, Tait 1967, Feferman 1993 and Avigad &amp; Feferman 1998. For interesting recent developments, e.g., in the area of relating Gödel’s Dialectica interpretation and Kreisel’s modified realizability, see Oliva 2006. See also van Oosten 2008.