{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,8]],"date-time":"2026-06-08T21:41:34Z","timestamp":1780954894990,"version":"3.54.1"},"publisher-location":"Berlin, Heidelberg","reference-count":23,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642229435","type":"print"},{"value":"9783642229442","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2011]]},"DOI":"10.1007\/978-3-642-22944-2_29","type":"book-chapter","created":{"date-parts":[[2011,8,25]],"date-time":"2011-08-25T05:45:59Z","timestamp":1314251159000},"page":"393-399","source":"Crossref","is-referenced-by-count":14,"title":["Minlog - A Tool for Program Extraction Supporting Algebras and Coalgebras"],"prefix":"10.1007","author":[{"given":"Ulrich","family":"Berger","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Kenji","family":"Miyamoto","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Helmut","family":"Schwichtenberg","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Monika","family":"Seisenberger","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","reference":[{"key":"29_CR1","unstructured":"Agda: http:\/\/wiki.portal.chalmers.se\/agda\/"},{"key":"29_CR2","doi-asserted-by":"publisher","first-page":"27","DOI":"10.1007\/s11225-006-6604-5","volume":"82","author":"U. Berger","year":"2006","unstructured":"Berger, U., Berghofer, S., Letouzey, P., Schwichtenberg, H.: Program extraction from normalization proofs. Studia Logica\u00a082, 27\u201351 (2006)","journal-title":"Studia Logica"},{"key":"29_CR3","series-title":"Applied Logic Series","doi-asserted-by":"crossref","first-page":"41","DOI":"10.1007\/978-94-017-0435-9_2","volume-title":"Automated Deduction","author":"H. Benl","year":"1998","unstructured":"Benl, H., Berger, U., Schwichtenberg, H., Seisenberger, M., Zuber, W.: Proof theory at work: Program development in the Minlog system. In: Bibel, W., Schmitt, P.H. (eds.) Automated Deduction. Applied Logic Series, vol.\u00a0II, pp. 41\u201371. Kluwer, Dordrecht (1998)"},{"key":"29_CR4","first-page":"3","volume":"114","author":"U. Berger","year":"2002","unstructured":"Berger, U., Buchholz, W., Schwichtenberg, H.: Refined program extraction from classical proofs. APAL\u00a0114, 3\u201325 (2002)","journal-title":"APAL"},{"key":"29_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"132","DOI":"10.1007\/978-3-642-04027-6_12","volume-title":"Computer Science Logic","author":"U. Berger","year":"2009","unstructured":"Berger, U.: From coinductive proofs to exact real arithmetic. In: Gr\u00e4del, E., Kahle, R. (eds.) CSL 2009. LNCS, vol.\u00a05771, pp. 132\u2013146. Springer, Heidelberg (2009)"},{"key":"29_CR6","doi-asserted-by":"publisher","first-page":"19","DOI":"10.1016\/S0890-5401(03)00014-2","volume":"183","author":"U. Berger","year":"2003","unstructured":"Berger, U., Eberl, M., Schwichtenberg, H.: Term rewriting for normalization by evaluation. Information and Computation\u00a0183, 19\u201342 (2003)","journal-title":"Information and Computation"},{"key":"29_CR7","doi-asserted-by":"publisher","first-page":"394","DOI":"10.1007\/s00224-007-9017-6","volume":"43","author":"U. Berger","year":"2008","unstructured":"Berger, U., Hou, T.: Coinduction for exact real number computation. Theory of Computing Systems\u00a043, 394\u2013409 (2008)","journal-title":"Theory of Computing Systems"},{"key":"29_CR8","first-page":"203","volume-title":"Proceedings 6\u2019th Symposium on Logic in Computer Science, LICS 1991","author":"U. Berger","year":"1991","unstructured":"Berger, U., Schwichtenberg, H.: An inverse of the evaluation functional for typed \u03bb-calculus. In: Vemuri, R. (ed.) Proceedings 6\u2019th Symposium on Logic in Computer Science, LICS 1991, pp. 203\u2013211. IEEE Computer Society Press, Los Alamitos (1991)"},{"key":"29_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"28","DOI":"10.1007\/978-3-540-73001-9_4","volume-title":"Computation and Logic in the Real World","author":"A. Bauer","year":"2007","unstructured":"Bauer, A., Stone, C.A.: RZ: A tool for bringing constructive and computable mathematics closer to programming practice. In: Cooper, S.B., L\u00f6we, B., Sorbi, A. (eds.) CiE 2007. LNCS, vol.\u00a04497, pp. 28\u201342. Springer, Heidelberg (2007)"},{"key":"29_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"39","DOI":"10.1007\/978-3-642-13962-8_5","volume-title":"Programs, Proofs, Processes","author":"U. Berger","year":"2010","unstructured":"Berger, U., Seisenberger, M.: Proofs, programs, processes. In: Ferreira, F., L\u00f6we, B., Mayordomo, E., Mendes Gomes, L. (eds.) CiE 2010. LNCS, vol.\u00a06158, pp. 39\u201348. Springer, Heidelberg (2010)"},{"key":"29_CR11","doi-asserted-by":"publisher","first-page":"39","DOI":"10.1016\/j.tcs.2005.09.061","volume":"351","author":"A. Ciaffaglione","year":"2006","unstructured":"Ciaffaglione, A., Di Gianantonio, P.: A certified, corecursive implementation of exact real numbers. Theor. Comp. Sci.\u00a0351, 39\u201351 (2006)","journal-title":"Theor. Comp. Sci."},{"key":"29_CR12","unstructured":"Chuang, C.M.: Extraction of Programs for Exact Real Number Computation Using Agda. PhD thesis. Swansea University, Wales (2011)"},{"key":"29_CR13","unstructured":"The Coq Proof Assistant, http:\/\/coq.inria.fr\/"},{"key":"29_CR14","unstructured":"Crosilla, L., Seisenberger, M., Schwichtenberg, H.: A Tutorial for Minlog, Version 5.0 (2011)"},{"issue":"1","key":"29_CR15","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. Comp. Sci.\u00a017(1), 3\u201336 (2007)","journal-title":"Math. Struct. Comp. Sci."},{"key":"29_CR16","unstructured":"Isabelle, http:\/\/isabelle.in.tum.de\/"},{"key":"29_CR17","unstructured":"Kreisel, G.: Interpretation of analysis by means of constructive functionals of finite types. Constructivity in Mathematics, 101\u2013128 (1959)"},{"key":"29_CR18","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.\u00a02646, pp. 200\u2013219. Springer, Heidelberg (2003)"},{"issue":"4","key":"29_CR19","doi-asserted-by":"publisher","first-page":"497","DOI":"10.1093\/logcom\/1.4.497","volume":"2","author":"D. Miller","year":"1991","unstructured":"Miller, D.: A logic programming language with lambda\u2013abstraction, function variables and simple unification. Jour. Logic Comput.\u00a02(4), 497\u2013536 (1991)","journal-title":"Jour. Logic Comput."},{"key":"29_CR20","unstructured":"The Minlog System, http:\/\/www.minlog-system.de"},{"issue":"1-2","key":"29_CR21","doi-asserted-by":"publisher","first-page":"120","DOI":"10.1016\/j.tcs.2007.01.021","volume":"379","author":"J.R. Marcial-Romero","year":"2007","unstructured":"Marcial-Romero, J.R., Escardo, M.H.: Semantics of a sequential language for exact real-number computation. Theor. Comp. Sci.\u00a0379(1-2), 120\u2013141 (2007)","journal-title":"Theor. Comp. Sci."},{"key":"29_CR22","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"15","DOI":"10.1007\/978-3-540-30210-0_3","volume-title":"Artificial Intelligence and Symbolic Computation","author":"H. Schwichtenberg","year":"2004","unstructured":"Schwichtenberg, H.: Proof search in minimal logic. In: Buchberger, B., Campbell, J.A. (eds.) AISC 2004. LNCS (LNAI), vol.\u00a03249, pp. 15\u201325. Springer, Heidelberg (2004)"},{"key":"29_CR23","doi-asserted-by":"crossref","unstructured":"Schwichtenberg, H., Wainer, S.S.: Proofs and Computations. Perspectives in Logic. Assoc. Symb. Logic, Cambridge Univ. Press (to appear, 2011)","DOI":"10.1017\/CBO9781139031905"}],"container-title":["Lecture Notes in Computer Science","Algebra and Coalgebra in Computer Science"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-22944-2_29.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,6,9]],"date-time":"2023-06-09T00:03:47Z","timestamp":1686269027000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-22944-2_29"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011]]},"ISBN":["9783642229435","9783642229442"],"references-count":23,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-22944-2_29","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2011]]}}}