2025/01/27 by Barbarossa, Davide, Powell, Thomas
#FOS: Computer and information sciences #Logic in Computer Science (cs.LO)
paper · doi:10.48550/arxiv.2501.16208
We explore the Dialectica interpretation from the perspective of programming languages, by presenting it as a collection of rules in the style of Hoare logic. This allows us to add a while loop construct for Dialectica realizers, which offers an elegant description of programs extracted from nonconstructive principles. We characterise Dialectica realizers in terms of a generalised backpropagation procedure, whose forward component can be regarded as a `stateful' program in the usual sense. We propose several directions in which the work we present here can be developed in future.