{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,7,20]],"date-time":"2025-07-20T04:24:36Z","timestamp":1752985476353,"version":"3.41.0"},"publisher-location":"New York, NY, USA","reference-count":29,"publisher":"ACM","license":[{"start":{"date-parts":[[2018,7,9]],"date-time":"2018-07-09T00:00:00Z","timestamp":1531094400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by-nd\/4.0\/"}],"funder":[{"DOI":"10.13039\/100011030","name":"U.S. Department of Energy","doi-asserted-by":"publisher","award":["DE-SC0014204, DE-SC0008923"],"award-info":[{"award-number":["DE-SC0014204, DE-SC0008923"]}],"id":[{"id":"10.13039\/100011030","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100007297","name":"Office of Naval Research","doi-asserted-by":"publisher","award":["N00014-17-1-2699"],"award-info":[{"award-number":["N00014-17-1-2699"]}],"id":[{"id":"10.13039\/100007297","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2018,7,9]]},"DOI":"10.1145\/3209108.3209193","type":"proceedings-article","created":{"date-parts":[[2018,6,27]],"date-time":"2018-06-27T12:14:43Z","timestamp":1530101683000},"page":"859-868","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":5,"title":["Computable decision making on the reals and other spaces"],"prefix":"10.1145","author":[{"given":"Benjamin","family":"Sherman","sequence":"first","affiliation":[{"name":"MIT CSAIL"}]},{"given":"Luke","family":"Sciarappa","sequence":"additional","affiliation":[{"name":"MIT CSAIL"}]},{"given":"Adam","family":"Chlipala","sequence":"additional","affiliation":[{"name":"MIT CSAIL"}]},{"given":"Michael","family":"Carbin","sequence":"additional","affiliation":[{"name":"MIT CSAIL"}]}],"member":"320","published-online":{"date-parts":[[2018,7,9]]},"reference":[{"key":"e_1_3_2_1_1_1","first-page":"2015","article-title":"ROSCoq: Robots Powered by Constructive Reals","volume":"15","author":"Anand Abhishek","year":"2015","unstructured":"Abhishek Anand and Ross A Knepper . 2015 . ROSCoq: Robots Powered by Constructive Reals . Interactive Theorem Proving 15 , 15 (2015), 2015 . Abhishek Anand and Ross A Knepper. 2015. ROSCoq: Robots Powered by Constructive Reals. Interactive Theorem Proving 15, 15 (2015), 2015.","journal-title":"Interactive Theorem Proving"},{"key":"e_1_3_2_1_2_1","volume-title":"Fifth International Conference on Computability and Complexity in Analysis","author":"Bauer Andrej","year":"2008","unstructured":"Andrej Bauer . 2008 . Efficient computation with Dedekind reals . In Fifth International Conference on Computability and Complexity in Analysis , Hagen, Germany. Andrej Bauer. 2008. Efficient computation with Dedekind reals. In Fifth International Conference on Computability and Complexity in Analysis, Hagen, Germany."},{"volume-title":"Foundations of Constructive Analysis","author":"Bishop Errett","key":"e_1_3_2_1_3_1","unstructured":"Errett Bishop . 1967. Foundations of Constructive Analysis . Academic Press . Errett Bishop. 1967. Foundations of Constructive Analysis. Academic Press."},{"key":"e_1_3_2_1_4_1","volume-title":"Maria Emilia Maietti, and Giovanni Sambin","author":"Ciraulo Francesco","year":"2013","unstructured":"Francesco Ciraulo , Maria Emilia Maietti, and Giovanni Sambin . 2013 . Convergence in formal topology: a unifying notion. Journal of Logic and Analysis 5 (2013). Francesco Ciraulo, Maria Emilia Maietti, and Giovanni Sambin. 2013. Convergence in formal topology: a unifying notion. Journal of Logic and Analysis 5 (2013)."},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0168-0072(03)00052-6"},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(95)00250-2"},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2004.09.017"},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2007.25"},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2012.41"},{"volume-title":"Topos theory","author":"Johnstone Peter T","key":"e_1_3_2_1_10_1","unstructured":"Peter T Johnstone . 1977. Topos theory . Academic Press . Peter T Johnstone. 1977. Topos theory. Academic Press."},{"volume-title":"Sketches of an elephant: A topos theory compendium","author":"Johnstone Peter T","key":"e_1_3_2_1_11_1","unstructured":"Peter T Johnstone . 2002. Sketches of an elephant: A topos theory compendium . Vol. 2 . Oxford University Press . Peter T Johnstone. 2002. Sketches of an elephant: A topos theory compendium. Vol. 2. Oxford University Press."},{"volume-title":"Sheaves in Geometry and Logic: A First Introduction to Topos Theory","author":"Lane Saunders Mac","key":"e_1_3_2_1_12_1","unstructured":"Saunders Mac Lane and Ieke Moerdijk . 1992. Sheaves in Geometry and Logic: A First Introduction to Topos Theory . Springer-Verlag . Saunders Mac Lane and Ieke Moerdijk. 1992. Sheaves in Geometry and Logic: A First Introduction to Topos Theory. Springer-Verlag."},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2007.01.021"},{"key":"e_1_3_2_1_14_1","unstructured":"Norbert Th M\u00fcller. 2009. Enhancing imperative exact real arithmetic with functions and logic. In Computability and Complexity in Analysis Ljubljana.  Norbert Th M\u00fcller. 2009. Enhancing imperative exact real arithmetic with functions and logic. In Computability and Complexity in Analysis Ljubljana."},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-71067-7_21"},{"key":"e_1_3_2_1_16_1","volume-title":"Proceedings of the Annual European Summer Meeting of the Association for Symbolic Logic, held in Helsinki, Finland. 221--231","author":"Palmgren Erik","year":"2003","unstructured":"Erik Palmgren . 2003 . Predicativity problems in point-free topology . In Proceedings of the Annual European Summer Meeting of the Association for Symbolic Logic, held in Helsinki, Finland. 221--231 . Erik Palmgren. 2003. Predicativity problems in point-free topology. In Proceedings of the Annual European Summer Meeting of the Association for Symbolic Logic, held in Helsinki, Finland. 221--231."},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/3209108.3209193"},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.5555\/645727.756598"},{"key":"e_1_3_2_1_19_1","first-page":"1","article-title":"A lambda calculus for real analysis","volume":"2","author":"Taylor Paul","year":"2010","unstructured":"Paul Taylor . 2010 . A lambda calculus for real analysis . Journal of Logic and Analysis 2 (2010), 1 -- 115 . Paul Taylor. 2010. A lambda calculus for real analysis. Journal of Logic and Analysis 2 (2010), 1--115.","journal-title":"Journal of Logic and Analysis"},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.apal.2005.05.027"},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(01)00104-9"},{"volume-title":"Topology via logic","author":"Vickers Steven","key":"e_1_3_2_1_22_1","unstructured":"Steven Vickers . 1989. Topology via logic . Cambridge University Press . Steven Vickers. 1989. Topology via logic. Cambridge University Press."},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0305004196001636"},{"key":"e_1_3_2_1_24_1","first-page":"372","article-title":"The double powerlocale and exponentiation: a case study in geometric logic","volume":"12","author":"Vickers Steven","year":"2004","unstructured":"Steven Vickers . 2004 . The double powerlocale and exponentiation: a case study in geometric logic . Theory and Applications of Categories 12 , 13 (2004), 372 -- 422 . Steven Vickers. 2004. The double powerlocale and exponentiation: a case study in geometric logic. Theory and Applications of Categories 12, 13 (2004), 372--422.","journal-title":"Theory and Applications of Categories"},{"key":"e_1_3_2_1_25_1","first-page":"328","article-title":"Localic completion of generalized metric spaces I","volume":"14","author":"Vickers Steven","year":"2005","unstructured":"Steven Vickers . 2005 . Localic completion of generalized metric spaces I . Theory and Applications of Categories 14 , 15 (2005), 328 -- 356 . Steven Vickers. 2005. Localic completion of generalized metric spaces I. Theory and Applications of Categories 14, 15 (2005), 328--356.","journal-title":"Theory and Applications of Categories"},{"volume-title":"Handbook of spatial logics","author":"Vickers Steven","key":"e_1_3_2_1_26_1","unstructured":"Steven Vickers . 2007a. Locales and toposes as spaces . In Handbook of spatial logics . Springer , 429--496. Steven Vickers. 2007a. Locales and toposes as spaces. In Handbook of spatial logics. Springer, 429--496."},{"key":"e_1_3_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.2178\/jsl\/1185803619"},{"key":"e_1_3_2_1_28_1","volume-title":"The connected Vietoris powerlocale. Topology and its Applications 156, 11","author":"Vickers Steven","year":"2009","unstructured":"Steven Vickers . 2009. The connected Vietoris powerlocale. Topology and its Applications 156, 11 ( 2009 ), 1886--1910. Steven Vickers. 2009. The connected Vietoris powerlocale. Topology and its Applications 156, 11 (2009), 1886--1910."},{"key":"e_1_3_2_1_29_1","unstructured":"K. Weihrauch. 1995. A simple introduction to computable analysis. Fernuniv. Fachbereich Informatik.  K. Weihrauch. 1995. A simple introduction to computable analysis. Fernuniv. Fachbereich Informatik."}],"event":{"name":"LICS '18: 33rd Annual ACM\/IEEE Symposium on Logic in Computer Science","sponsor":["SIGLOG ACM Special Interest Group on Logic and Computation","EACSL European Association for Computer Science Logic","IEEE-CS\\DATC IEEE Computer Society"],"location":"Oxford United Kingdom","acronym":"LICS '18"},"container-title":["Proceedings of the 33rd Annual ACM\/IEEE Symposium on Logic in Computer Science"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3209108.3209193","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3209108.3209193","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3209108.3209193","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T02:07:08Z","timestamp":1750212428000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3209108.3209193"}},"subtitle":["via partiality and nondeterminism"],"short-title":[],"issued":{"date-parts":[[2018,7,9]]},"references-count":29,"alternative-id":["10.1145\/3209108.3209193","10.1145\/3209108"],"URL":"https:\/\/doi.org\/10.1145\/3209108.3209193","relation":{},"subject":[],"published":{"date-parts":[[2018,7,9]]},"assertion":[{"value":"2018-07-09","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}