Document Open Access Logo

Computation First: Rebuilding Constructivism with Effects (Invited Talk)

Author Liron Cohen

PDF HTML 5

Files

Thumbnail PDF
PDF
LIPIcs.FSCD.2025.1.pdf
  • Filesize: 0.77 MB
  • 20 pages
HTML5 Logo HTML (experimental)
LIPIcs.FSCD.2025.1.html

Document Identifiers

Subject Classification

ACM Subject Classification
  • Theory of computation
Keywords
  • Effectful constructivism
  • realizability
  • type theory
  • monadic combinatory algebras
  • evidenced frame

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Abstract

Constructive logic and type theory have traditionally been grounded in pure, effect-free model of computation. This paper argues that such a restriction is not a foundational necessity but a historical artifact, and it advocates for a broader perspective of effectful constructivism, where computational effects, such as state, non-determinism, and exceptions, are directly and internally embedded in the logical and computational foundations. We begin by surveying examples where effects reshape logical principles, and then outline three approaches to effectful constructivism, focusing on realizability models: Monadic Combinatory Algebras, which extend classical partial combinatory algebras with effectful computation; Evidenced Frames, a flexible semantic structure capable of uniformly capturing a wide range of effects; and Effectful Higher-Order Logic (EffHOL), a syntactic approach that directly translates logical propositions into specifications for effectful programs. We further illustrate how concrete type theories can internalize effects, via the family of type theories TT^□_C. Together, these works demonstrate that effectful constructivism is not merely possible but a natural and robust extension of traditional frameworks.

Cite As Get BibTex

Liron Cohen. Computation First: Rebuilding Constructivism with Effects (Invited Talk). In 10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 337, pp. 1:1-1:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025) https://doi.org/10.4230/LIPIcs.FSCD.2025.1

Author Details

Liron Cohen
  • Ben-Gurion University, Beer-Sheva, Israel

Funding

This work was supported by Grant No. 2020145 from the United States-Israel Binational Science Foundation (BSF).

Acknowledgements

The author is deeply grateful to her collaborators in the various parts of this exploration - Robert Constable, Ariel Grunfeld, Dominik Kirst, Étienne Miquey, Bruno da Rocha Paiva, Vincent Rahli, Sam Speight and Ross Tate - for an exceptionally insightful and truly enjoyable research experience.

