Document Open Access Logo

On the Algorithmic Structure of Dialectica Realisers

Authors Davide Barbarossa , Thomas Powell

PDF

File

Thumbnail PDF
PDF
LIPIcs.CSL.2026.22.pdf
  • Filesize: 0.89 MB
  • 22 pages

Document Identifiers

Related Versions

Subject Classification

ACM Subject Classification
  • Theory of computation → Proof theory
  • Theory of computation → Constructive mathematics
Keywords
  • Dialectica interpretation
  • Hoare logic
  • Programs from proofs

Metrics

Abstract

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 past decades, it has also been studied from the perspective of programming languages, and our contribution is in that direction. Specifically, we present Dialectica as a collection of rules in the style of Hoare logic, where Dialectica is now viewed as a language for specifying procedural programs that come with a forward and backward direction. This viewpoint captures the interesting dynamics of realisers extracted by the Dialectica interpretation, and we illustrate this by defining a generalised backpropagation semantics for a fragment of this language. We envisage this work as providing a base for several future developments, both theoretical and practical, which we outline at the end.

Cite As Get BibTex

Davide Barbarossa and Thomas Powell. On the Algorithmic Structure of Dialectica Realisers. In 34th EACSL Annual Conference on Computer Science Logic (CSL 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 363, pp. 22:1-22:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026) https://doi.org/10.4230/LIPIcs.CSL.2026.22

Author Details

Davide Barbarossa
  • Department of Computer Science, University of Bath, UK
Thomas Powell
  • Department of Computer Science, University of Bath, UK

Funding

This work was funded by the Engineering and Physical Sciences Research Council, grant number EP/W035847/1.

Acknowledgements

The authors thank Ulrich Berger (who first suggested looking at the frame rule) and Marie Kerjean (who among other things helped clarify several points from [Kerjean and Pédrot, 2024]).

