{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,8,31]],"date-time":"2025-08-31T10:33:53Z","timestamp":1756636433944,"version":"3.40.3"},"publisher-location":"Cham","reference-count":30,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783031067723"},{"type":"electronic","value":"9783031067730"}],"license":[{"start":{"date-parts":[[2022,1,1]],"date-time":"2022-01-01T00:00:00Z","timestamp":1640995200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2022,1,1]],"date-time":"2022-01-01T00:00:00Z","timestamp":1640995200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2022]]},"DOI":"10.1007\/978-3-031-06773-0_41","type":"book-chapter","created":{"date-parts":[[2022,5,19]],"date-time":"2022-05-19T11:24:44Z","timestamp":1652959484000},"page":"771-789","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":4,"title":["Certified Computation of\u00a0Nondeterministic Limits"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-2374-9017","authenticated-orcid":false,"given":"Michal","family":"Kone\u010dn\u00fd","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-6443-2617","authenticated-orcid":false,"given":"Sewon","family":"Park","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0003-3959-0741","authenticated-orcid":false,"given":"Holger","family":"Thies","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2022,5,20]]},"reference":[{"key":"41_CR1","unstructured":"Balluchi, A., Casagrande, A., Collins, P., Ferrari, A., Villa, T., Sangiovanni-Vincentelli, A.: Ariadne: a framework for reachability analysis of hybrid automata. In: Proceedings 17th International Symposium on Mathematical Theory of Networks and Systems. Kyoto (2006)"},{"key":"41_CR2","doi-asserted-by":"publisher","unstructured":"Berger, U., Tsuiki, H.: Intuitionistic fixed point logic. Ann. Pure Appl. Log. 172(3), 102903 (2021). https:\/\/doi.org\/10.1016\/j.apal.2020.102903","DOI":"10.1016\/j.apal.2020.102903"},{"key":"41_CR3","unstructured":"Bishop, E.A.: Foundations of Constructive Analysis (1967)"},{"key":"41_CR4","doi-asserted-by":"crossref","unstructured":"Boldo, S., Melquiond, G.: Computer Arithmetic and Formal Proofs - Verifying Floating-point Algorithms with the Coq System. ISTE Press (2017). https:\/\/www.elsevier.com\/books\/computer-arithmetic-and-formal-proofs\/boldo\/978-1-78548-112-3","DOI":"10.1016\/B978-1-78548-112-3.50001-1"},{"key":"41_CR5","doi-asserted-by":"crossref","unstructured":"Brattka, V.: The emperor\u2019s new recursiveness: the epigraph of the exponential function in two models of computability. In: Ito, M., Imaoka, T. (eds.) Words, Languages & Combinatorics III, pp. 63\u201372. World Scientific Publishing, Singapore (2003), iCWLC 2000, Kyoto, Japan, 14\u201318 March 2000","DOI":"10.1142\/9789812704979_0005"},{"key":"41_CR6","doi-asserted-by":"publisher","unstructured":"Brattka, V., Hertling, P.: Feasible real random access machines. J. Complex. 14(4), 490\u2013526 (1998). https:\/\/doi.org\/10.1006\/jcom.1998.0488, https:\/\/www.sciencedirect.com\/science\/article\/pii\/S0885064X98904885","DOI":"10.1006\/jcom.1998.0488"},{"key":"41_CR7","doi-asserted-by":"publisher","unstructured":"Bridges, D.S.: Constructive mathematics: a foundation for computable analysis. Theor. Comput. Sci. 219(1), 95\u2013109 (1999). https:\/\/doi.org\/10.1016\/S0304-3975(98)00285-0, https:\/\/www.sciencedirect.com\/science\/article\/pii\/S0304397598002850","DOI":"10.1016\/S0304-3975(98)00285-0"},{"key":"41_CR8","unstructured":"Collins, P., Geretti, L., Casagrande, A., Zapreev, I., Zivanovic, S.: Ariadne (2005\u201320). http:\/\/www.ariadne-cps.org\/"},{"key":"41_CR9","doi-asserted-by":"crossref","unstructured":"Cooke, R.L.: Classical Algebra: its Nature, Origins, and Uses. John Wiley & Sons (2008)","DOI":"10.1002\/9780470277980"},{"key":"41_CR10","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"},{"key":"41_CR11","unstructured":"Brausse, F., Norbert M\u00fcller, R.R.: Intensionality and multi-valued limits. In: Proceedings 15th International Conference on Computability and Complexity in Analysis (CCA), p. 11 (2018)"},{"key":"41_CR12","doi-asserted-by":"publisher","unstructured":"Hertling, P.: A real number structure that is effectively categorical. Math. Log. Q. 45, 147\u2013182 (1999). https:\/\/doi.org\/10.1002\/malq.19990450202","DOI":"10.1002\/malq.19990450202"},{"key":"41_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"427","DOI":"10.1007\/BFb0022273","volume-title":"Computer Science Logic","author":"M Hofmann","year":"1995","unstructured":"Hofmann, M.: On the interpretation of type theory in locally cartesian closed categories. In: Pacholski, L., Tiuryn, J. (eds.) CSL 1994. LNCS, vol. 933, pp. 427\u2013441. Springer, Heidelberg (1995). https:\/\/doi.org\/10.1007\/BFb0022273"},{"key":"41_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"252","DOI":"10.1007\/978-3-030-88853-4_16","volume-title":"Logic, Language, Information, and Computation","author":"M Kone\u010dn\u00fd","year":"2021","unstructured":"Kone\u010dn\u00fd, M., Park, S., Thies, H.: Axiomatic reals and certified efficient exact real computation. In: Silva, A., Wassermann, R., de Queiroz, R. (eds.) WoLLIC 2021. LNCS, vol. 13038, pp. 252\u2013268. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-88853-4_16"},{"key":"41_CR15","unstructured":"Kone\u010dn\u00fd, M.: Verified exact real limit computation. In: Proceedings 15th International Conference on Computability and Complexity in Analysis (CCA), pp. 9\u201310 (2018)"},{"key":"41_CR16","unstructured":"Kone\u010dn\u00fd, M.: aern2-real: A Haskell library for exact real number computation. https:\/\/hackage.haskell.org\/package\/aern2-real (2021)"},{"key":"41_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"200","DOI":"10.1007\/3-540-39185-1_12","volume-title":"Types for Proofs and Programs","author":"P Letouzey","year":"2003","unstructured":"Letouzey, P.: A new extraction for Coq. In: Geuvers, H., Wiedijk, F. (eds.) TYPES 2002. LNCS, vol. 2646, pp. 200\u2013219. Springer, Heidelberg (2003). https:\/\/doi.org\/10.1007\/3-540-39185-1_12"},{"key":"41_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"359","DOI":"10.1007\/978-3-540-69407-6_39","volume-title":"Logic and Theory of Algorithms","author":"P Letouzey","year":"2008","unstructured":"Letouzey, P.: Extraction in Coq: an overview. In: Beckmann, A., Dimitracopoulos, C., L\u00f6we, B. (eds.) CiE 2008. LNCS, vol. 5028, pp. 359\u2013369. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-69407-6_39"},{"key":"41_CR19","doi-asserted-by":"publisher","unstructured":"Luckhardt, H.: A fundamental effect in computations on real numbers. Theor. Comput. Sci. 5(3), 321 \u2013 324 (1977). https:\/\/doi.org\/10.1016\/0304-3975(77)90048-2, http:\/\/www.sciencedirect.com\/science\/article\/pii\/0304397577900482","DOI":"10.1016\/0304-3975(77)90048-2"},{"key":"41_CR20","unstructured":"M\u00fcller, N.T.: Implementing limits in an interactive realram. In: 3rd Conference on Real Numbers and Computers, 1998, Paris. vol. 13, p. 26 (1998)"},{"key":"41_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"222","DOI":"10.1007\/3-540-45335-0_14","volume-title":"Computability and Complexity in Analysis","author":"NT M\u00fcller","year":"2001","unstructured":"M\u00fcller, N.T.: The iRRAM: exact arithmetic in C++. In: Blanck, J., Brattka, V., Hertling, P. (eds.) CCA 2000. LNCS, vol. 2064, pp. 222\u2013252. Springer, Heidelberg (2001). https:\/\/doi.org\/10.1007\/3-540-45335-0_14"},{"key":"41_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"168","DOI":"10.1007\/978-3-642-28891-3_17","volume-title":"NASA Formal Methods","author":"NT M\u00fcller","year":"2012","unstructured":"M\u00fcller, N.T., Uhrhan, C.: Some steps into verification of exact real arithmetic. In: Goodloe, A.E., Person, S. (eds.) NFM 2012. LNCS, vol. 7226, pp. 168\u2013173. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-28891-3_17"},{"key":"41_CR23","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/j.jco.2017.08.003","volume":"44","author":"E Neumann","year":"2018","unstructured":"Neumann, E., Pauly, A.: A topological view on algebraic computation models. J. Complex. 44, 1\u201322 (2018)","journal-title":"J. Complex."},{"key":"41_CR24","unstructured":"Park, S., et al.: Foundation of computer (algebra) analysis systems: Semantics, logic, programming, verification. arXiv e-prints pp. arXiv-1608 (2016)"},{"issue":"1","key":"41_CR25","doi-asserted-by":"publisher","first-page":"128","DOI":"10.1016\/S1571-0661(04)00108-2","volume":"23","author":"B Reus","year":"1999","unstructured":"Reus, B.: Realizability models for type theories. Electron. Notes Theor. Comput. Sci. 23(1), 128\u2013158 (1999)","journal-title":"Electron. Notes Theor. Comput. Sci."},{"issue":"1","key":"41_CR26","doi-asserted-by":"publisher","first-page":"33","DOI":"10.1017\/S0305004100061284","volume":"95","author":"RAG Seely","year":"1984","unstructured":"Seely, R.A.G.: Locally cartesian closed categories and type theory. Math. Proc. Camb. Philoso. Soc. 95(1), 33\u201348 (1984). https:\/\/doi.org\/10.1017\/S0305004100061284","journal-title":"Math. Proc. Camb. Philoso. Soc."},{"issue":"3","key":"41_CR27","doi-asserted-by":"publisher","first-page":"145","DOI":"10.2307\/2267043","volume":"14","author":"E Specker","year":"1949","unstructured":"Specker, E.: Nicht konstruktiv beweisbare S\u00e4tze der analysis. J. Symb. Logic 14(3), 145\u2013158 (1949)","journal-title":"J. Symb. Logic"},{"key":"41_CR28","unstructured":"Steinberg, F., Thery, L., Thies, H.: Computable analysis and notions of continuity in Coq. Logical Meth. Comput. Sci. 17(2) (2021). https:\/\/lmcs.episciences.org\/7478"},{"key":"41_CR29","unstructured":"Univalent Foundations Program, T.: Homotopy Type Theory: Univalent Foundations of Mathematics. https:\/\/homotopytypetheory.org\/book, Institute for Advanced Study (2013)"},{"key":"41_CR30","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-56999-9","volume-title":"Computable Analysis","author":"K Weihrauch","year":"2000","unstructured":"Weihrauch, K.: Computable Analysis. Springer, Berlin (2000). https:\/\/doi.org\/10.1007\/978-3-642-56999-9"}],"container-title":["Lecture Notes in Computer Science","NASA Formal Methods"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-06773-0_41","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,8,1]],"date-time":"2022-08-01T11:14:45Z","timestamp":1659352485000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-06773-0_41"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022]]},"ISBN":["9783031067723","9783031067730"],"references-count":30,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-06773-0_41","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2022]]},"assertion":[{"value":"20 May 2022","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"NFM","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"NASA Formal Methods Symposium","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Pasadena, CA","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"USA","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2022","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"24 May 2022","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"27 May 2022","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"14","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"nfm2022","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/shemesh.larc.nasa.gov\/nfm2022\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Single-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"118","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"33","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"6","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"28% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"6.3","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"No","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}