{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,24]],"date-time":"2025-03-24T07:25:45Z","timestamp":1742801145567},"publisher-location":"Berlin, Heidelberg","reference-count":28,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642396335"},{"type":"electronic","value":"9783642396342"}],"license":[{"start":{"date-parts":[[2013,1,1]],"date-time":"2013-01-01T00:00:00Z","timestamp":1356998400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2013]]},"DOI":"10.1007\/978-3-642-39634-2_27","type":"book-chapter","created":{"date-parts":[[2013,7,22]],"date-time":"2013-07-22T09:52:36Z","timestamp":1374486756000},"page":"370-385","source":"Crossref","is-referenced-by-count":5,"title":["Program Extraction from Nested Definitions"],"prefix":"10.1007","author":[{"given":"Kenji","family":"Miyamoto","sequence":"first","affiliation":[]},{"given":"Fredrik","family":"Nordvall Forsberg","sequence":"additional","affiliation":[]},{"given":"Helmut","family":"Schwichtenberg","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"27_CR1","unstructured":"Agda, http:\/\/wiki.portal.chalmers.se\/agda\/"},{"key":"27_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"91","DOI":"10.1007\/BFb0037100","volume-title":"Typed Lambda Calculi and Applications","author":"U. Berger","year":"1993","unstructured":"Berger, U.: Program extraction from normalization proofs. In: Bezem, M., Groote, J.F. (eds.) TLCA 1993. LNCS, vol.\u00a0664, pp. 91\u2013106. Springer, Heidelberg (1993)"},{"issue":"1","key":"27_CR3","doi-asserted-by":"publisher","first-page":"1","DOI":"10.2168\/LMCS-7(1:8)2011","volume":"7","author":"U. Berger","year":"2011","unstructured":"Berger, U.: From coinductive proofs to exact real arithmetic: theory and applications. Logical Methods in Computer Science\u00a07(1), 1\u201324 (2011)","journal-title":"Logical Methods in Computer Science"},{"key":"27_CR4","doi-asserted-by":"publisher","first-page":"313","DOI":"10.1007\/s00224-011-9325-8","volume":"51","author":"U. Berger","year":"2012","unstructured":"Berger, U., Seisenberger, M.: Proofs, programs, processes. Theory of Computing Systems\u00a051, 313\u2013329 (2012)","journal-title":"Theory of Computing Systems"},{"key":"27_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"24","DOI":"10.1007\/3-540-45842-5_2","volume-title":"Types for Proofs and Programs","author":"S. Berghofer","year":"2002","unstructured":"Berghofer, S., Nipkow, T.: Executing higher order logic. In: Callaghan, P., Luo, Z., McKinna, J., Pollack, R. (eds.) TYPES 2000. LNCS, vol.\u00a02277, pp. 24\u201340. Springer, Heidelberg (2002)"},{"key":"27_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"52","DOI":"10.1007\/BFb0054285","volume-title":"Mathematics of Program Construction","author":"R. Bird","year":"1998","unstructured":"Bird, R., Meertens, L.: Nested datatypes. In: Jeuring, J. (ed.) MPC 1998. LNCS, vol.\u00a01422, pp. 52\u201367. Springer, Heidelberg (1998)"},{"key":"27_CR7","volume-title":"Foundations of Constructive Analysis","author":"E. Bishop","year":"1967","unstructured":"Bishop, E.: Foundations of Constructive Analysis. McGraw-Hill, New York (1967)"},{"key":"27_CR8","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., Nordstr\u00f6m, B., Dybjer, P., Smith, J. (eds.) TYPES 1999. LNCS, vol.\u00a01956, pp. 114\u2013130. Springer, Heidelberg (2000)"},{"key":"27_CR9","unstructured":"Coq, http:\/\/coq.inria.fr\/"},{"key":"27_CR10","unstructured":"Danielsson, N.A., Altenkirch, T.: Mixing Induction and Coinduction. Draft (2009)"},{"key":"27_CR11","doi-asserted-by":"crossref","unstructured":"Ghani, N., Hancock, P., Pattinson, D.: Continuous functions on final coalgebras. In: Power, J. (ed.) CMCS 2006. Electr. Notes in Theoret. Computer Science (2006)","DOI":"10.1016\/j.entcs.2006.06.009"},{"key":"27_CR12","doi-asserted-by":"crossref","unstructured":"Hancock, P., Pattinson, D., Ghani, N.: Representations of stream processors using nested fixed points. Logical Methods in Computer Science\u00a05(3) (2009)","DOI":"10.2168\/LMCS-5(3:9)2009"},{"key":"27_CR13","unstructured":"Isabelle, http:\/\/isabelle.in.tum.de\/"},{"key":"27_CR14","doi-asserted-by":"crossref","unstructured":"Jacobs, B., Rutten, J.: An introduction to (co)algebras and (co)induction. In: Sangiorgi, D., Rutten, J. (eds.) Advanced Topics in Bisimulation and Coinduction, vol.\u00a052, pp. 38\u201399. Cambridge University Press (2011)","DOI":"10.1017\/CBO9780511792588.003"},{"key":"27_CR15","doi-asserted-by":"crossref","unstructured":"Krebbers, R., Spitters, B.: Type classes for efficient exact real arithmetic in Coq. Logical Methods in Computer Science\u00a09(1) (2013)","DOI":"10.2168\/LMCS-9(1:1)2013"},{"key":"27_CR16","unstructured":"Kreisel, G.: Interpretation of analysis by means of constructive functionals of finite types. In: Heyting, A. (ed.) Constructivity in Mathematics, pp. 101\u2013128. North-Holland, Amsterdam (1959)"},{"key":"27_CR17","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.\u00a05028, pp. 359\u2013369. Springer, Heidelberg (2008)"},{"key":"27_CR18","unstructured":"The Minlog System, http:\/\/www.minlog-system.de"},{"key":"27_CR19","unstructured":"Mitchell, N.: HLint, http:\/\/community.haskell.org\/~ndm\/hlint\/"},{"key":"27_CR20","doi-asserted-by":"crossref","unstructured":"Nakata, K., Uustalu, T.: Resumptions, weak bisimilarity and big-step semantics for while with interactive I\/O: An exercise in mixed induction-coinduction. In: Aceto, L., Sobocinski, P. (eds.) SOS. EPTCS, vol.\u00a032, pp. 57\u201375 (2010)","DOI":"10.4204\/EPTCS.32.5"},{"key":"27_CR21","unstructured":"Nuprl, http:\/\/www.nuprl.org\/"},{"key":"27_CR22","series-title":"LNAI","doi-asserted-by":"publisher","first-page":"151","DOI":"10.1007\/11542384_19","volume-title":"The Seventeen Provers of the World","author":"H. Schwichtenberg","year":"2006","unstructured":"Schwichtenberg, H.: Minlog. In: Wiedijk, F. (ed.) The Seventeen Provers of the World. LNCS (LNAI), vol.\u00a03600, pp. 151\u2013157. Springer, Heidelberg (2006)"},{"key":"27_CR23","unstructured":"Schwichtenberg, H.: Constructive analysis with witnesses. Manuscript (April 2012), http:\/\/www.math.lmu.de\/~schwicht\/seminars\/semws11\/constr11.pdf"},{"key":"27_CR24","doi-asserted-by":"crossref","unstructured":"Schwichtenberg, H., Wainer, S.S.: Proofs and Computations. In: Perspectives in Logic. Association for Symbolic Logic and Cambridge University Press (2012)","DOI":"10.1017\/CBO9781139031905"},{"key":"27_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"577","DOI":"10.1007\/BFb0012801","volume-title":"Automata, Languages, and Programming","author":"D. Scott","year":"1982","unstructured":"Scott, D.: Domains for denotational semantics. In: Nielsen, M., Schmidt, E.M. (eds.) ICALP 1982. LNCS, vol.\u00a0140, pp. 577\u2013610. Springer, Heidelberg (1982)"},{"key":"27_CR26","unstructured":"Takeyama, M.: A new compiler MAlonzo, https:\/\/lists.chalmers.se\/pipermail\/agda\/2008\/000219.html"},{"key":"27_CR27","unstructured":"Wiedmer, E.: Exaktes Rechnen mit reellen Zahlen und anderen unendlichen Objekten. PhD thesis, ETH Z\u00fcrich (1977)"},{"key":"27_CR28","doi-asserted-by":"publisher","first-page":"133","DOI":"10.1016\/0304-3975(80)90011-0","volume":"10","author":"E. Wiedmer","year":"1980","unstructured":"Wiedmer, E.: Computing with infinite objects. Theoretical Comput. Sci.\u00a010, 133\u2013155 (1980)","journal-title":"Theoretical Comput. Sci."}],"container-title":["Lecture Notes in Computer Science","Interactive Theorem Proving"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-39634-2_27","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,7,3]],"date-time":"2023-07-03T06:52:25Z","timestamp":1688367145000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-39634-2_27"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013]]},"ISBN":["9783642396335","9783642396342"],"references-count":28,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-39634-2_27","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2013]]}}}