Showing cs.LOShow all
2 papers · 1 filter
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…
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…