{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,4]],"date-time":"2026-05-04T05:57:19Z","timestamp":1777874239340,"version":"3.51.4"},"publisher-location":"Cham","reference-count":69,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783032227195","type":"print"},{"value":"9783032227201","type":"electronic"}],"license":[{"start":{"date-parts":[[2026,1,1]],"date-time":"2026-01-01T00:00:00Z","timestamp":1767225600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2026,4,10]],"date-time":"2026-04-10T00:00:00Z","timestamp":1775779200000},"content-version":"vor","delay-in-days":99,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2026]]},"abstract":"<jats:title>Abstract<\/jats:title>\n                  <jats:p>\n                    We revisit the famous notion of sheaves through the lens of type theory and side-effects. Using the language of\n                    <jats:inline-formula>\n                      <jats:alternatives>\n                        <jats:tex-math>$$\\textsf{MLTT}$$<\/jats:tex-math>\n                        <mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                          <mml:mi>MLTT<\/mml:mi>\n                        <\/mml:math>\n                      <\/jats:alternatives>\n                    <\/jats:inline-formula>\n                    , we\u00a0show that they inductively approximate idealized functional objects as decision trees, realizing a generalized\u00a0form of continuity. We materialize this intuition in\n                    <jats:inline-formula>\n                      <jats:alternatives>\n                        <jats:tex-math>$$\\textsf{MLTT}^{\\textsf{F}}$$<\/jats:tex-math>\n                        <mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                          <mml:msup>\n                            <mml:mi>MLTT<\/mml:mi>\n                            <mml:mi>F<\/mml:mi>\n                          <\/mml:msup>\n                        <\/mml:math>\n                      <\/jats:alternatives>\n                    <\/jats:inline-formula>\n                    , a case-study sheaf extension\u00a0of\n                    <jats:inline-formula>\n                      <jats:alternatives>\n                        <jats:tex-math>$$\\textsf{MLTT}$$<\/jats:tex-math>\n                        <mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                          <mml:mi>MLTT<\/mml:mi>\n                        <\/mml:math>\n                      <\/jats:alternatives>\n                    <\/jats:inline-formula>\n                    with a Cohen real and leverage it to\u00a0show uniform continuity of all\n                    <jats:inline-formula>\n                      <jats:alternatives>\n                        <jats:tex-math>$$\\textsf{MLTT}$$<\/jats:tex-math>\n                        <mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                          <mml:mi>MLTT<\/mml:mi>\n                        <\/mml:math>\n                      <\/jats:alternatives>\n                    <\/jats:inline-formula>\n                    functionals of type\n                    <jats:inline-formula>\n                      <jats:alternatives>\n                        <jats:tex-math>$$({\\mathbb {N}}\\rightarrow {\\mathbb {B}}) \\rightarrow {\\mathbb {N}}$$<\/jats:tex-math>\n                        <mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                          <mml:mrow>\n                            <mml:mo>(<\/mml:mo>\n                            <mml:mi>N<\/mml:mi>\n                            <mml:mo>\u2192<\/mml:mo>\n                            <mml:mi>B<\/mml:mi>\n                            <mml:mo>)<\/mml:mo>\n                            <mml:mo>\u2192<\/mml:mo>\n                            <mml:mi>N<\/mml:mi>\n                          <\/mml:mrow>\n                        <\/mml:math>\n                      <\/jats:alternatives>\n                    <\/jats:inline-formula>\n                    . The latter results were mechanized in Rocq.\n                  <\/jats:p>","DOI":"10.1007\/978-3-032-22720-1_4","type":"book-chapter","created":{"date-parts":[[2026,4,9]],"date-time":"2026-04-09T15:30:23Z","timestamp":1775748623000},"page":"72-103","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["In Cantor Space No One Can Hear You Stream"],"prefix":"10.1007","author":[{"given":"Martin","family":"Baillon","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Assia","family":"Mahboubi","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Pierre-Marie","family":"P\u00e9drot","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2026,4,10]]},"reference":[{"key":"4_CR1","doi-asserted-by":"publisher","unstructured":"Abel, A., Aehlig, K., Dybjer, P.: Normalization by evaluation for martin-l\u00f6f type theory with one universe. In: Fiore, M. (ed.) Proceedings of the 23rd Conference on the Mathematical Foundations of Programming Semantics, MFPS 2007, New Orleans, LA, USA, April 11-14, 2007. Electronic Notes in Theoretical Computer Science, vol.\u00a0173, pp. 17\u201339. Elsevier (2007). https:\/\/doi.org\/10.1016\/J.ENTCS.2007.02.025, https:\/\/doi.org\/10.1016\/j.entcs.2007.02.025","DOI":"10.1016\/J.ENTCS.2007.02.025"},{"key":"4_CR2","doi-asserted-by":"publisher","unstructured":"Abel, A., \u00d6hman, J., Vezzosi, A.: Decidability of conversion for type theory in type theory. Proc. ACM Program. Lang. 2(POPL) (dec 2017). https:\/\/doi.org\/10.1145\/3158111, https:\/\/doi.org\/10.1145\/3158111","DOI":"10.1145\/3158111"},{"key":"4_CR3","doi-asserted-by":"publisher","unstructured":"Adjedj, A., Lennon-Bertrand, M., Maillard, K., P\u00e9drot, P., Pujet, L.: Martin-l\u00f6f \u00e0 la coq. In: Timany, A., Traytel, D., Pientka, B., Blazy, S. (eds.) Proceedings of the 13th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2024, London, UK, January 15-16, 2024. pp. 230\u2013245. ACM (2024). https:\/\/doi.org\/10.1145\/3636501.3636951, https:\/\/doi.org\/10.1145\/3636501.3636951","DOI":"10.1145\/3636501.3636951"},{"key":"4_CR4","doi-asserted-by":"publisher","unstructured":"Ahman, D.: Handling fibred algebraic effects. Proc. ACM Program. Lang. 2(POPL), 7:1\u20137:29 (2018). https:\/\/doi.org\/10.1145\/3158095, https:\/\/doi.org\/10.1145\/3158095","DOI":"10.1145\/3158095"},{"key":"4_CR5","doi-asserted-by":"publisher","unstructured":"Ahman, D., Ghani, N., Plotkin, G.D.: Dependent types and fibred computational effects. In: Jacobs, B., L\u00f6ding, C. (eds.) Foundations of Software Science and Computation Structures - 19th International Conference, FOSSACS 2016, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2016, Eindhoven, The Netherlands, April 2-8, 2016, Proceedings. Lecture Notes in Computer Science, vol.\u00a09634, pp. 36\u201354. Springer (2016). https:\/\/doi.org\/10.1007\/978-3-662-49630-5_3, https:\/\/doi.org\/10.1007\/978-3-662-49630-5_3","DOI":"10.1007\/978-3-662-49630-5_3"},{"key":"4_CR6","doi-asserted-by":"publisher","unstructured":"Altenkirch, T., Capriotti, P., Dijkstra, G., Kraus, N., Forsberg, F.N.: Quotient inductive-inductive types. In: Baier, C., Lago, U.D. (eds.) Foundations of Software Science and Computation Structures - 21st International Conference, FOSSACS 2018, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2018, Thessaloniki, Greece, April 14-20, 2018, Proceedings. Lecture Notes in Computer Science, vol. 10803, pp. 293\u2013310. Springer (2018). https:\/\/doi.org\/10.1007\/978-3-319-89366-2_16, https:\/\/doi.org\/10.1007\/978-3-319-89366-2_16","DOI":"10.1007\/978-3-319-89366-2_16"},{"key":"4_CR7","doi-asserted-by":"publisher","unstructured":"Altenkirch, T., McBride, C., Swierstra, W.: Observational equality, now! In: Stump, A., Xi, H. (eds.) Proceedings of the ACM Workshop Programming Languages meets Program Verification, PLPV 2007, Freiburg, Germany, October 5, 2007. pp. 57\u201368. ACM (2007). https:\/\/doi.org\/10.1145\/1292597.1292608, https:\/\/doi.org\/10.1145\/1292597.1292608","DOI":"10.1145\/1292597.1292608"},{"key":"4_CR8","doi-asserted-by":"publisher","unstructured":"Anand, A., Rahli, V.: Towards a formally verified proof assistant. In: Klein, G., Gamboa, R. (eds.) Interactive Theorem Proving - 5th International Conference, ITP 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 14-17, 2014. Proceedings. Lecture Notes in Computer Science, vol.\u00a08558, pp. 27\u201344. Springer (2014). https:\/\/doi.org\/10.1007\/978-3-319-08970-6_3, https:\/\/doi.org\/10.1007\/978-3-319-08970-6_3","DOI":"10.1007\/978-3-319-08970-6_3"},{"key":"4_CR9","doi-asserted-by":"crossref","unstructured":"Aschenbrenner, M., Dries, L.v.d., Hoeven, J.v.d.: Asymptotic Differential Algebra and Model Theory of Transseries. No.\u00a0195 in Annals of Mathematics studies, Princeton University Press (2017), http:\/\/arxiv.org\/abs\/1509.02588","DOI":"10.23943\/princeton\/9780691175423.001.0001"},{"key":"4_CR10","unstructured":"Authors, T.S.P.: Stacks project, https:\/\/stacks.math.columbia.edu\/"},{"key":"4_CR11","doi-asserted-by":"publisher","unstructured":"Baillon, M., Forster, Y., Mahboubi, A., P\u00e9drot, P.M., Piquerez, M.: A Zoo of Continuity Properties in Constructive Type Theory. In: Fern\u00e1ndez, M. (ed.) 10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025). Leibniz International Proceedings in Informatics (LIPIcs), vol.\u00a0337, pp. 9:1\u20139:20. Schloss Dagstuhl \u2013 Leibniz-Zentrum f\u00fcr Informatik, Dagstuhl, Germany (2025). https:\/\/doi.org\/10.4230\/LIPIcs.FSCD.2025.9, https:\/\/drops.dagstuhl.de\/entities\/document\/10.4230\/LIPIcs.FSCD.2025.9","DOI":"10.4230\/LIPIcs.FSCD.2025.9"},{"key":"4_CR12","doi-asserted-by":"publisher","unstructured":"Baillon, M., Mahboubi, A., P\u00e9drot, P.: Gardening with the pythia A model of continuity in a dependent setting. In: Manea, F., Simpson, A. (eds.) 30th EACSL Annual Conference on Computer Science Logic, CSL 2022, February 14-19, 2022, G\u00f6ttingen, Germany (Virtual Conference). LIPIcs, vol.\u00a0216, pp. 5:1\u20135:18. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2022). https:\/\/doi.org\/10.4230\/LIPICS.CSL.2022.5, https:\/\/doi.org\/10.4230\/LIPIcs.CSL.2022.5","DOI":"10.4230\/LIPICS.CSL.2022.5"},{"key":"4_CR13","doi-asserted-by":"publisher","unstructured":"Bernardy, J., Lasson, M.: Realizability and parametricity in pure type systems. In: Hofmann, M. (ed.) Foundations of Software Science and Computational Structures - 14th International Conference, FOSSACS 2011, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2011, Saarbr\u00fccken, Germany, March 26-April 3, 2011. Proceedings. Lecture Notes in Computer Science, vol.\u00a06604, pp. 108\u2013122. Springer (2011). https:\/\/doi.org\/10.1007\/978-3-642-19805-2_8, https:\/\/doi.org\/10.1007\/978-3-642-19805-2_8","DOI":"10.1007\/978-3-642-19805-2_8"},{"key":"4_CR14","unstructured":"Blechschmidt, I.: Using the internal language of toposes in algebraic geometry. Ph.D. thesis, Augsburg University (2017), https:\/\/rawgit.com\/iblech\/internal-methods\/master\/notes.pdf"},{"key":"4_CR15","doi-asserted-by":"publisher","unstructured":"Brede, N., Herbelin, H.: On the logical structure of choice and bar induction principles. In: 36th Annual ACM\/IEEE Symposium on Logic in Computer Science, LICS 2021, Rome, Italy, June 29 - July 2, 2021. pp. 1\u201313. IEEE (2021). https:\/\/doi.org\/10.1109\/LICS52264.2021.9470523, https:\/\/doi.org\/10.1109\/LICS52264.2021.9470523","DOI":"10.1109\/LICS52264.2021.9470523"},{"key":"4_CR16","doi-asserted-by":"publisher","unstructured":"Cavallo, E., M\u00f6rtberg, A., Swan, A.W.: Unifying cubical models of univalent type theory. In: Fern\u00e1ndez, M., Muscholl, A. (eds.) 28th EACSL Annual Conference on Computer Science Logic, CSL 2020, January 13-16, 2020, Barcelona, Spain. LIPIcs, vol.\u00a0152, pp. 14:1\u201314:17. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2020). https:\/\/doi.org\/10.4230\/LIPICS.CSL.2020.14, https:\/\/doi.org\/10.4230\/LIPIcs.CSL.2020.14","DOI":"10.4230\/LIPICS.CSL.2020.14"},{"key":"4_CR17","doi-asserted-by":"publisher","unstructured":"Cohen, L., Rahli, V.: Realizing continuity using stateful computations. In: Klin, B., Pimentel, E. (eds.) 31st EACSL Annual Conference on Computer Science Logic, CSL 2023, February 13-16, 2023, Warsaw, Poland. LIPIcs, vol.\u00a0252, pp. 15:1\u201315:18. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2023). https:\/\/doi.org\/10.4230\/LIPICS.CSL.2023.15, https:\/\/doi.org\/10.4230\/LIPIcs.CSL.2023.15","DOI":"10.4230\/LIPICS.CSL.2023.15"},{"key":"4_CR18","doi-asserted-by":"publisher","unstructured":"Cohen, L., Rahli, V.: $$\\text{TT}^{\\Box }_{\\cal{C}}$$: A family of extensional type theories with effectful realizers of continuity. Logical Methods in Computer Science Volume 20, Issue 2, 18 (Jun 2024). https:\/\/doi.org\/10.46298\/lmcs-20(2:18)2024, https:\/\/lmcs.episciences.org\/11666","DOI":"10.46298\/lmcs-20(2:18)2024"},{"key":"4_CR19","doi-asserted-by":"publisher","unstructured":"Cohen, L., da\u00a0Rocha\u00a0Paiva, B., Rahli, V., Tosun, A.: Inductive continuity via Brouwer trees. In: Leroux, J., Lombardy, S., Peleg, D. (eds.) 48th International Symposium on Mathematical Foundations of Computer Science, MFCS 2023, August 28 to September 1, 2023, Bordeaux, France. LIPIcs, vol.\u00a0272, pp. 37:1\u201337:16. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2023). https:\/\/doi.org\/10.4230\/LIPICS.MFCS.2023.37, https:\/\/doi.org\/10.4230\/LIPIcs.MFCS.2023.37","DOI":"10.4230\/LIPICS.MFCS.2023.37"},{"key":"4_CR20","doi-asserted-by":"publisher","unstructured":"Coquand, T.: Dynamical method in algebra: A survey. In: Mayer, M.C., Pirri, F. (eds.) Automated Reasoning with Analytic Tableaux and Related Methods, International Conference, TABLEAUX 2003, Rome, Italy, September 9-12, 2003. Proceedings. Lecture Notes in Computer Science, vol.\u00a02796, p.\u00a02. Springer (2003). https:\/\/doi.org\/10.1007\/978-3-540-45206-5_2, https:\/\/doi.org\/10.1007\/978-3-540-45206-5_2","DOI":"10.1007\/978-3-540-45206-5_2"},{"key":"4_CR21","unstructured":"Coquand, T.: A completeness proof for geometrical logic. Logic, Methodology and Philosophy of Sciences (2005)"},{"key":"4_CR22","unstructured":"Coquand, T., Danielsson, N.A., Escard\u00f3, M.H., Norell, U., Xu, C.: Negative consistent axioms can be postulated without loss of canonicity (2013), https:\/\/martinescardo.github.io\/papers\/negative-axioms.pdf"},{"key":"4_CR23","doi-asserted-by":"publisher","unstructured":"Coquand, T., Jaber, G.: A note on forcing and type theory. Fundam. Informaticae 100(1-4), 43\u201352 (2010). https:\/\/doi.org\/10.3233\/FI-2010-262, https:\/\/doi.org\/10.3233\/FI-2010-262","DOI":"10.3233\/FI-2010-262"},{"key":"4_CR24","doi-asserted-by":"publisher","unstructured":"Coquand, T., Jaber, G.: A computational interpretation of forcing in type theory. In: Dybjer, P., Lindstr\u00f6m, S., Palmgren, E., Sundholm, G. (eds.) Epistemology versus Ontology - Essays on the Philosophy and Foundations of Mathematics in Honour of Per Martin-L\u00f6f, Logic, Epistemology, and the Unity of Science, vol.\u00a027, pp. 203\u2013213. Springer (2012). https:\/\/doi.org\/10.1007\/978-94-007-4435-6_10, https:\/\/doi.org\/10.1007\/978-94-007-4435-6_10","DOI":"10.1007\/978-94-007-4435-6_10"},{"key":"4_CR25","doi-asserted-by":"publisher","unstructured":"Coquand, T., Ruch, F., Sattler, C.: Constructive sheaf models of type theory. Math. Struct. Comput. Sci. 31(9), 979\u20131002 (2021). https:\/\/doi.org\/10.1017\/S0960129521000359, https:\/\/doi.org\/10.1017\/S0960129521000359","DOI":"10.1017\/S0960129521000359"},{"key":"4_CR26","doi-asserted-by":"publisher","unstructured":"Coste, M., Lombardi, H., Roy, M.: Dynamical method in algebra: effective nullstellens\u00e4tze. Ann. Pure Appl. Log. 111(3), 203\u2013256 (2001). https:\/\/doi.org\/10.1016\/S0168-0072(01)00026-4, https:\/\/doi.org\/10.1016\/S0168-0072(01)00026-4","DOI":"10.1016\/S0168-0072(01)00026-4"},{"key":"4_CR27","doi-asserted-by":"crossref","unstructured":"Dora, J.D., Dicrescenzo, C., Duval, D.: About a new method for computing in algebraic number fields. In: European Conference on Computer Algebra (2). Lecture Notes in Computer Science, vol.\u00a0204, pp. 289\u2013290. Springer (1985)","DOI":"10.1007\/3-540-15984-3_279"},{"key":"4_CR28","doi-asserted-by":"publisher","unstructured":"Duval, D., Reynaud, J.C.: Sketches and computation \u2013 ii: dynamic evaluation and applications. Mathematical Structures in Computer Science 4(2), 239\u2013271 (1994). https:\/\/doi.org\/10.1017\/S096012950000044X","DOI":"10.1017\/S096012950000044X"},{"key":"4_CR29","doi-asserted-by":"publisher","unstructured":"Escard\u00f3, M., Xu, C.: A constructive manifestation of the Kleene-Kreisel continuous functionals. Ann. Pure Appl. Log. 167(9), 770\u2013793 (2016). https:\/\/doi.org\/10.1016\/J.APAL.2016.04.011, https:\/\/doi.org\/10.1016\/j.apal.2016.04.011","DOI":"10.1016\/J.APAL.2016.04.011"},{"key":"4_CR30","doi-asserted-by":"publisher","unstructured":"Escard\u00f3, M.H., da\u00a0Rocha\u00a0Paiva, B., Rahli, V., Tosun, A.: Internal effectful forcing in system T. In: Fern\u00e1ndez, M. (ed.) 10th International Conference on Formal Structures for Computation and Deduction, FSCD 2025, July 14-20, 2025, Birmingham, UK. LIPIcs, vol.\u00a0337, pp. 19:1\u201319:17. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2025). https:\/\/doi.org\/10.4230\/LIPICS.FSCD.2025.19, https:\/\/doi.org\/10.4230\/LIPIcs.FSCD.2025.19","DOI":"10.4230\/LIPICS.FSCD.2025.19"},{"key":"4_CR31","doi-asserted-by":"publisher","unstructured":"Escard\u00f3, M.H.: Continuity of G\u00f6del\u2019s System T definable functionals via effectful forcing. Proceedings of the Twenty-ninth Conference on the Mathematical Foundations of Programming Semantics, MFPS 2013, New Orleans, LA, USA, June 23-25, 2013 (2013). https:\/\/doi.org\/10.1016\/j.entcs.2013.09.010, https:\/\/doi.org\/10.1016\/j.entcs.2013.09.010","DOI":"10.1016\/j.entcs.2013.09.010"},{"key":"4_CR32","doi-asserted-by":"publisher","unstructured":"Escard\u00f3, M.H., Xu, C.: The inconsistency of a brouwerian continuity principle with the Curry-Howard interpretation. 13th International Conference on Typed Lambda Calculi and Applications, TLCA 2015, July 1-3, 2015, Warsaw, Poland (2015). https:\/\/doi.org\/10.4230\/LIPIcs.TLCA.2015.153, https:\/\/doi.org\/10.4230\/LIPIcs.TLCA.2015.153","DOI":"10.4230\/LIPIcs.TLCA.2015.153"},{"key":"4_CR33","doi-asserted-by":"publisher","unstructured":"Fiore, M.P., Pitts, A.M., Steenkamp, S.C.: Quotients, inductive types, and quotient inductive types. Log. Methods Comput. Sci. 18(2) (2022). https:\/\/doi.org\/10.46298\/LMCS-18(2:15)2022, https:\/\/doi.org\/10.46298\/lmcs-18(2:15)2022","DOI":"10.46298\/LMCS-18(2:15)2022"},{"key":"4_CR34","doi-asserted-by":"publisher","unstructured":"Fujiwara, M., Kawai, T.: Equivalence of bar induction and bar recursion for continuous functions with continuous moduli. Ann. Pure Appl. Log. 170(8), 867\u2013890 (2019). https:\/\/doi.org\/10.1016\/J.APAL.2019.04.001, https:\/\/doi.org\/10.1016\/j.apal.2019.04.001","DOI":"10.1016\/J.APAL.2019.04.001"},{"key":"4_CR35","doi-asserted-by":"publisher","unstructured":"Gilbert, G., Cockx, J., Sozeau, M., Tabareau, N.: Definitional proof-irrelevance without K. Proc. ACM Program. Lang. 3(POPL), 3:1\u20133:28 (2019). https:\/\/doi.org\/10.1145\/3290316, https:\/\/doi.org\/10.1145\/3290316","DOI":"10.1145\/3290316"},{"key":"4_CR36","unstructured":"Girard, J.Y., Taylor, P., Lafont, Y.: Proofs and Types. Cambridge University Press, Cambridge (1989), http:\/\/www.worldcat.org\/isbn\/0521371813"},{"key":"4_CR37","unstructured":"Gratzer, D.: An inductive-recursive universe generic for small families. CoRR abs\/2202.05529 (2022), https:\/\/arxiv.org\/abs\/2202.05529"},{"key":"4_CR38","doi-asserted-by":"publisher","unstructured":"Gratzer, D., Kavvos, G.A., Nuyts, A., Birkedal, L.: Multimodal dependent type theory. In: Hermanns, H., Zhang, L., Kobayashi, N., Miller, D. (eds.) LICS \u201920: 35th Annual ACM\/IEEE Symposium on Logic in Computer Science, Saarbr\u00fccken, Germany, July 8-11, 2020. pp. 492\u2013506. ACM (2020). https:\/\/doi.org\/10.1145\/3373718.3394736, https:\/\/doi.org\/10.1145\/3373718.3394736","DOI":"10.1145\/3373718.3394736"},{"key":"4_CR39","unstructured":"Gratzer, D., Shulman, M., Sterling, J.: Strict universes for grothendieck topoi. CoRR abs\/2202.12012 (2022), https:\/\/arxiv.org\/abs\/2202.12012"},{"key":"4_CR40","doi-asserted-by":"publisher","unstructured":"Griffin, T.: A formulae-as-types notion of control. In: Allen, F.E. (ed.) Conference Record of the Seventeenth Annual ACM Symposium on Principles of Programming Languages, San Francisco, California, USA, January 1990. pp. 47\u201358. ACM Press (1990). https:\/\/doi.org\/10.1145\/96709.96714, https:\/\/doi.org\/10.1145\/96709.96714","DOI":"10.1145\/96709.96714"},{"key":"4_CR41","doi-asserted-by":"publisher","unstructured":"Hancock, P.G., McBride, C., Ghani, N., Malatesta, L., Altenkirch, T.: Small induction recursion. In: Hasegawa, M. (ed.) Typed Lambda Calculi and Applications, 11th International Conference, TLCA 2013, Eindhoven, The Netherlands, June 26-28, 2013. Proceedings. Lecture Notes in Computer Science, vol.\u00a07941, pp. 156\u2013172. Springer (2013). https:\/\/doi.org\/10.1007\/978-3-642-38946-7_13, https:\/\/doi.org\/10.1007\/978-3-642-38946-7_13","DOI":"10.1007\/978-3-642-38946-7_13"},{"key":"4_CR42","unstructured":"Kaposi, A.: Towards quotient inductive-inductive-recursive types. In: 29th International Conference on Types for Proofs and Programs, TYPES 2023. pp. 124\u2013126 (2023), https:\/\/types2023.webs.upv.es\/TYPES2023.pdf"},{"key":"4_CR43","doi-asserted-by":"publisher","unstructured":"Kaposi, A., Kov\u00e1cs, A., Altenkirch, T.: Constructing quotient inductive-inductive types. Proc. ACM Program. Lang. 3(POPL), 2:1\u20132:24 (2019). https:\/\/doi.org\/10.1145\/3290315, https:\/\/doi.org\/10.1145\/3290315","DOI":"10.1145\/3290315"},{"key":"4_CR44","doi-asserted-by":"publisher","unstructured":"Kiselyov, O., Shan, C.: Delimited continuations in operating systems. In: Kokinov, B.N., Richardson, D.C., Roth-Berghofer, T., Vieu, L. (eds.) Modeling and Using Context, 6th International and Interdisciplinary Conference, CONTEXT 2007, Roskilde, Denmark, August 20-24, 2007, Proceedings. Lecture Notes in Computer Science, vol.\u00a04635, pp. 291\u2013302. Springer (2007). https:\/\/doi.org\/10.1007\/978-3-540-74255-5_22, https:\/\/doi.org\/10.1007\/978-3-540-74255-5_22","DOI":"10.1007\/978-3-540-74255-5_22"},{"key":"4_CR45","doi-asserted-by":"publisher","unstructured":"Kleene, S.C.: Recursive Functionals and Quantifiers of Finite Types I. Transactions of the American Mathematical Society 91(1), \u00a01 (Apr 1959). https:\/\/doi.org\/10.2307\/1993145, https:\/\/www.jstor.org\/stable\/1993145?origin=crossref","DOI":"10.2307\/1993145"},{"key":"4_CR46","doi-asserted-by":"publisher","unstructured":"Lombardi, H., Quitt\u00e9, C., Yengui, I.: Hidden constructions in abstract algebra. VI. The theorem of Maroscia and Brewer & Costa. J. Pure Appl. Algebra 212(7), 1575\u20131582 (2008). https:\/\/doi.org\/10.1016\/j.jpaa.2007.10.009, https:\/\/doi.org\/10.1016\/j.jpaa.2007.10.009","DOI":"10.1016\/j.jpaa.2007.10.009"},{"key":"4_CR47","unstructured":"Mac\u00a0Lane, S., Moerdijk, I.: Sheaves in Geometry and Logic a First Introduction to Topos Theory. Springer New York, New York, NY (1992), http:\/\/link.springer.com\/book\/10.1007\/978-1-4612-0927-0"},{"key":"4_CR48","doi-asserted-by":"crossref","unstructured":"Mannaa, B., Coquand, T.: A sheaf model of the algebraic closure. In: CL&C. EPTCS, vol.\u00a0164, pp. 18\u201332 (2014)","DOI":"10.4204\/EPTCS.164.2"},{"key":"4_CR49","doi-asserted-by":"publisher","unstructured":"Miquel, A.: Forcing as a program transformation. In: Proceedings of the 26th Annual IEEE Symposium on Logic in Computer Science, LICS 2011, June 21-24, 2011, Toronto, Ontario, Canada. pp. 197\u2013206. IEEE Computer Society (2011). https:\/\/doi.org\/10.1109\/LICS.2011.47, https:\/\/doi.org\/10.1109\/LICS.2011.47","DOI":"10.1109\/LICS.2011.47"},{"key":"4_CR50","doi-asserted-by":"publisher","unstructured":"Palmgren, E.: From intuitionistic to point-free topology: on the foundation of homotopy theory. In: Logicism, intuitionism, and formalism, Synth. Libr., vol.\u00a0341, pp. 237\u2013253. Springer, Dordrecht (2009). https:\/\/doi.org\/10.1007\/978-1-4020-8926-8_12, https:\/\/doi.org\/10.1007\/978-1-4020-8926-8_12","DOI":"10.1007\/978-1-4020-8926-8_12"},{"key":"4_CR51","unstructured":"Paulin-Mohring, C.: D\u00e9finitions Inductives en Th\u00e9orie des Types. Accreditation to supervise research, Universit\u00e9 Claude Bernard - Lyon I (Dec 1996), https:\/\/theses.hal.science\/tel-00431817"},{"key":"4_CR52","doi-asserted-by":"publisher","unstructured":"P\u00e9drot, P.: Russian constructivism in a prefascist theory. In: Hermanns, H., Zhang, L., Kobayashi, N., Miller, D. (eds.) LICS \u201920: 35th Annual ACM\/IEEE Symposium on Logic in Computer Science, Saarbr\u00fccken, Germany, July 8-11, 2020. pp. 782\u2013794. ACM (2020). https:\/\/doi.org\/10.1145\/3373718.3394740, https:\/\/doi.org\/10.1145\/3373718.3394740","DOI":"10.1145\/3373718.3394740"},{"key":"4_CR53","doi-asserted-by":"publisher","unstructured":"P\u00e9drot, P., Tabareau, N.: An effectful way to eliminate addiction to dependence. In: 32nd Annual ACM\/IEEE Symposium on Logic in Computer Science, LICS 2017, Reykjavik, Iceland, June 20-23, 2017. pp. 1\u201312. IEEE Computer Society (2017). https:\/\/doi.org\/10.1109\/LICS.2017.8005113, https:\/\/doi.org\/10.1109\/LICS.2017.8005113","DOI":"10.1109\/LICS.2017.8005113"},{"key":"4_CR54","doi-asserted-by":"publisher","unstructured":"P\u00e9drot, P., Tabareau, N.: The fire triangle: how to mix substitution, dependent elimination, and effects. Proc. ACM Program. Lang. 4(POPL), 58:1\u201358:28 (2020). https:\/\/doi.org\/10.1145\/3371126, https:\/\/doi.org\/10.1145\/3371126","DOI":"10.1145\/3371126"},{"key":"4_CR55","unstructured":"Poirier, H.: La vraie nature de l\u2019intelligence. Science & Vie 1013, 38\u201357 (February 2002)"},{"key":"4_CR56","doi-asserted-by":"publisher","unstructured":"Rahli, V., Bickford, M.: Validating brouwer\u2019s continuity principle for numbers using named exceptions. Math. Struct. Comput. Sci. 28(6), 942\u2013990 (2018). https:\/\/doi.org\/10.1017\/S0960129517000172, https:\/\/doi.org\/10.1017\/S0960129517000172","DOI":"10.1017\/S0960129517000172"},{"key":"4_CR57","doi-asserted-by":"publisher","unstructured":"Rahli, V., Bickford, M., Cohen, L., Constable, R.L.: Bar induction is compatible with constructive type theory. J. ACM 66(2), 13:1\u201313:35 (2019). https:\/\/doi.org\/10.1145\/3305261, https:\/\/doi.org\/10.1145\/3305261","DOI":"10.1145\/3305261"},{"key":"4_CR58","doi-asserted-by":"publisher","unstructured":"Rahli, V., Bickford, M., Constable, R.L.: Bar induction: The good, the bad, and the ugly. In: 32nd Annual ACM\/IEEE Symposium on Logic in Computer Science, LICS 2017, Reykjavik, Iceland, June 20-23, 2017. pp. 1\u201312. IEEE Computer Society (2017). https:\/\/doi.org\/10.1109\/LICS.2017.8005074, https:\/\/doi.org\/10.1109\/LICS.2017.8005074","DOI":"10.1109\/LICS.2017.8005074"},{"key":"4_CR59","doi-asserted-by":"publisher","unstructured":"Rijke, E., Shulman, M., Spitters, B.: Modalities in homotopy type theory. Log. Methods Comput. Sci. 16(1) (2020). https:\/\/doi.org\/10.23638\/LMCS-16(1:2)2020, https:\/\/doi.org\/10.23638\/LMCS-16(1:2)2020","DOI":"10.23638\/LMCS-16(1:2)2020"},{"key":"4_CR60","doi-asserted-by":"publisher","unstructured":"Serre, J.P.: Faisceaux alg\u00e9briques coh\u00e9rents. Ann. of Math. (2) 61, 197\u2013278 (1955). https:\/\/doi.org\/10.2307\/1969915, https:\/\/doi.org\/10.2307\/1969915","DOI":"10.2307\/1969915"},{"key":"4_CR61","doi-asserted-by":"crossref","unstructured":"Sherman, B., Sciarappa, L., Chlipala, A., Carbin, M.: Computable decision making on the reals and other spaces: via partiality and nondeterminism. In: LICS. pp. 859\u2013868. ACM (2018)","DOI":"10.1145\/3209108.3209193"},{"key":"4_CR62","doi-asserted-by":"publisher","unstructured":"Sterling, J.: Higher order functions and brouwer\u2019s thesis. J. Funct. Program. 31, \u00a0e11 (2021). https:\/\/doi.org\/10.1017\/S0956796821000095, https:\/\/doi.org\/10.1017\/S0956796821000095","DOI":"10.1017\/S0956796821000095"},{"key":"4_CR63","doi-asserted-by":"publisher","unstructured":"Sterling, J.: First Steps in Synthetic Tait Computability: The Objective Metatheory of Cubical Type Theory. Ph.D. thesis, Carnegie Mellon University, USA (2022). https:\/\/doi.org\/10.1184\/R1\/19632681.V1, https:\/\/doi.org\/10.1184\/r1\/19632681.v1","DOI":"10.1184\/R1\/19632681.V1"},{"key":"4_CR64","doi-asserted-by":"crossref","unstructured":"Streicher, T.: Universes in toposes. In: Crosilla, L., Schuster, P.M. (eds.) From sets and types to topology and analysis - Towards practicable foundations for constructive mathematics, Oxford logic guides, vol.\u00a048. Oxford University Press (2005)","DOI":"10.1093\/acprof:oso\/9780198566519.003.0005"},{"key":"4_CR65","unstructured":"Troelstra, A., van Dalen, D.: Constructivism in Mathematics An Introduction, vol.\u00a0121. Elsevier (1988)"},{"key":"4_CR66","unstructured":"Univalent Foundations Program, T.: Homotopy Type Theory: Univalent Foundations of Mathematics. https:\/\/homotopytypetheory.org\/book, Institute for Advanced Study (2013)"},{"key":"4_CR67","unstructured":"Werner, B.: Une Th\u00e9orie des Constructions Inductives. Ph.D. thesis, Paris Diderot University, France (1994), https:\/\/tel.archives-ouvertes.fr\/tel-00196524"},{"key":"4_CR68","doi-asserted-by":"publisher","unstructured":"Xia, L., Zakowski, Y., He, P., Hur, C., Malecha, G., Pierce, B.C., Zdancewic, S.: Interaction trees: representing recursive and impure programs in coq. Proc. ACM Program. Lang. 4(POPL), 51:1\u201351:32 (2020). https:\/\/doi.org\/10.1145\/3371119, https:\/\/doi.org\/10.1145\/3371119","DOI":"10.1145\/3371119"},{"key":"4_CR69","doi-asserted-by":"publisher","unstructured":"Xu, C., Escard\u00f3, M.H.: A constructive model of uniform continuity. In: Hasegawa, M. (ed.) Typed Lambda Calculi and Applications, 11th International Conference, TLCA 2013, Eindhoven, The Netherlands, June 26-28, 2013. Proceedings. Lecture Notes in Computer Science, vol.\u00a07941, pp. 236\u2013249. Springer (2013). https:\/\/doi.org\/10.1007\/978-3-642-38946-7_18, https:\/\/doi.org\/10.1007\/978-3-642-38946-7_18","DOI":"10.1007\/978-3-642-38946-7_18"}],"container-title":["Lecture Notes in Computer Science","Programming Languages and Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-032-22720-1_4","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,4,30]],"date-time":"2026-04-30T19:23:37Z","timestamp":1777577017000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-032-22720-1_4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026]]},"ISBN":["9783032227195","9783032227201"],"references-count":69,"URL":"https:\/\/doi.org\/10.1007\/978-3-032-22720-1_4","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2026]]},"assertion":[{"value":"10 April 2026","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"ESOP","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"European Symposium on Programming","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Turin","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Italy","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2026","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"11 April 2026","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"16 April 2026","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"35","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"esop2026","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/etaps.org\/about\/esop\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}