References

  1. Wilhelm Ackermann. Begründung des "tertium non datur" mittels der Hilbertschen Theorie der Widerspruchsfreiheit. Mathematische Annalen, 93:1-36, 1924. URL: https://doi.org/10.1007/BF01449946.
  2. Federico Aschieri and Stefano Berardi. Interactive learning-based realizability for Heyting arithmetic with EM1. Logical Methods in Computer Science, 6(3), 2010. URL: https://doi.org/10.2168/LMCS-6(3:19)2010.
  3. Federico Aschieri, Adata Ciabattoni, and Francesco Genco. On the concurrent computational content of intermediate logics. Theoretical Computer Science, 813:375-409, 2020. URL: https://doi.org/10.1016/j.tcs.2020.01.022.
  4. Jeremy Avigad, Edward T. Dean, and Jason Rute. A metastable dominated convergence theorem. Journal of Logic & Analysis, 4(3):1-19, 2012. URL: https://doi.org/10.4115/jla.2012.4.3.
  5. Jeremy Avigad, Philipp Gerhardy, and Henry Towsner. Local stability of ergodic averages. Transactions of the American Mathematical Society, 362(1):261-288, 2010. URL: https://doi.org/10.1090/S0002-9947-09-04814-4.
  6. Stefano Berardi, Marc Bezem, and Thierry Coquand. On the computational content of the axiom of choice. Journal of Symbolic Logic, 63(2):600-622, 1998. URL: https://doi.org/10.2307/2586854.
  7. Ulrich Berger and Helmut Schwichtenber. Program extraction from classical proofs. In Logic and Computational Complexity workshop (LCC’94), volume 960 of Lecture Notes in Computer Science, pages 77-97, 1995. URL: https://doi.org/10.1007/3-540-60178-3_80.
  8. Valeria de Paiva. The Dialectica categories. PhD thesis, University of Cambridge, 1991. Published as Technical Report 213, Computer Laboratory, University of Cambridge. URL: https://doi.org/10.48456/tr-213.
  9. Jerry den Hartog and Erik P. de Vink. Verifying probabilistic programs using a Hoare like logic. International Journal of Foundations of Computer Science, 13:315-340, 2002. URL: https://doi.org/10.1142/S012905410200114X.
  10. Justus Diller. Eine Variante zur Dialectica-Interpretation der Heyting-Arithmetik endlicher Typen. Archiv für mathematische Logik und Grundlagenforschung, 16(1-2):49-66, 1974. URL: https://doi.org/10.1007/BF02025118.
  11. Philipp Gerhardy and Ulrich Kohlenbach. General logical metatheorems for functional analysis. Transactions of the American Mathematical Society, 360:2615-2660, 2008. URL: https://doi.org/10.1090/S0002-9947-07-04429-7.
  12. Kurt Gödel. Über eine bisher noch nicht benützte Erweiterung des finiten Standpunktes. dialectica, 12(3-4):280-287, 1958. URL: https://doi.org/10.1111/j.1746-8361.1958.tb01464.x.
  13. Timothy Griffin. A formulae-as-type notion of control. In Proceedings of Principles of Programming Languages (POPL'90), pages 47-58. ACM, 1990. URL: https://doi.org/10.1145/96709.96714.
  14. Charles Antony Richard Hoare. An axiomatic basis for computer programming. Communications of the ACM, 12(10):576-580, 1969. URL: https://doi.org/10.1145/363235.363259.
  15. William A. Howard. Hereditarily majorizable functionals of finite type. In Anne S. Troelstra, editor, Metamathematical Investigation of Intuitionistic Arithmetic and Analysis, volume 344 of Lecture Notes in Mathematics. Springer-Verlag, 1973. URL: https://doi.org/10.1007/BFb0066739.
  16. Marie Kerjean and Pierre-Marie Pédrot. δ is for Dialectica. In Proceedings of Logic in Computer Science (LICS'24), pages 48:1-13. ACM, 2024. URL: https://doi.org/10.1145/3661814.3662106.
  17. Ulrich Kohlenbach. Some logical metatheorems with applications in functional analysis. Transactions of the American Mathematical Society, 357(1):89-128, 2005. URL: https://doi.org/10.1090/s0002-9947-04-03515-9.
  18. Ulrich Kohlenbach. Applied Proof Theory: Proof Interpretations and their Use in Mathematics. Springer Monographs in Mathematics. Springer, 2008. URL: https://doi.org/10.1007/978-3-540-77533-1.
  19. Ulrich Kohlenbach. Recent progress in proof mining in nonlinear analysis. IFCoLoG Journal of Logics and their Applications, 10(4):3361-3410, 2017. URL: https://www2.mathematik.tu-darmstadt.de/~kohlenbach/progress-new.pdf.
  20. Ulrich Kohlenbach. Proof-theoretic methods in nonlinear analysis. In Proceedings of the International Congress of Mathematicians 2018, volume 2, pages 61-82. World Scientific, 2019. URL: https://doi.org/10.1142/9789813272880_0045.
  21. Ulrich Kohlenbach. Local formalizations in nonlinear analysis and related areas and proof-theoretic tameness. In Kreisel’s Interests: On the Foundations of Logic and Mathematics, volume 41 of Tributes, pages 45-61. College Publications, 2020. URL: https://www2.mathematik.tu-darmstadt.de/~kohlenbach/Kreisel2018.pdf.
  22. Jean-Louis Krivine. Realizability in classical logic. in: Interactive models of computation and program behaviour. Panoramas et synthéses, 27:197-229, 2009. URL: https://hal.science/hal-00154500/document.
  23. Wilfried Meyer-Viol. Instantial Logic. PhD thesis, University of Amsterdam, 1985. URL: https://eprints.illc.uva.nl/id/eprint/1984/2/DS-1995-11.text.pdf.
  24. Alexandre Miquel. Existential witness extraction in classical realizability and via a negative translation. Logical Methods in Computer Science, 7(2:2):1-47, 2011. URL: https://doi.org/10.2168/LMCS-7(2:2)2011.
  25. Morenikeji Neri and Nicholas Pischke. Proof mining and probability theory. Forum of Mathematics, Sigma, 13:e187, 2025. URL: https://doi.org/10.1017/fms.2025.10138.
  26. Morenikeji Neri, Nicholas Pischke, and Thomas Powell. Generalized learnability of stochastic principles. In Proceedings of Computability in Europe (CiE'25), volume 15764 of LNCS, pages 333-348, 2025. URL: https://doi.org/10.1007/978-3-031-95908-0_24.
  27. Morenikeji Neri and Thomas Powell. On quantitative convergence for stochastic processes: Crossings, fluctuations and martingales. Transactions of the American Mathematical Society, Series B, 12:974-1019, 2025. URL: https://doi.org/10.1090/btran/229.
  28. Morenikeji Neri and Thomas Powell. A quantitative Robbins-Siegmund theorem. Annals of Applied Probability, 2025. To appear. URL: https://doi.org/10.48550/arXiv.2410.15986.
  29. Peter O'Hearn and David Pym. The logic of bunched implications. Bulletin of Symbolic Logic, 5(2):215-244, 1999. URL: https://doi.org/10.2307/421090.
  30. Paulo Oliva. Unifying functional interpretations. Notre Dame Journal of Formal Logic, 47(2):263-290, 2006. URL: https://doi.org/10.1305/ndjfl/1153858651.
  31. Paulo Oliva. Functional interpretations of linear and intuitionistic logic. Information and Computation, 208(5):565-577, 2010. URL: https://doi.org/10.1016/j.ic.2008.11.008.
  32. Michel Parigot. λμ-calculus: An algorithmic interpretation of classical natural deduction. In Proceedings of Logic Programming and Automated Reasoning (LPAR'92), pages 190-201. Springer Berlin Heidelberg, 1992. URL: https://doi.org/10.1007/BFb0013061.
  33. Pierre-Marie Pédrot. A functional functional interpretation. In Joint proceedings of Computer Science Logic and Logic in Computer Science (CSL-LICS'14), pages 77:1-10. ACM, 2014. URL: https://doi.org/10.1145/2603088.2603094.
  34. Thomas Powell. Gödel’s functional interpretation and the concept of learning. In Proceedings of Logic in Computer Science (LICS '16), pages 136-145. ACM, 2016. URL: https://doi.org/10.1145/2933575.2933605.
  35. Thomas Powell. Computational interpretations of classical reasoning: From the epsilon calculus to stateful programs. In Mathesis Universalis, Computability and Proof, volume 412 of Synthese Library, pages 255-290. Springer, 2019. URL: https://doi.org/10.1007/978-3-030-20447-1_14.
  36. Thomas Powell. Proofs as stateful programs: A first-order logic with abstract Hoare triples. Logical Methods in Computer Science, 20(1):7:1-7:32, 2024. URL: https://doi.org/10.46298/LMCS-20(1:7)2024.
  37. John C. Reynolds. Separation logic: a logic for shared mutable data structures. In Proceedings of Logic in Computer Science (LICS'02), pages 55-74. IEEE, 2002. URL: https://doi.org/10.1109/LICS.2002.1029817.
  38. Helmut Schwichtenberg. Dialectica interpretation of well‐founded induction. Mathematical Logic Quarterly, 54(3):229-239, 2008. URL: https://doi.org/10.1002/malq.200710045.
  39. Davide Trotta, Jonathan Weinberger, and Valeria de Paiva. Skolem, Gödel, and Hilbert fibrations. available at https://arxiv.org/abs/2407.15765, 2024.
Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

Please try again later or send an E-mail
© 2023-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact