xacid: (Default)
[personal profile] xacid
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.
This account has disabled anonymous posting.
If you don't have an account you can create one now.
No Subject Icon Selected
More info about formatting

Profile

xacid: (Default)
xacid

April 2021

S M T W T F S
    123
45678910
11121314151617
18192021222324
252627282930 

Most Popular Tags

Style Credit

Expand Cut Tags

No cut tags
Page generated Jul. 26th, 2025 08:59 am
Powered by Dreamwidth Studios