References

  1. Peter Aczel. The Type Theoretic Interpretation of Constructive Set Theory: Choice Principles. In Studies in Logic and the Foundations of Mathematics, volume 110, pages 1-40. Elsevier, 1982. Google Scholar
  2. Nada Amin and Ross Tate. Java and Scala’s Type Systems Are Unsound: The Existential Crisis of Null Pointers. In Proceedings of the 2016 ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, and Applications, OOPSLA 2016, pages 838-848, New York, NY, USA, 2016. ACM. URL: https://doi.org/10.1145/2983990.2984004.
  3. Zena M. Ariola, Paul Downen, Hugo Herbelin, Keiko Nakata, and Alexis Saurin. Classical Call-by-Need Sequent Calculi: The Unity of Semantic Artifacts. In Tom Schrijvers and Peter Thiemann, editors, Functional and Logic Programming - 11th International Symposium, FLOPS, Lecture Notes in Computer Science, pages 32-46. Springer, 2012. URL: https://doi.org/10.1007/978-3-642-29822-6.
  4. Jeremy Avigad. Forcing in Proof Theory. The Bulletin of Symbolic Logic, 10(3):305-333, 2004. URL: https://doi.org/10.2178/BSL/1102022660.
  5. Martin Baillon, Assia Mahboubi, and Pierre-Marie Pédrot. Gardening with the Pythia A Model of Continuity in a Dependent Setting. In Florin Manea and Alex Simpson, editors, CSL, volume 216 of LIPIcs, pages 5:1-5:18. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2022. URL: https://doi.org/10.4230/LIPIcs.CSL.2022.5.
  6. Andrej Bauer and James E. Hanson. The Countable Reals, 2024. URL: https://arxiv.org/abs/2404.01256.
  7. Stefano Berardi, Marc Bezem, and Thierry Coquand. On the Computational Content of the Axiom of Choice. J. Symb. Log., 63(2):600-622, 1998. URL: https://doi.org/10.2307/2586854.
  8. Jean-Philippe Bernardy and Marc Lasson. Realizability and Parametricity in Pure Type Systems. In Foundations of Software Science and Computational Structures: 14th International Conference, FOSSACS, pages 108-122. Springer, 2011. URL: https://doi.org/10.1007/978-3-642-19805-2_8.
  9. Mark Bickford, Liron Cohen, Robert L. Constable, and Vincent Rahli. Open Bar - a Brouwerian Intuitionistic Logic with a Pinch of Excluded Middle. In Christel Baier and Jean Goubault-Larrecq, editors, 29th EACSL Annual Conference on Computer Science Logic (CSL 2021), volume 183, pages 11:1-11:23, 2021. URL: https://doi.org/10.4230/LIPIcs.CSL.2021.11.
  10. Valentin Blot and Colin Riba. On Bar Recursion and Choice in a Classical Setting. In Programming Languages and Systems - 11th Asian Symposium, APLAS, pages 349-364, December 2013. URL: https://doi.org/10.1007/978-3-319-03542-0_25.
  11. Simon Boulier, Pierre-Marie Pédrot, and Nicolas Tabareau. The Next 700 Syntactical Models of Type Theory. In Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs, CPP 2017, pages 182-194, 2017. URL: https://doi.org/10.1145/3018610.3018620.
  12. Liron Cohen, Sofia Abreu Faro, and Ross Tate. The Effects of Effects on Constructivism. In Proceedings of the Thirty-Fifth Conference on the Mathematical Foundations of Programming Semantics, MFPS 2019, London, UK, June 4-7, 2019, volume 347, pages 87-120, 2019. Proceedings of the Thirty-Fifth Conference on the Mathematical Foundations of Programming Semantics. URL: https://doi.org/10.1016/j.entcs.2019.09.006.
  13. Liron Cohen, Bruno da Rocha Paiva, Vincent Rahli, and Ayberk Tosun. Inductive Continuity via Brouwer Trees. In Jérôme Leroux, Sylvain Lombardy, and David Peleg, editors, 48th International Symposium on Mathematical Foundations of Computer Science (MFCS), volume 272, pages 37:1-37:16, 2023. URL: https://doi.org/10.4230/LIPIcs.MFCS.2023.37.
  14. Liron Cohen, Yannick Forster, Dominik Kirst, Bruno Da Rocha Paiva, and Vincent Rahli. Separating Markov’s Principles. In Proceedings of the 39th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS '24, 2024. URL: https://doi.org/10.1145/3661814.3662104.
  15. Liron Cohen, Ariel Grunfeld, Dominik Kirst, and Étienne Miquey. From Partial to Monadic: Combinatory Algebra with Effects. In Maribel Fernández, editor, 10th International Conference on Formal Structures for Computation and Deduction (FSCD), volume 337 of LIPIcs, 2025. Google Scholar
  16. Liron Cohen, Ariel Grunfeld, Dominik Kirst, and Étienne Miquey. Syntactic Effectful Realizability in Higher-Order Logic. In 40th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), 2025. Google Scholar
  17. Liron Cohen, Étienne Miquey, and Ross Tate. Evidenced Frames: A Unifying Framework Broadening Realizability Models. In 2021 36th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), pages 1-13, 2021. URL: https://doi.org/10.1109/LICS52264.2021.9470514.
  18. Liron Cohen and Vincent Rahli. Constructing Unprejudiced Extensional Type Theories with Choices via Modalities. In FSCD, volume 228 of LIPIcs, pages 10:1-10:23, 2022. URL: https://doi.org/10.4230/LIPIcs.FSCD.2022.10.
  19. Liron Cohen and Vincent Rahli. Realizing Continuity Using Stateful Computations. In Bartek Klin and Elaine Pimentel, editors, 31st EACSL Annual Conference on Computer Science Logic (CSL), volume 252, pages 15:1-15:18, 2023. URL: https://doi.org/10.4230/LIPIcs.CSL.2023.15.
  20. Liron Cohen and Vincent Rahli. TT^□_C: a Family of Extensional Type Theories with Effectful Realizers of Continuity. Logical Methods in Computer Science, Volume 20, Issue 2, June 2024. URL: https://doi.org/10.46298/lmcs-20(2:18)2024.
  21. The CompCert Project. URL: http://compcert.inria.fr/.
  22. Thierry Coquand and Guilhem Jaber. A Note on Forcing and Type Theory. Fundam. Inform., 100(1-4):43-52, 2010. URL: https://doi.org/10.3233/FI-2010-262.
  23. Thierry Coquand and Guilhem Jaber. A Computational Interpretation of Forcing in Type Theory. In P. Dybjer, Sten Lindström, Erik Palmgren, and G. Sundholm, editors, Epistemology versus Ontology: Essays on the Philosophy and Foundations of Mathematics in Honour of Per Martin-Löf, pages 203-213. Springer Netherlands, Dordrecht, 2012. URL: https://doi.org/10.1007/978-94-007-4435-6_10.
  24. Thierry Coquand and Bassel Mannaa. The Independence of Markov’s Principle in Type Theory. Log. Methods Comput. Sci., 13(3), 2017. URL: https://doi.org/10.23638/LMCS-13(3:10)2017.
  25. Pierre-Louis Curien and Hugo Herbelin. The Duality of Computation. In ICFP, 2000. URL: https://doi.org/10.1145/351240.351262.
  26. Radu Diaconescu. Axiom of Choice and Complementation. Proceedings of the American Mathematical Society, 51(1):176-178, 1975. URL: http://www.jstor.org/stable/2039868.
  27. Hannes Diener. Constructive Reverse Mathematics, 2020. URL: https://arxiv.org/abs/1804.05495.
  28. Bruno Dinis and Étienne Miquey. Realizability with Stateful Computations for Nonstandard Analysis. In Computer Science Logic, January 2021. URL: https://hal.science/hal-03002239.
  29. Sophia Drossopoulou, Susan Eisenbach, and Sarfraz Khurshid. Is the Java Type System Sound? Theory and practice of object systems, 5(1):3-24, 1999. Google Scholar
  30. Martín Hötzel Escardó. Continuity of Gödel’s System T Definable Functionals via Effectful Forcing. Electr. Notes Theor. Comput. Sci., 298:119-141, 2013. URL: https://doi.org/10.1016/j.entcs.2013.09.010.
  31. Solomon Feferman. A Language and Axioms for Explicit Mathematics. In Algebra and logic, pages 87-139. Springer, 1975. Google Scholar
  32. Andrzej Filinski. Controlling Effects. PhD thesis, School of Computer Science, Carnegie Mellon University, Pittsburgh, Pennsylvania, 1996. Google Scholar
  33. Yannick Forster, Matthieu Sozeau, and Nicolas Tabareau. Verified Extraction from Coq to OCaml. Proceedings of the ACM on Programming Languages, 8(PLDI):52-75, 2024. URL: https://doi.org/10.1145/3656379.
  34. Jonas Frey. Characterizing Partitioned Assemblies and Realizability Toposes. Journal of Pure and Applied Algebra, 223(5):2000-2014, 2019. URL: https://doi.org/10.1016/j.jpaa.2018.08.012.
  35. Samuel Gardelle and Étienne Miquey. Do CPS Translations Also Translate Realizers? In Timothy Bourke and Delphine Demange, editors, JFLA 2023 - 34èmes Journées Francophones des Langages Applicatifs, pages 103-120, January 2023. URL: https://hal.inria.fr/hal-03910311.
  36. Jean-Yves Girard. Interprétation Fonctionnelle Et élimination Des Coupures De L’arithmétique D’ordre Supérieur. PhD thesis, Université Paris Diderot - Paris 7, 1972. Google Scholar
  37. Von Kurt Gödel. Über eine bisher noch nicht benützte erweiterung des finiten standpunktes. dialectica, 12(3-4):280-287, 1958. Google Scholar
  38. Timothy Griffin. A Formulae-as-type Notion of Control. In Proceedings of the 17th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL '90, pages 47-58, New York, NY, USA, 1990. ACM. URL: https://doi.org/10.1145/96709.96714.
  39. Hugo Herbelin. An Intuitionistic Logic that Proves Markov’s Principle. In 2010 25th Annual IEEE Symposium on Logic in Computer Science. IEEE, 2010. URL: https://doi.org/10.1109/lics.2010.49.
  40. Hugo Herbelin. A Constructive Proof of Dependent Choice, Compatible with Classical Logic. In LICS, 2012. URL: https://hal.inria.fr/hal-00697240.
  41. Pieter JW Hofstra. Partial Combinatory Algebras and Realizability Toposes. University of Ottowa, 2004. Google Scholar
  42. William Alvin Howard. The Formulae-as-Types Notion of Construction. In Haskell Curry, Hindley B., Seldin J. Roger, and P. Jonathan, editors, To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus, and Formalism. Academic Press, 1980. Google Scholar
  43. J. Martin E. Hyland, Peter T. Johnstone, and Andrew M Pitts. Tripos Theory. In Mathematical Proceedings of the Cambridge philosophical society, volume 88, pages 205-232, 1980. Google Scholar
  44. INRIA. The Coq Proof Assistant Reference Manual, 2023. Google Scholar
  45. Guilhem Jaber, Gabriel Lewertowski, Pierre-Marie Pédrot, Matthieu Sozeau, and Nicolas Tabareau. The Definitional Side of the Forcing. In Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science, LICS '16, pages 367-376. Association for Computing Machinery, 2016. URL: https://doi.org/10.1145/2933575.2935320.
  46. Stephen C. Kleene. On the Interpretation of Intuitionistic Number Theory. Journal of Symbolic Logic, 10(4):109-124, 1945. URL: https://doi.org/10.2307/2269016.
  47. Michal Konečný, Sewon Park, and Holger Thies. Axiomatic Reals and Certified Efficient Exact Real Computation. In Logic, Language, Information, and Computation: 27th International Workshop, WoLLIC, pages 252-268, Berlin, Heidelberg, 2021. URL: https://doi.org/10.1007/978-3-030-88853-4_16.
  48. Georg Kreisel. A Remark on Free Choice Sequences and the Topological Completeness Proofs. The Journal of Symbolic Logic, 23(4):369-388, 1958. URL: https://doi.org/10.2307/2964012.
  49. Georg Kreisel. The Non-derivability of ¬(x)A(x) → (∃ x)¬(Ax), A (x) primitive recursive, in intuitionistic formal systems (abstract). Jour. Symb. Logic, 23(4):456–457, 1958. Google Scholar
  50. Georg Kreisel. Interpretation of Analysis by Means of Constructive Functionals of Finite Types. In A. Heyting, editor, Constructivity in mathematics, pages 101-128. North-Holland Pub. Co., 1959. Google Scholar
  51. Jean-Louis Krivine. Dependent choice, `Quote' and the Clock. Th. Comp. Sc., 308:259-276, 2003. URL: https://doi.org/10.1016/S0304-3975(02)00776-4.
  52. Jean-Louis Krivine. Realizability in Classical Logic. Panoramas et synthèses, 27:197-229, 2009. URL: https://hal.science/hal-00154500.
  53. Pierre Letouzey. A New Extraction for Coq. In International Workshop on Types for Proofs and Programs, pages 200-219. Springer, 2002. URL: https://doi.org/10.1007/3-540-39185-1_12.
  54. Robert S. Lubarsky. On the Cauchy Completeness of the Constructive Cauchy Reals. Electron. Notes Theor. Comput. Sci., 167:225-254, January 2007. URL: https://doi.org/10.1016/j.entcs.2006.09.012.
  55. Per Martin-Löf. Constructive Mathematics and Computer Programming. Oxford University Press, 1982. Google Scholar
  56. Alexandre Miquel. Existential Witness Extraction in Classical Realizability and via a Negative Translation. Logical Methods in Computer Science, Volume 7, Issue 2, April 2011. URL: https://doi.org/10.2168/LMCS-7(2:2)2011.
  57. Étienne Miquey. A Sequent Calculus with Dependent Types for Classical Arithmetic. In Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS '18, pages 720-729, 2018. URL: https://doi.org/10.1145/3209108.3209199.
  58. Étienne Miquey. A Constructive Proof of Dependent Choice in Classical Arithmetic via Memoization, 2019. URL: https://arxiv.org/abs/1903.07616.
  59. Étienne Miquey and Hugo Herbelin. Realizability Interpretation and Normalization of Typed Call-by-Need λ-Calculus with Control. In FoSSaCS, 2018. URL: https://doi.org/10.1007/978-3-319-89366-2_1.
  60. Eugenio Moggi. Notions of Computation and Monads. Information and computation, 93(1):55-92, 1991. URL: https://doi.org/10.1016/0890-5401(91)90052-4.
  61. Tobias Nipkow and David von Oheimb. Javalight is Type-Safe—Definitely. In Proceedings of the 25th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL '98, pages 161-170, 1998. URL: https://doi.org/10.1145/268946.268960.
  62. Ulf Norell. Towards a Practical Programming Language Based on Dependent Type Theory. PhD thesis, Chalmers University of Technology, 2007. Google Scholar
  63. P. Oliva and T. Streicher. On Krivine’s Realizability Interpretation of Classical Second-Order Arithmetic. Fundam. Inform., 84(2):207-220, 2008. URL: http://iospress.metapress.com/content/f51774wm73404583/.
  64. Christine Paulin-Mohring. Introduction to the Calculus of Inductive Constructions. In Bruno Woltzenlogel Paleo and David Delahaye, editors, All about Proofs, Proofs for All, volume 55 of Studies in Logic (Mathematical logic and foundations). College Publications, January 2015. URL: https://hal.inria.fr/hal-01094195.
  65. Pierre-Marie Pédrot. Russian Constructivism in a Prefascist Theory. In Holger Hermanns, Lijun Zhang, Naoki Kobayashi, and Dale Miller, editors, 35th Annual ACM/IEEE Symposium on Logic in Computer Science, Saarbrücken, Germany, pages 782-794. ACM, 2020. URL: https://doi.org/10.1145/3373718.3394740.
  66. Pierre-Marie Pédrot. "Upon This Quote I Will Build My Church Thesis". In Proceedings of the 39th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS '24, 2024. URL: https://doi.org/10.1145/3661814.3662070.
  67. Pierre-Marie Pédrot and Nicolas Tabareau. An Effectful Way to Eliminate Addiction to Dependence. In Logic in Computer Science (LICS), 2017 32nd Annual ACM/IEEE Symposium on, page 12, 2017. URL: https://doi.org/10.1109/LICS.2017.8005113.
  68. Pierre-Marie Pédrot and Nicolas Tabareau. Failure is Not an Option - An Exceptional Type Theory. In 27th European Symposium on Programming, volume 10801 of LNCS, pages 245-271. Springer, April 2018. URL: https://doi.org/10.1007/978-3-319-89884-1_9.
  69. Pierre-Marie Pédrot and Nicolas Tabareau. The Fire Triangle: How to Mix Substitution, Dependent Elimination, and Effects. Proc. ACM Program. Lang., 4(POPL):58:1-58:28, 2020. URL: https://doi.org/10.1145/3371126.
  70. Pierre-Marie Pédrot, Nicolas Tabareau, Hans Jacob Fehrmann, and Éric Tanter. A Reasonably Exceptional Type Theory. Proc. ACM Program. Lang., 3(ICFP):108:1-108:29, 2019. URL: https://doi.org/10.1145/3341712.
  71. Andrew M Pitts. Evaluation Logic. In IV Higher Order Workshop, Banff 1990: Proceedings of the IV Higher Order Workshop, pages 162-189. Springer, 1991. Google Scholar
  72. Andrew M Pitts. Tripos Theory in Retrospect. Mathematical structures in computer science, 12(3):265-279, 2002. URL: https://doi.org/10.1017/S096012950200364X.
  73. Vincent Rahli and Mark Bickford. A Nominal Exploration of Intuitionism. In Proceedings of the 5th ACM SIGPLAN Conference on Certified Programs and Proofs, CPP 2016, pages 130-141, 2016. URL: https://doi.org/10.1145/2854065.2854077.
  74. Michael Rathjen. Choice Principles in Constructive and Classical Set Theories. In Logic Colloquium, volume 2, pages 299-326, 2002. Google Scholar
  75. Anne S. Troelstra. Metamathematical Investigation of Intuitionistic Arithmetic and Analysis, volume 344 of Lecture Notes in Mathematics. Springer-Verlag, 1973. Google Scholar
  76. Mark van Atten. On Brouwer. Wadsworth Philosophers. Cengage Learning, 2004. Google Scholar
  77. Jaap van Oosten. The Modified Realizability Topos. Journal of pure and applied algebra, 116(1-3):273-289, 1997. Google Scholar
  78. Jaap Van Oosten. Realizability: an Introduction to its Categorical Side, volume 152. Elsevier, Amsterdam, 2008. Google Scholar
  79. Philip Wadler. Monads for Functional Programming. In International School on Advanced Functional Programming, pages 24-52. Springer, 1995. URL: https://doi.org/10.1007/3-540-59451-5_2.
  80. Philip Wadler. Propositions as types. Communications of the ACM, 58(12):75-84, 2015. URL: https://doi.org/10.1145/2699407.
  81. Chuangjie Xu. A Continuous Computational Interpretation of Type Theories. PhD thesis, University of Birmingham, UK, 2015. URL: http://etheses.bham.ac.uk/5967/.
  82. Xuejun Yang, Yang Chen, Eric Eide, and John Regehr. Finding and Understanding Bugs in C Compilers. In Proceedings of the 32nd ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), pages 283-294. ACM, 2011. URL: https://doi.org/10.1145/1993498.1993532.
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