A functional functional interpretation

ABSTRACT. In this paper, we present a modern reformulation of the Dialectica interpretation based on the linearized version of De Paiva. Contrarily to Gödel's original translation which translated HA into system T, our presentation applies on untyped λ-terms and features nicer proof-theoretical properties.

In the Curry-Howard perspective, we show that the computational behaviour of this translation can be accurately described by the explicit stack manipulation of the Krivine abstract machine, thus giving it a direct-style operational explanation.

Finally, we give direct evidence that supports the fact our presentation is quite relevant, by showing that we can apply it to the dependently-typed system CCω almost without any adaptation. This answers the question of the validity of Dialectica-like constructions in a dependent setting.