{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T22:12:41Z","timestamp":1725487961528},"publisher-location":"Berlin, Heidelberg","reference-count":35,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540730002"},{"type":"electronic","value":"9783540730019"}],"license":[{"start":{"date-parts":[[2007,1,1]],"date-time":"2007-01-01T00:00:00Z","timestamp":1167609600000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2007]]},"DOI":"10.1007\/978-3-540-73001-9_4","type":"book-chapter","created":{"date-parts":[[2007,7,24]],"date-time":"2007-07-24T11:16:31Z","timestamp":1185275791000},"page":"28-42","source":"Crossref","is-referenced-by-count":1,"title":["RZ: A Tool for Bringing Constructive and Computable Mathematics Closer to Programming Practice"],"prefix":"10.1007","author":[{"given":"Andrej","family":"Bauer","sequence":"first","affiliation":[]},{"given":"Christopher A.","family":"Stone","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"4_CR1","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)"},{"key":"4_CR2","volume-title":"Handbook of Logic in Computer Science","author":"J. Tucker","year":"1998","unstructured":"Tucker, J., Zucker, J.I.: Computable functions and semicomputable sets on many-sorted algebras. In: Abramsky, S., Gabbay, D., Maibaum, T. (eds.) Handbook of Logic in Computer Science, vol.\u00a05, Clarendon Press, Oxford (1998)"},{"key":"4_CR3","doi-asserted-by":"publisher","first-page":"225","DOI":"10.1016\/S0168-0072(96)00017-6","volume":"83","author":"J. Blanck","year":"1997","unstructured":"Blanck, J.: Domain representability of metric spaces. Annals of Pure. and Applied Logic\u00a083, 225\u2013247 (1997)","journal-title":"Annals of Pure and Applied Logic"},{"key":"4_CR4","series-title":"Lecture Notes in Computer Science","first-page":"17","volume-title":"Computability and Complexity in Analysis","author":"A. Edalat","year":"2000","unstructured":"Edalat, A., Lieutier, A.: Domain of differentiable functions. In: Blank, J., Brattka, V., Hertling, P. (eds.) CCA 2000. LNCS, vol.\u00a02064, pp. 17\u201319. Springer, Heidelberg (2000)"},{"key":"4_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"17","DOI":"10.1007\/3-540-46406-9","volume-title":"Computability and Complexity in Analysis","author":"N. M\u00fcller","year":"2000","unstructured":"M\u00fcller, N.: The iRRAM: Exact arithmetic in C++. In: Blank, J., Brattka, V., Hertling, P. (eds.) CCA 2000. LNCS, vol.\u00a02064, pp. 17\u201319. Springer, Heidelberg (2000)"},{"key":"4_CR6","unstructured":"Lambov, B.: RealLib: an efficient implementation of exact real arithmetic. In: Grubba, T., Hertling, P., Tsuiki, H., Weihrauch, K. (eds.) Computability and Complexity in Analysis Proccedings, Second International Conference, CCA 2005, Kyoto, Japan, August 25\u201329, 2005 pp. 169\u2013175 (2005)"},{"key":"4_CR7","unstructured":"Leroy, X., Doligez, D., Garrigue, J., R\u00e9my, D., Vouillon, J.: The Objective Caml system, documentation and user\u2019s manual - release 3.08. Technical report, INRIA (July 2004)"},{"key":"4_CR8","unstructured":"Komagata, Y., Schmidt, D.A.: Implementation of intuitionistic type theory and realizability theory. Technical Report TR-CS-95-4, Kansas State University (1995)"},{"key":"4_CR9","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-07964-5","volume-title":"Interactive Theorem Proving and Program Development","author":"Y. Bertot","year":"2004","unstructured":"Bertot, Y., Cast\u00e9ran, P.: Interactive Theorem Proving and Program Development. Springer, Heidelberg (2004)"},{"key":"4_CR10","volume-title":"Automated Deduction: A Basis for Applications, Systems and Implementation Techniques","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., Schmidt, P.H. (eds.) Automated Deduction: A Basis for Applications, Systems and Implementation Techniques, vol.\u00a0II, Kluwer Academic Publishers, Dordrecht (1998)"},{"key":"4_CR11","doi-asserted-by":"crossref","unstructured":"Bauer, A., Stone, C.A.: Specifications via realizability. In: Proceedings of the Workshop on the Constructive Logic for Automated Software Engineering (CLASE 2005) volume 153 of Electronic Notes in Theoretical Computer Science, pp. 77\u201392 (2006)","DOI":"10.1016\/j.entcs.2005.08.007"},{"key":"4_CR12","doi-asserted-by":"crossref","unstructured":"Longley, J.: Matching typed and untyped realizability. Electr. Notes Theor. Comput. Sci. 23(1) (1999)","DOI":"10.1016\/S1571-0661(04)00105-7"},{"key":"4_CR13","doi-asserted-by":"crossref","unstructured":"Longley, J.: When is a functional program not a functional program? In: International Conference on Functional Programming, pp. 1\u20137 (1999)","DOI":"10.1145\/317636.317775"},{"key":"4_CR14","unstructured":"Bauer, A.: The Realizability Approach to Computable Analysis and Topology. PhD thesis, Carnegie Mellon University (2000)"},{"key":"4_CR15","volume-title":"Categorical Logic and Type Theory","author":"B. Jacobs","year":"1999","unstructured":"Jacobs, B.: Categorical Logic and Type Theory. Elsevier, Amsterdam (1999)"},{"key":"4_CR16","doi-asserted-by":"publisher","first-page":"1","DOI":"10.2307\/2267170","volume":"12","author":"E. Post","year":"1947","unstructured":"Post, E.: Recursive unsolvability of a problem of Thue. The Journal of Symbolic Logic\u00a012, 1\u201311 (1947)","journal-title":"The Journal of Symbolic Logic"},{"key":"4_CR17","series-title":"Studies in Logic and the Foundations of Mathematics","volume-title":"Constructivism in Mathematics, An Introduction","author":"A.S. Troelstra","year":"1988","unstructured":"Troelstra, A.S., van Dalen, D.: Constructivism in Mathematics, An Introduction. Studies in Logic and the Foundations of Mathematics, vol.\u00a01(121). North-Holland, Amsterdam (1988)"},{"key":"4_CR18","first-page":"341","volume-title":"Proceedings of the 17th ACM Symposium on Principles of Programming Languages (POPL \u201990)","author":"R. Harper","year":"1990","unstructured":"Harper, R., Mitchell, J.C., Moggi, E.: Higher-order Modules and the Phase Distinction. In: Proceedings of the 17th ACM Symposium on Principles of Programming Languages (POPL \u201990), pp. 341\u2013354. ACM Press, New York (1990)"},{"key":"4_CR19","volume-title":"Programming in Martin-L\u00f6f\u2019s Type Theory","author":"B. Nordstr\u00f6m","year":"1990","unstructured":"Nordstr\u00f6m, B., Petersson, K., Smith, J.M.: Programming in Martin-L\u00f6f\u2019s Type Theory. Oxford University Press, Oxford (1990)"},{"key":"4_CR20","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-11035-5","volume-title":"Admissible Sets and Structures","author":"J. Barwise","year":"1975","unstructured":"Barwise, J.: Admissible Sets and Structures. Springer, Heidelberg (1975)"},{"key":"4_CR21","volume-title":"Studies in Logic and the Foundations of Mathematics","author":"A.S. Troelstra","year":"1988","unstructured":"Troelstra, A.S., van Dalen, D.: Constructivism in Mathematics, An Introduction. In: Studies in Logic and the Foundations of Mathematics, vol.\u00a02(123), North-Holland, Amsterdam (1988)"},{"issue":"2","key":"4_CR22","doi-asserted-by":"publisher","first-page":"445","DOI":"10.1016\/S0304-3975(96)00163-6","volume":"173","author":"S. Kahrs","year":"1997","unstructured":"Kahrs, S., Sannella, D., Tarlecki, A.: The definition of Extended ML: A gentle introduction. Theoretical Computer Science\u00a0173(2), 445\u2013484 (1997)","journal-title":"Theoretical Computer Science"},{"volume-title":"Handbook of Recursive Mathematics","year":"1998","key":"4_CR23","unstructured":"Ershov, Y.L., Goncharov, S.S., Nerode, A., Remmel, J.B. (eds.): Handbook of Recursive Mathematics. Elsevier, Amsterdam (1998)"},{"key":"4_CR24","doi-asserted-by":"publisher","first-page":"109","DOI":"10.2307\/2269016","volume":"10","author":"S.C. Kleene","year":"1945","unstructured":"Kleene, S.C.: On the interpretation of intuitionistic number theory. Journal of Symbolic Logic\u00a010, 109\u2013124 (1945)","journal-title":"Journal of Symbolic Logic"},{"key":"4_CR25","volume-title":"The Foundations of Intuitionistic Mathematics, especially in relation to recursive functions","author":"S.C. Kleene","year":"1965","unstructured":"Kleene, S.C., Vesley, R.E.: The Foundations of Intuitionistic Mathematics, especially in relation to recursive functions. North-Holland Publishing Company, Amsterdam (1965)"},{"key":"4_CR26","doi-asserted-by":"crossref","unstructured":"Birkedal, L.: Developing Theories of Types and Computability. PhD thesis, School of Computer Science, Carnegie Mellon University (December 1999)","DOI":"10.1016\/S1571-0661(05)80642-5"},{"key":"4_CR27","unstructured":"Blanck, J.: Computability on topological spaces by effective domain representations. PhD thesis, Uppsala University, Department of Mathematics, Uppsala, Sweden (1997)"},{"issue":"315","key":"4_CR28","doi-asserted-by":"publisher","first-page":"35","DOI":"10.1016\/j.tcs.2003.11.012","volume":"1","author":"A. Bauer","year":"2004","unstructured":"Bauer, A., Birkedal, L., Scott, D.S.: Equilogical spaces. Theoretical Computer Science\u00a01(315), 35\u201359 (2004)","journal-title":"Theoretical Computer Science"},{"issue":"3","key":"4_CR29","doi-asserted-by":"publisher","first-page":"522","DOI":"10.1137\/0205037","volume":"5","author":"D.S. Scott","year":"1976","unstructured":"Scott, D.S.: Data types as lattices. SIAM Journal of Computing\u00a05(3), 522\u2013587 (1976)","journal-title":"SIAM Journal of Computing"},{"key":"4_CR30","unstructured":"Escard\u00f3, M.H.: PCF extended with real numbers. PhD thesis, Department of Computer Science, University of Edinburgh (December 1997)"},{"key":"4_CR31","first-page":"426","volume-title":"Proceedings of the 19th Annual IEEE Symposium on Logic in Computer Science","author":"J.R. Marcial-Romero","year":"2004","unstructured":"Marcial-Romero, J.R., Escard\u00f3, M.H.: Semantics of a sequential language for exact real-number computation. In: Proceedings of the 19th Annual IEEE Symposium on Logic in Computer Science, pp. 426\u2013435. IEEE Computer Society Press, Los Alamitos (2004)"},{"key":"4_CR32","series-title":"Elsevier computer science library : Theory of computation series","volume-title":"The computational complexity of algebraic and numeric problems","author":"A. Borodin","year":"1975","unstructured":"Borodin, A., Monro, J.I.: The computational complexity of algebraic and numeric problems. Elsevier computer science library: Theory of computation series, vol.\u00a01. American Elsevier, New York, London, Amsterdam (1975)"},{"key":"4_CR33","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4612-0701-6","volume-title":"Complexity and Real Computation","author":"L. Blum","year":"1998","unstructured":"Blum, L., Cucker, F., Shub, M., Smale, S.: Complexity and Real Computation. Springer, New York (1998)"},{"key":"4_CR34","unstructured":"Yap, C.K.: Theory of real computation according to EGC (2006) To appear in LNCS Volume based on the Dagstuhl Seminar Reliable Implementation of Real Number Algorithms: Theory and Practice, (Jan 8-13, 2006)"},{"key":"4_CR35","series-title":"Grundlehren der math. Wissenschaften","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-642-61667-9","volume-title":"Constructive Analysis","author":"E. Bishop","year":"1985","unstructured":"Bishop, E., Bridges, D.: Constructive Analysis. Grundlehren der math. Wissenschaften, vol.\u00a0279. Springer, Heidelberg (1985)"}],"container-title":["Lecture Notes in Computer Science","Computation and Logic in the Real World"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-73001-9_4","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,1]],"date-time":"2019-05-01T08:18:00Z","timestamp":1556698680000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-73001-9_4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2007]]},"ISBN":["9783540730002","9783540730019"],"references-count":35,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-73001-9_4","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2007]]}}}