In this thesis, we give a computational interpretation to Gödel's Dialectica translation, in a fashion inspired by classical realizability. In particular, it can be shown that the Dialectica translation manipulates stacks of the Krivine machine as first-class objects and that the main effect at work lies in the accumulation of those stacks at each variable use. The original translation suffers from a handful of defects due to hacks used by Gödel to work around historical limitations. Once these defects are solved, the translation naturally extends to much more expressive settings such as dependent type theory. A few variants are studied thanks to the linear decomposition, and relationships with other translations such as forcing and CPS are scrutinized.
展开▼
