2 papers
cs.LO2025
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…
math.CT2025
An excursion into Dialectica and Differentiation
Davide Barbarossa
Gödel's Dialectica has been introduced and developed in the tradition of the so-called functional interpretations. Only recently has it been related with the a priori unrelated no…