A Functional Functional Interpretation
May. 30th, 2020 04:47 pm![[personal profile]](https://www.dreamwidth.org/img/silk/identity/user.png)
https://www.pédrot.fr/articles/lics2014.pdf
In this paper, we present a modern reformulation of the Dialectica interpretation based on the linearized version of de Paiva. Contrarily to Go ̈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 calculus of constructions with universes CCω almost without any adaptation. This answers the question of the validity of Dialectica-like constructions in a dependent setting.
In this paper, we present a modern reformulation of the Dialectica interpretation based on the linearized version of de Paiva. Contrarily to Go ̈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 calculus of constructions with universes CCω almost without any adaptation. This answers the question of the validity of Dialectica-like constructions in a dependent setting.