{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,6]],"date-time":"2026-06-06T06:00:01Z","timestamp":1780725601270,"version":"3.54.1"},"reference-count":21,"publisher":"Cambridge University Press (CUP)","issue":"8","license":[{"start":{"date-parts":[[2014,11,10]],"date-time":"2014-11-10T00:00:00Z","timestamp":1415577600000},"content-version":"unspecified","delay-in-days":0,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Math. Struct. Comp. Sci."],"published-print":{"date-parts":[[2015,12]]},"abstract":"<jats:p>The importance of an abstract approach to a computation theory over general data types has been stressed by Tucker in many of his papers. Berger and Seisenberger recently elaborated the idea for extraction out of proofs involving (only) abstract reals. They considered a proof involving coinduction of the proposition that any two reals in [\u22121, 1] have their average in the same interval, and informally extract a Haskell program from this proof, which works with stream representations of reals. Here we formalize the proof, and machine extract its computational content using the Minlog proof assistant. This required an extension of this system to also take coinduction into account.<\/jats:p>","DOI":"10.1017\/s0960129513000327","type":"journal-article","created":{"date-parts":[[2014,11,10]],"date-time":"2014-11-10T17:39:00Z","timestamp":1415641140000},"page":"1692-1704","source":"Crossref","is-referenced-by-count":5,"title":["Program extraction in exact real arithmetic"],"prefix":"10.1017","volume":"25","author":[{"given":"KENJI","family":"MIYAMOTO","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"HELMUT","family":"SCHWICHTENBERG","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"56","published-online":{"date-parts":[[2014,11,10]]},"reference":[{"key":"S0960129513000327_ref7","unstructured":"Berghofer S. (2003) Proofs, Programs and Executable Specifications in Higher Order Logic, Ph.D. thesis, Institut f\u00fcr Informatik, TU M\u00fcnchen."},{"key":"S0960129513000327_ref8","unstructured":"Chuang C. M. (2011) Extraction of Programs for Exact Real Number Computation Using Agda, Ph.D. thesis, Swansea University, Wales, UK."},{"key":"S0960129513000327_ref2","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0037100"},{"key":"S0960129513000327_ref10","unstructured":"Coq Development Team (2009) The Coq Proof Assistant Reference Manual \u2013 Version 8.2. Inria."},{"key":"S0960129513000327_ref3","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-04027-6_12"},{"key":"S0960129513000327_ref4","doi-asserted-by":"publisher","DOI":"10.1016\/S0890-5401(03)00014-2"},{"key":"S0960129513000327_ref1","unstructured":"Agda. (2013) Available at http:\/\/wiki.portal.chalmers.se\/agda\/"},{"key":"S0960129513000327_ref20","unstructured":"Wiedmer E. (1977) Exaktes Rechnen mit reellen Zahlen und anderen unendlichen Objekten, Ph.D. thesis, ETH Z\u00fcrich."},{"key":"S0960129513000327_ref17","doi-asserted-by":"publisher","DOI":"10.1007\/s00224-007-9027-4"},{"key":"S0960129513000327_ref13","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-39185-1_12"},{"key":"S0960129513000327_ref5","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-13962-8_5"},{"key":"S0960129513000327_ref9","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2005.09.061"},{"key":"S0960129513000327_ref12","first-page":"101","volume-title":"Constructivity in Mathematics","author":"Kreisel","year":"1959"},{"key":"S0960129513000327_ref11","volume-title":"Applied Proof Theory: Proof Interpretations and Their Use in Mathematics","author":"Kohlenbach","year":"2008"},{"key":"S0960129513000327_ref15","unstructured":"Plume D. (1998) A Calculator for Exact Real Number Computation, Ph.D. thesis, University of Edinburgh."},{"key":"S0960129513000327_ref18","volume-title":"Proofs and Computations","author":"Schwichtenberg","year":"2012"},{"key":"S0960129513000327_ref19","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-55808-X_6"},{"key":"S0960129513000327_ref21","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(80)90011-0"},{"key":"S0960129513000327_ref16","first-page":"151","article-title":"Minlog","volume":"3600","author":"Schwichtenberg","year":"2006","journal-title":"Springer Verlag Lecture Notes in Artificial Intelligence"},{"key":"S0960129513000327_ref14","unstructured":"O'Connor R. (2009) Incompleteness & Completeness. Formalizing Logic and Analysis in Type Theory, Ph.D. thesis, Nijmegen University."},{"key":"S0960129513000327_ref6","first-page":"313","article-title":"Proofs, programs, processes.","volume":"51","author":"Berger","year":"2012","journal-title":"Theory of Computing"}],"container-title":["Mathematical Structures in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0960129513000327","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,4,20]],"date-time":"2019-04-20T01:07:40Z","timestamp":1555722460000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0960129513000327\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014,11,10]]},"references-count":21,"journal-issue":{"issue":"8","published-print":{"date-parts":[[2015,12]]}},"alternative-id":["S0960129513000327"],"URL":"https:\/\/doi.org\/10.1017\/s0960129513000327","relation":{},"ISSN":["0960-1295","1469-8072"],"issn-type":[{"value":"0960-1295","type":"print"},{"value":"1469-8072","type":"electronic"}],"subject":[],"published":{"date-parts":[[2014,11,10]]}}}