3 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 pa…
math.CT2024
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 not…
cs.LO2024
Denotational semantics driven simplicial homology?
Davide Barbarossa
We look at the proofs of a fragment of Linear Logic as a whole: in fact, Linear Logic's coherent semantics interprets the proofs of a given formula as faces of an abstract simp…