{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,7]],"date-time":"2024-09-07T04:56:07Z","timestamp":1725684967402},"publisher-location":"Berlin, Heidelberg","reference-count":21,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642298219"},{"type":"electronic","value":"9783642298226"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2012]]},"DOI":"10.1007\/978-3-642-29822-6_23","type":"book-chapter","created":{"date-parts":[[2012,5,20]],"date-time":"2012-05-20T13:21:09Z","timestamp":1337520069000},"page":"290-306","source":"Crossref","is-referenced-by-count":2,"title":["Computing in Cantor\u2019s Paradise with \u03bb ZFC"],"prefix":"10.1007","author":[{"given":"Neil","family":"Toronto","sequence":"first","affiliation":[]},{"given":"Jay","family":"McCarthy","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"23_CR1","doi-asserted-by":"crossref","unstructured":"Abbott, S.: Understanding Analysis. Springer (2001)","DOI":"10.1007\/978-0-387-21506-8"},{"key":"23_CR2","doi-asserted-by":"publisher","first-page":"739","DOI":"10.1016\/S0049-237X(08)71120-0","volume":"90","author":"P. Aczel","year":"1977","unstructured":"Aczel, P.: An introduction to inductive definitions. Studies in Logic and the Foundations of Mathematics\u00a090, 739\u2013782 (1977)","journal-title":"Studies in Logic and the Foundations of Mathematics"},{"key":"23_CR3","unstructured":"Barras, B.: Sets in Coq, Coq in sets. Journal of Formalized Reasoning\u00a03(1) (2010)"},{"issue":"1-2","key":"23_CR4","doi-asserted-by":"publisher","first-page":"137","DOI":"10.1016\/S0304-3975(96)00302-7","volume":"179","author":"C. Berline","year":"1997","unstructured":"Berline, C., Grue, K.: A \u03ba-denotational semantics for Map Theory in ZFC+SI. Theoretical Computer Science\u00a0179(1-2), 137\u2013202 (1997)","journal-title":"Theoretical Computer Science"},{"key":"23_CR5","unstructured":"Bertot, Y., Cast\u00e9ran, P.: Interactive Theorem Proving and Program Development. Coq\u2019Art: The Calculus of Inductive Constructions. Texts in Theoretical Computer Science. Springer (2004), http:\/\/www.labri.fr\/publications\/l3a\/2004\/BC04"},{"key":"23_CR6","doi-asserted-by":"publisher","first-page":"79","DOI":"10.1016\/0168-0072(89)90026-2","volume":"43","author":"R.C. Flagg","year":"1989","unstructured":"Flagg, R.C., Myhill, J.: A type-free system extending ZFC. Annals of Pure and Applied Logic\u00a043, 79\u201397 (1989)","journal-title":"Annals of Pure and Applied Logic"},{"key":"23_CR7","unstructured":"Flatt, M.: PLT: Reference: Racket. Tech. Rep. PLT-TR-2010-1, PLT Inc. (2010), http:\/\/racket-lang.org\/tr1\/"},{"key":"23_CR8","unstructured":"Hrbacek, K., Jech, T.J.: Introduction to set theory. Pure and Applied Mathematics. M. Dekker (1999)"},{"key":"23_CR9","unstructured":"Hurd, J.: Formal Verification of Probabilistic Algorithms. Ph.D. thesis, University of Cambridge (2002)"},{"key":"23_CR10","doi-asserted-by":"publisher","first-page":"93","DOI":"10.1016\/S0304-3975(96)00171-5","volume":"175","author":"R. Kennaway","year":"1997","unstructured":"Kennaway, R., Klop, J.W., Sleep, M.R., Jan De Vries, F.: Infinitary lambda calculus. Theoretical Computer Science\u00a0175, 93\u2013125 (1997)","journal-title":"Theoretical Computer Science"},{"key":"23_CR11","doi-asserted-by":"crossref","unstructured":"Leivant, D.: Higher order logic. In: Handbook of Logic in Artificial Intelligence and Logic Programming, pp. 229\u2013321. Clarendon Press (1994)","DOI":"10.1093\/oso\/9780198537465.003.0004"},{"key":"23_CR12","unstructured":"Munkres, J.R.: Topology, 2nd edn. Prentice Hall (2000)"},{"key":"23_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"246","DOI":"10.1007\/978-3-540-71067-7_21","volume-title":"Theorem Proving in Higher Order Logics","author":"R. O\u2019Connor","year":"2008","unstructured":"O\u2019Connor, R.: Certified Exact Transcendental Real Number Computation in Coq. In: Mohamed, O.A., Mu\u00f1oz, C., Tahar, S. (eds.) TPHOLs 2008. LNCS, vol.\u00a05170, pp. 246\u2013261. Springer, Heidelberg (2008)"},{"key":"23_CR14","doi-asserted-by":"publisher","first-page":"143","DOI":"10.1016\/j.amc.2005.09.076","volume":"178","author":"T. Ord","year":"2006","unstructured":"Ord, T.: The many forms of hypercomputation. Applied Mathematics and Computation\u00a0178, 143\u2013153 (2006)","journal-title":"Applied Mathematics and Computation"},{"key":"23_CR15","doi-asserted-by":"publisher","first-page":"167","DOI":"10.1007\/BF00881916","volume":"15","author":"L.C. Paulson","year":"1995","unstructured":"Paulson, L.C.: Set theory for verification: II. Induction and recursion. Journal of Automated Reasoning\u00a015, 167\u2013215 (1995)","journal-title":"Journal of Automated Reasoning"},{"key":"23_CR16","doi-asserted-by":"publisher","first-page":"353","DOI":"10.1007\/BF00881873","volume":"11","author":"L.C. Paulson","year":"1993","unstructured":"Paulson, L.C.: Set theory for verification: I. From foundations to functions. Journal of Automated Reasoning\u00a011, 353\u2013389 (1993)","journal-title":"Journal of Automated Reasoning"},{"key":"23_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"89","DOI":"10.1007\/978-3-642-24276-2_6","volume-title":"Implementation and Application of Functional Languages","author":"N. Toronto","year":"2011","unstructured":"Toronto, N., McCarthy, J.: From Bayesian Notation to Pure Racket, via Measure-Theoretic Probability in \u03bb ZFC. In: Hage, J., Moraz\u00e1n, M.T. (eds.) IFL 2010. LNCS, vol.\u00a06647, pp. 89\u2013104. Springer, Heidelberg (2011)"},{"key":"23_CR18","doi-asserted-by":"publisher","first-page":"230","DOI":"10.1112\/plms\/s2-42.1.230","volume":"42","author":"A.M. Turing","year":"1936","unstructured":"Turing, A.M.: On computable numbers, with an application to the Entscheidungsproblem. Proceedings of the London Mathematical Society\u00a042, 230\u2013265 (1936)","journal-title":"Proceedings of the London Mathematical Society"},{"issue":"1","key":"23_CR19","doi-asserted-by":"crossref","first-page":"121","DOI":"10.1007\/s11225-005-6780-8","volume":"80","author":"A. Tzouvaras","year":"2005","unstructured":"Tzouvaras, A.: Cardinality without enumeration. Studia Logica: An International Journal for Symbolic Logic\u00a080(1), 121\u2013141 (2005)","journal-title":"Studia Logica: An International Journal for Symbolic Logic"},{"issue":"3","key":"23_CR20","doi-asserted-by":"publisher","first-page":"289","DOI":"10.2307\/421182","volume":"5","author":"G. Uzquiano","year":"1999","unstructured":"Uzquiano, G.: Models of second-order Zermelo set theory. The Bulletin of Symbolic Logic\u00a05(3), 289\u2013302 (1999)","journal-title":"The Bulletin of Symbolic Logic"},{"key":"23_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"530","DOI":"10.1007\/BFb0014566","volume-title":"Theoretical Aspects of Computer Software","author":"B. Werner","year":"1997","unstructured":"Werner, B.: Sets in Types, Types in Sets. In: Ito, T., Abadi, M. (eds.) TACS 1997. LNCS, vol.\u00a01281, pp. 530\u2013546. Springer, Heidelberg (1997)"}],"container-title":["Lecture Notes in Computer Science","Functional and Logic Programming"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-29822-6_23.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,4,24]],"date-time":"2024-04-24T17:44:56Z","timestamp":1713980696000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-29822-6_23"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012]]},"ISBN":["9783642298219","9783642298226"],"references-count":21,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-29822-6_23","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2012]]}}}