 One alternative to realizability semantics for intuitionistic arithmetic is Gödel’s [1958] “Dialectica” interpretation, which associates with each formula \(B\) of \(L(\mathbf{HA})\) a quantifier-free formula \(B_D\) in the language of intuitionistic arithmetic of all finite types. The “Dialectica” interpretation of \(B,\) call it \(B^D,\) is \(\exists Y\forall x B_D (Y, x).\) If \(B\) is a closed theorem of \(\mathbf{HA},\) then \(B_D (F, x)\) is provable for some term \(F\) in Gödel’s theory \(\mathbf{T}\) of “primitive recursive” functionals of higher type. The translation from \(B\) to \(B^D\) requires the axiom of choice (at all finite types), MP and IP, so is not strictly constructive; however, the number-theoretic functions expressible by terms \(F\) of \(\mathbf{T}\) are precisely the provably recursive functions of \(\mathbf{HA}\) (and of \(\mathbf{PA}).\) The interpretation was extended to analysis by Spector [1962]; cf. Howard [1973]. Clear expositions, and additional references, are to be found in Troelstra’s introduction to the English translation in Gödel [1990] of the original Dialectica article, in Avigad and Feferman [1998], and in Ferreira [2008].