On the algorithmic structure of Dialectica realisers

Davide Barbarossa, Thomas Powell

Gödel's Dialectica interpretation is a fundamental tool for the extraction of computational content from proofs, and plays a central role in today's proof mining program. In the p…