{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,26]],"date-time":"2025-03-26T20:39:40Z","timestamp":1743021580592,"version":"3.40.3"},"publisher-location":"Cham","reference-count":36,"publisher":"Springer Nature Switzerland","isbn-type":[{"type":"print","value":"9783031617157"},{"type":"electronic","value":"9783031617164"}],"license":[{"start":{"date-parts":[[2024,1,1]],"date-time":"2024-01-01T00:00:00Z","timestamp":1704067200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2024,1,1]],"date-time":"2024-01-01T00:00:00Z","timestamp":1704067200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2024]]},"DOI":"10.1007\/978-3-031-61716-4_16","type":"book-chapter","created":{"date-parts":[[2024,5,29]],"date-time":"2024-05-29T03:47:52Z","timestamp":1716954472000},"page":"241-256","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["The Interval Domain in\u00a0Homotopy Type Theory"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-1146-4161","authenticated-orcid":false,"given":"Niels","family":"van der Weide","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0001-5864-7278","authenticated-orcid":false,"given":"Dan","family":"Frumin","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2024,5,22]]},"reference":[{"key":"16_CR1","doi-asserted-by":"crossref","unstructured":"Abramsky, S., Jung, A.: Domain theory (corrected and expanded version). In: Handbook of Logic in Computer Science, pp. 1\u2013168. Oxford University Press (1994)","DOI":"10.1093\/oso\/9780198537625.003.0001"},{"key":"16_CR2","unstructured":"Ambridge, T.W.: Exact Real Search: Formalised Optimisation and Regression in Constructive Univalent Mathematics (2024). https:\/\/doi.org\/10.48550\/arXiv.2401.09270"},{"issue":"8","key":"16_CR3","doi-asserted-by":"publisher","first-page":"568","DOI":"10.1016\/j.scico.2007.09.002","volume":"74","author":"P Audebaud","year":"2009","unstructured":"Audebaud, P., Paulin-Mohring, C.: Proofs of randomized algorithms in Coq. Sci. Comput. Program. 74(8), 568\u2013589 (2009). https:\/\/doi.org\/10.1016\/j.scico.2007.09.002","journal-title":"Sci. Comput. Program."},{"issue":"3","key":"16_CR4","doi-asserted-by":"publisher","first-page":"251","DOI":"10.1016\/j.apal.2008.09.025","volume":"159","author":"A Bauer","year":"2009","unstructured":"Bauer, A., Kavkler, I.: A constructive theory of continuous domains suitable for implementation. Ann. Pure Appl. Logic 159(3), 251\u2013267 (2009). https:\/\/doi.org\/10.1016\/j.apal.2008.09.025","journal-title":"Ann. Pure Appl. Logic"},{"issue":"4","key":"16_CR5","doi-asserted-by":"publisher","first-page":"757","DOI":"10.1017\/S0960129509007695","volume":"19","author":"A Bauer","year":"2009","unstructured":"Bauer, A., Taylor, P.: The Dedekind reals in abstract Stone duality. Math. Struct. Comput. Sci. 19(4), 757\u2013838 (2009). https:\/\/doi.org\/10.1017\/S0960129509007695","journal-title":"Math. Struct. Comput. Sci."},{"issue":"10","key":"16_CR6","doi-asserted-by":"publisher","first-page":"1301","DOI":"10.1017\/S0960129521000165","volume":"31","author":"ME Bidlingmaier","year":"2021","unstructured":"Bidlingmaier, M.E., Faissole, F., Spitters, B.: Synthetic topology in homotopy type theory for probabilistic programming. Math. Struct. Comput. Sci. 31(10), 1301\u20131329 (2021). https:\/\/doi.org\/10.1017\/S0960129521000165","journal-title":"Math. Struct. Comput. Sci."},{"key":"16_CR7","unstructured":"Bishop, E.: Foundations of Constructive Analysis. McGraw-Hill (1967)"},{"key":"16_CR8","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-61667-9","volume-title":"Constructive Analysis","author":"E Bishop","year":"1985","unstructured":"Bishop, E., Bridges, D.: Constructive Analysis. Springer, Berlin (1985)"},{"issue":"7","key":"16_CR9","doi-asserted-by":"publisher","first-page":"1196","DOI":"10.1017\/S0960129514000437","volume":"26","author":"S Boldo","year":"2016","unstructured":"Boldo, S., Lelay, C., Melquiond, G.: Formalization of real analysis: a survey of proof assistants and libraries. Math. Struct. Comput. Sci. 26(7), 1196\u20131233 (2016). https:\/\/doi.org\/10.1017\/S0960129514000437","journal-title":"Math. Struct. Comput. Sci."},{"issue":"1","key":"16_CR10","doi-asserted-by":"publisher","first-page":"64","DOI":"10.1017\/S0960129520000171","volume":"31","author":"AB Booij","year":"2021","unstructured":"Booij, A.B.: Extensional constructive real analysis via locators. Math. Struct. Comput. Sci. 31(1), 64\u201388 (2021). https:\/\/doi.org\/10.1017\/S0960129520000171","journal-title":"Math. Struct. Comput. Sci."},{"key":"16_CR11","unstructured":"Booij, A.B.: The HoTT reals coincide with the Escard\u00f3-Simpson reals (2017). http:\/\/arxiv.org\/abs\/1706.05956"},{"key":"16_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"114","DOI":"10.1007\/3-540-44557-9_7","volume-title":"Types for Proofs and Programs","author":"A Ciaffaglione","year":"2000","unstructured":"Ciaffaglione, A., Di Gianantonio, P.: A co-inductive approach to real numbers. In: Coquand, T., Dybjer, P., Nordstr\u00f6m, B., Smith, J. (eds.) TYPES 1999. LNCS, vol. 1956, pp. 114\u2013130. Springer, Heidelberg (2000). https:\/\/doi.org\/10.1007\/3-540-44557-9_7"},{"key":"16_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"108","DOI":"10.1007\/3-540-39185-1_7","volume-title":"Types for Proofs and Programs","author":"L Cruz-Filipe","year":"2003","unstructured":"Cruz-Filipe, L.: A constructive formalization of the fundamental theorem of calculus. In: Geuvers, H., Wiedijk, F. (eds.) TYPES 2002. LNCS, vol. 2646, pp. 108\u2013126. Springer, Heidelberg (2003). https:\/\/doi.org\/10.1007\/3-540-39185-1_7"},{"key":"16_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"88","DOI":"10.1007\/978-3-540-27818-4_7","volume-title":"Mathematical Knowledge Management","author":"L Cruz-Filipe","year":"2004","unstructured":"Cruz-Filipe, L., Geuvers, H., Wiedijk, F.: C-CoRN, the constructive Coq repository at Nijmegen. In: Asperti, A., Bancerek, G., Trybulec, A. (eds.) MKM 2004. LNCS, vol. 3119, pp. 88\u2013103. Springer, Heidelberg (2004). https:\/\/doi.org\/10.1007\/978-3-540-27818-4_7"},{"issue":"10","key":"16_CR15","doi-asserted-by":"publisher","first-page":"1270","DOI":"10.1017\/S0960129521000153","volume":"31","author":"T de Jong","year":"2021","unstructured":"de Jong, T.: The Scott model of PCF in univalent type theory. Math. Struct. Comput. Sci. 31(10), 1270\u20131300 (2021). https:\/\/doi.org\/10.1017\/S0960129521000153","journal-title":"Math. Struct. Comput. Sci."},{"key":"16_CR16","doi-asserted-by":"publisher","first-page":"134","DOI":"10.4204\/EPTCS.351.9","volume":"351","author":"T de Jong","year":"2021","unstructured":"de Jong, T.: Sharp elements and apartness in domains. Electron. Proc. Theor. Comput. Sci. 351, 134\u2013151 (2021). https:\/\/doi.org\/10.4204\/EPTCS.351.9","journal-title":"Electron. Proc. Theor. Comput. Sci."},{"key":"16_CR17","doi-asserted-by":"publisher","unstructured":"de Jong, T.: Apartness, sharp elements, and the Scott topology of domains. Math. Struct. Comput. Sci. 1\u201332 (2023). https:\/\/doi.org\/10.1017\/S0960129523000282","DOI":"10.1017\/S0960129523000282"},{"key":"16_CR18","doi-asserted-by":"crossref","unstructured":"de Jong, T.: Domain theory in constructive and predicative univalent foundations. Ph.D. thesis, University of Birmingham (2023)","DOI":"10.46298\/lmcs-19(2:8)2023"},{"issue":"6","key":"16_CR19","doi-asserted-by":"publisher","first-page":"803","DOI":"10.1017\/S0960129504004360","volume":"14","author":"M Escard\u00f3","year":"2004","unstructured":"Escard\u00f3, M., Hofmann, M., Streicher, T.: On the non-sequential nature of the interval-domain model of real-number computation. Math. Struct. Comput. Sci. 14(6), 803\u2013814 (2004). https:\/\/doi.org\/10.1017\/S0960129504004360","journal-title":"Math. Struct. Comput. Sci."},{"issue":"1","key":"16_CR20","doi-asserted-by":"publisher","first-page":"79","DOI":"10.1016\/0304-3975(95)00250-2","volume":"162","author":"MH Escard\u00f3","year":"1996","unstructured":"Escard\u00f3, M.H.: PCF extended with real numbers. Theor. Comput. Sci. 162(1), 79\u2013115 (1996). https:\/\/doi.org\/10.1016\/0304-3975(95)00250-2","journal-title":"Theor. Comput. Sci."},{"issue":"1","key":"16_CR21","doi-asserted-by":"publisher","first-page":"121","DOI":"10.1016\/S0304-3975(98)00099-1","volume":"210","author":"MH Escard\u00f3","year":"1999","unstructured":"Escard\u00f3, M.H., Streicher, T.: Induction and recursion on the partial real line with applications to Real PCF. Theor. Comput. Sci. 210(1), 121\u2013157 (1999). https:\/\/doi.org\/10.1016\/S0304-3975(98)00099-1","journal-title":"Theor. Comput. Sci."},{"key":"16_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"79","DOI":"10.1007\/3-540-45842-5_6","volume-title":"Types for Proofs and Programs","author":"H Geuvers","year":"2002","unstructured":"Geuvers, H., Niqui, M.: Constructive reals in Coq: axioms and categoricity. In: Callaghan, P., Luo, Z., McKinna, J., Pollack, R., Pollack, R. (eds.) TYPES 2000. LNCS, vol. 2277, pp. 79\u201395. Springer, Heidelberg (2002). https:\/\/doi.org\/10.1007\/3-540-45842-5_6"},{"issue":"1","key":"16_CR23","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1017\/S0960129506005834","volume":"17","author":"H Geuvers","year":"2007","unstructured":"Geuvers, H., Niqui, M., Spitters, B., Wiedijk, F.: Constructive analysis, types and exact real numbers. Math. Struct. Comput. Sci. 17(1), 3\u201336 (2007). https:\/\/doi.org\/10.1017\/S0960129506005834","journal-title":"Math. Struct. Comput. Sci."},{"key":"16_CR24","doi-asserted-by":"publisher","unstructured":"Ghica, D.R., Ambridge, T.W.: Global optimisation with constructive reals. In: 36th Annual ACM\/IEEE Symposium on Logic in Computer Science, LICS 2021, Rome, Italy, 29 June\u20132 July 2021, pp. 1\u201313. IEEE (2021). https:\/\/doi.org\/10.1109\/LICS52264.2021.9470549","DOI":"10.1109\/LICS52264.2021.9470549"},{"key":"16_CR25","doi-asserted-by":"publisher","unstructured":"Gilbert, G.: Formalising real numbers in homotopy type theory. In: Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs, CPP 2017, pp. 112\u2013124. Association for Computing Machinery, New York (2017). https:\/\/doi.org\/10.1145\/3018610.3018614","DOI":"10.1145\/3018610.3018614"},{"key":"16_CR26","unstructured":"Jones, C.: Completing the rationals and metric spaces in LEGO. Logical Environ. 297\u2013316 (1993)"},{"key":"16_CR27","doi-asserted-by":"publisher","unstructured":"de\u00a0Jong, T., Escard\u00f3, M.H.: Domain theory in constructive and predicative univalent foundations. In: 29th EACSL Annual Conference on Computer Science Logic (CSL 2021). Leibniz International Proceedings in Informatics (LIPIcs), vol.\u00a0183, pp. 28:1\u201328:18. Schloss Dagstuhl\u2013Leibniz-Zentrum f\u00fcr Informatik, Dagstuhl, Germany (2021). https:\/\/doi.org\/10.4230\/LIPIcs.CSL.2021.28","DOI":"10.4230\/LIPIcs.CSL.2021.28"},{"key":"16_CR28","doi-asserted-by":"publisher","unstructured":"Krebbers, R., Spitters, B.: Type classes for efficient exact real arithmetic in Coq. Logical Methods Comput. Sci. 9(1) (2013). https:\/\/doi.org\/10.2168\/LMCS-9(1:1)2013","DOI":"10.2168\/LMCS-9(1:1)2013"},{"key":"16_CR29","doi-asserted-by":"publisher","unstructured":"Leinster, T.: Higher Operads, Higher Categories (2003). https:\/\/doi.org\/10.48550\/arXiv.math\/0305049","DOI":"10.48550\/arXiv.math\/0305049"},{"key":"16_CR30","unstructured":"Ljungstrom, A.: Symmetric Monoidal Smash Products in Homotopy Type Theory (2024). https:\/\/arxiv.org\/abs\/2402.03523"},{"key":"16_CR31","unstructured":"Moore, R.E.: Interval Analysis, vol.\u00a04. Prentice-Hall Englewood Cliffs (1966)"},{"issue":"1","key":"16_CR32","doi-asserted-by":"publisher","first-page":"129","DOI":"10.1017\/S0960129506005871","volume":"17","author":"R O\u2019Connor","year":"2007","unstructured":"O\u2019Connor, R.: A monadic, functional implementation of real numbers. Math. Struct. Comput. Sci. 17(1), 129\u2013159 (2007). https:\/\/doi.org\/10.1017\/S0960129506005871","journal-title":"Math. Struct. Comput. Sci."},{"key":"16_CR33","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"246","DOI":"10.1007\/978-3-540-71067-7_21","volume-title":"Theorem Proving in Higher Order Logics","author":"R O\u2019Connor","year":"2008","unstructured":"O\u2019Connor, R.: Certified exact transcendental real number computation in Coq. In: Mohamed, O.A., Mu\u00f1oz, C., Tahar, S. (eds.) TPHOLs 2008. LNCS, vol. 5170, pp. 246\u2013261. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-71067-7_21"},{"issue":"1","key":"16_CR34","doi-asserted-by":"publisher","first-page":"360","DOI":"10.1016\/j.apal.2005.05.032","volume":"137","author":"MB Smyth","year":"2006","unstructured":"Smyth, M.B.: The constructive maximal point space and partial metrizability. Ann. Pure Appl. Logic 137(1), 360\u2013379 (2006). https:\/\/doi.org\/10.1016\/j.apal.2005.05.032","journal-title":"Ann. Pure Appl. Logic"},{"key":"16_CR35","unstructured":"Univalent Foundations Program, T.: Homotopy Type Theory: Univalent Foundations of Mathematics (2013). https:\/\/homotopytypetheory.org\/book, Institute for Advanced Study"},{"key":"16_CR36","doi-asserted-by":"publisher","unstructured":"Voevodsky, V., Ahrens, B., Grayson, D., et\u00a0al.: UniMath\u2014a computer-checked library of univalent mathematics. http:\/\/unimath.org. https:\/\/doi.org\/10.5281\/zenodo.7848572. https:\/\/github.com\/UniMath\/UniMath","DOI":"10.5281\/zenodo.7848572"}],"container-title":["Lecture Notes in Computer Science","Logics and Type Systems in Theory and Practice"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-61716-4_16","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,5,29]],"date-time":"2024-05-29T03:49:29Z","timestamp":1716954569000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-61716-4_16"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024]]},"ISBN":["9783031617157","9783031617164"],"references-count":36,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-61716-4_16","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2024]]},"assertion":[{"value":"22 May 2024","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}