2026-07-26T17:14:36Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:18016 2024-03-06T11:00:52Z ddc:004 open_access

Diller-Nahm Bar Recursion Blot, Valentin Dialectica Bar recursion We present a generalization of Spector’s bar recursion to the Diller-Nahm variant of Gödel’s Dialectica interpretation. This generalized bar recursion collects witnesses of universal formulas in sets of approximation sequences to provide an interpretation to the double-negation shift principle. The interpretation is presented in a fully computational way, implementing sets via lists. We also present a demand-driven version of this extended bar recursion manipulating partial sequences rather than initial segments. We explain why in a Diller-Nahm context there seems to be several versions of this demand-driven bar recursion, but no canonical one. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Valentin Blot 2023 Is Part Of LIPIcs, Volume 260, 8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.FSCD.2023.32 urn:nbn:de:0030-drops-180164 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2023.32 eng https://creativecommons.org/licenses/by/4.0/legalcode