{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,9]],"date-time":"2024-09-09T22:44:38Z","timestamp":1725921878959},"publisher-location":"Cham","reference-count":34,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319720555"},{"type":"electronic","value":"9783319720562"}],"license":[{"start":{"date-parts":[[2017,11,28]],"date-time":"2017-11-28T00:00:00Z","timestamp":1511827200000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2018]]},"DOI":"10.1007\/978-3-319-72056-2_3","type":"book-chapter","created":{"date-parts":[[2017,11,27]],"date-time":"2017-11-27T09:33:31Z","timestamp":1511775211000},"page":"37-54","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["A Minimal Computational Theory of a Minimal Computational Universe"],"prefix":"10.1007","author":[{"given":"Arnon","family":"Avron","sequence":"first","affiliation":[]},{"given":"Liron","family":"Cohen","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2017,11,28]]},"reference":[{"key":"3_CR1","unstructured":"Aczel, P., Rathjen, M.: Notes on constructive set theory. Technical report 40, Mittag-Leffler (2001)"},{"issue":"4","key":"3_CR2","doi-asserted-by":"crossref","first-page":"66","DOI":"10.1145\/2591012","volume":"57","author":"J Avigad","year":"2014","unstructured":"Avigad, J., Harrison, J.: Formally verified mathematics. Commun. ACM 57(4), 66\u201375 (2014)","journal-title":"Commun. ACM"},{"key":"3_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"87","DOI":"10.1007\/978-3-540-78127-1_6","volume-title":"Pillars of Computer Science","author":"A Avron","year":"2008","unstructured":"Avron, A.: A framework for formalizing set theories based on the use of static set terms. In: Avron, A., Dershowitz, N., Rabinovich, A. (eds.) Pillars of Computer Science. LNCS, vol. 4800, pp. 87\u2013106. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-78127-1_6"},{"key":"3_CR4","doi-asserted-by":"crossref","unstructured":"Avron, A.: A new approach to predicative set theory. In: Schindler, R. (ed.) Ways of Proof Theory, Onto Series in Mathematical Logic, pp. 31\u201363. Verlag (2010)","DOI":"10.1515\/9783110324907.31"},{"issue":"1","key":"3_CR5","first-page":"53","volume":"9","author":"A Avron","year":"2016","unstructured":"Avron, A., Cohen, L.: Formalizing scientifically applicable mathematics in a definitional framework. J. Formalized Reasoning 9(1), 53\u201370 (2016)","journal-title":"J. Formalized Reasoning"},{"issue":"3","key":"3_CR6","doi-asserted-by":"crossref","first-page":"730","DOI":"10.1017\/jsl.2015.26","volume":"80","author":"A Beckmann","year":"2015","unstructured":"Beckmann, A., Buss, S.R., Friedman, S.D.: Safe recursive set functions. J. Symbolic Logic 80(3), 730\u2013762 (2015)","journal-title":"J. Symbolic Logic"},{"key":"3_CR7","volume-title":"Foundations of Constructive Mathematics: Metamathematical Studies","author":"MJ Beeson","year":"2012","unstructured":"Beeson, M.J.: Foundations of Constructive Mathematics: Metamathematical Studies, vol. 6. Springer Science & Business Media, Boston (2012)"},{"key":"3_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-85110-3","volume-title":"Intelligent Computer Mathematics","year":"2008","unstructured":"Autexier, S., Campbell, J., Rubio, J., Sorge, V., Suzuki, M., Wiedijk, F. (eds.): CICM 2008. LNCS, vol. 5144. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-85110-3"},{"key":"3_CR9","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4757-3452-2","volume-title":"Set Theory for Computing: From Decision Procedures to Declarative Programming with Sets","author":"D Cantone","year":"2001","unstructured":"Cantone, D., Omodeo, E., Policriti, A.: Set Theory for Computing: From Decision Procedures to Declarative Programming with Sets. Springer, New York (2001)"},{"key":"3_CR10","doi-asserted-by":"crossref","DOI":"10.7551\/mitpress\/9153.001.0001","volume-title":"Certified Programming with Dependent Types","author":"A Chlipala","year":"2013","unstructured":"Chlipala, A.: Certified Programming with Dependent Types. MIT Press, Cambridge (2013)"},{"key":"3_CR11","doi-asserted-by":"crossref","unstructured":"Cohen, L., Avron, A.: The middle ground-ancestral logic. Synthese, 1\u201323 (2015)","DOI":"10.1007\/s11229-015-0784-3"},{"key":"3_CR12","volume-title":"Implementing Mathematics with the Nuprl Proof Development System","author":"RL Constable","year":"1986","unstructured":"Constable, R.L., Allen, S.F., Bromley, M., Cleaveland, R., et al.: Implementing Mathematics with the Nuprl Proof Development System. Prentice Hall, Englewood Cliffs (1986)"},{"issue":"12","key":"3_CR13","doi-asserted-by":"crossref","first-page":"177","DOI":"10.1002\/malq.19720181202","volume":"18","author":"J Corcoran","year":"1972","unstructured":"Corcoran, J., Hatcher, W., Herring, J.: Variable binding term operators. Math. Logic Q. 18(12), 177\u2013182 (1972)","journal-title":"Math. Logic Q."},{"key":"3_CR14","series-title":"Perspectives in Mathematical Logic","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-662-21723-8","volume-title":"Constructibility","author":"K Devlin","year":"1984","unstructured":"Devlin, K.: Constructibility. Perspectives in Mathematical Logic. Springer, Heidelberg (1984)"},{"issue":"01","key":"3_CR15","doi-asserted-by":"crossref","first-page":"1","DOI":"10.2307\/2269764","volume":"29","author":"S Feferman","year":"1964","unstructured":"Feferman, S.: Systems of predicative analysis. J. Symbolic Logic 29(01), 1\u201330 (1964)","journal-title":"J. Symbolic Logic"},{"issue":"02","key":"3_CR16","doi-asserted-by":"crossref","first-page":"193","DOI":"10.2307\/2269866","volume":"33","author":"S Feferman","year":"1968","unstructured":"Feferman, S.: Systems of predicative analysis, II: representations of ordinals. J. Symbolic Logic 33(02), 193\u2013220 (1968)","journal-title":"J. Symbolic Logic"},{"key":"3_CR17","doi-asserted-by":"crossref","unstructured":"Feferman, S.: Why a little bit goes a long way: logical foundations of scientifically applicable mathematics. In: PSA: Proceedings of the Biennial Meeting of the Philosophy of Science Association, pp. 442\u2013455. JSTOR (1992)","DOI":"10.1086\/psaprocbienmeetp.1992.2.192856"},{"issue":"10","key":"3_CR18","doi-asserted-by":"crossref","first-page":"971","DOI":"10.1016\/j.ic.2008.04.007","volume":"207","author":"S Feferman","year":"2009","unstructured":"Feferman, S.: Operational set theory and small large cardinals. Inf. Comput. 207(10), 971\u2013979 (2009)","journal-title":"Inf. Comput."},{"issue":"1","key":"3_CR19","doi-asserted-by":"crossref","first-page":"1","DOI":"10.2307\/1971023","volume":"105","author":"H Friedman","year":"1977","unstructured":"Friedman, H.: Set theoretic foundations for constructive analysis. Ann. Math. 105(1), 1\u201328 (1977)","journal-title":"Ann. Math."},{"key":"3_CR20","doi-asserted-by":"crossref","unstructured":"Gandy, R.O.: Set-theoretic functions for elementary syntax. In: Proceedings of Symposia in Pure Mathematics, vol. 13, pp. 103\u2013126 (1974)","DOI":"10.1090\/pspum\/013.2\/0376348"},{"issue":"3","key":"3_CR21","doi-asserted-by":"crossref","first-page":"275","DOI":"10.1017\/bsl.2014.21","volume":"20","author":"G J\u00e4ger","year":"2014","unstructured":"J\u00e4ger, G., Zumbrunnen, R.: Explicit mathematics and operational set theory: some ontological comparisons. Bull. Symbolic Logic 20(3), 275\u2013292 (2014)","journal-title":"Bull. Symbolic Logic"},{"issue":"3","key":"3_CR22","doi-asserted-by":"crossref","first-page":"229","DOI":"10.1016\/0003-4843(72)90001-0","volume":"4","author":"RB Jensen","year":"1972","unstructured":"Jensen, R.B.: The fine structure of the constructible hierarchy. Ann. Math. Logic 4(3), 229\u2013308 (1972)","journal-title":"Ann. Math. Logic"},{"key":"3_CR23","doi-asserted-by":"crossref","DOI":"10.1007\/978-94-017-0253-9","volume-title":"Thirty Five Years of Automating Mathematics","author":"FD Kamareddine","year":"2003","unstructured":"Kamareddine, F.D.: Thirty Five Years of Automating Mathematics, vol. 28. Springer, Netherlands (2003)"},{"issue":"1","key":"3_CR24","doi-asserted-by":"crossref","first-page":"3","DOI":"10.1215\/00294527-2835101","volume":"56","author":"ARD Mathias","year":"2015","unstructured":"Mathias, A.R.D., Bowler, N.J., et al.: Rudimentary recursion, gentle functions and provident sets. Notre Dame J. Formal Logic 56(1), 3\u201360 (2015)","journal-title":"Notre Dame J. Formal Logic"},{"key":"3_CR25","volume-title":"Metamath: A Computer Language for Pure Mathematics","author":"N Megill","year":"1997","unstructured":"Megill, N.: Metamath: A Computer Language for Pure Mathematics. Elsevier Science, Amsterdam (1997)"},{"issue":"03","key":"3_CR26","doi-asserted-by":"crossref","first-page":"347","DOI":"10.2307\/2272159","volume":"40","author":"J Myhill","year":"1975","unstructured":"Myhill, J.: Constructive set theory. J. Symbolic Logic 40(03), 347\u2013382 (1975)","journal-title":"J. Symbolic Logic"},{"key":"3_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45949-9","volume-title":"Isabelle\/HOL: A Proof Assistant for Higher-Order Logic","year":"2002","unstructured":"Nipkow, T., Wenzel, M., Paulson, L.C. (eds.): Isabelle\/HOL: A Proof Assistant for Higher-Order Logic. LNCS, vol. 2283. Springer, Heidelberg (2002). https:\/\/doi.org\/10.1007\/3-540-45949-9"},{"issue":"4","key":"3_CR28","doi-asserted-by":"crossref","first-page":"743","DOI":"10.2307\/2373917","volume":"101","author":"RH Risch","year":"1979","unstructured":"Risch, R.H.: Algebraic properties of the elementary functions of analysis. Am. J. Math. 101(4), 743\u2013759 (1979)","journal-title":"Am. J. Math."},{"key":"3_CR29","unstructured":"Rudnicki, P.: An overview of the MIZAR project. In: Proceedings of the 1992 Workshop on Types for Proofs and Programs, pp. 311\u2013330 (1992)"},{"key":"3_CR30","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4613-9575-1","volume-title":"Programming with Sets: An Introduction to SETL","author":"JT Schwartz","year":"1986","unstructured":"Schwartz, J.T., Dewar, R.B., Schonberg, E., Dubinsky, E.: Programming with Sets: An Introduction to SETL. Springer-Verlag New York Inc., New York (1986). https:\/\/doi.org\/10.1007\/978-1-4613-9575-1"},{"key":"3_CR31","volume-title":"Foundations Without Foundationalism: A Case for Second-Order Logic","author":"S Shapiro","year":"1991","unstructured":"Shapiro, S.: Foundations Without Foundationalism: A Case for Second-Order Logic. Oxford University Press, Oxford (1991)"},{"key":"3_CR32","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9780511581007","volume-title":"Subsystems of Second Order Arithmetic","author":"SG Simpson","year":"2009","unstructured":"Simpson, S.G.: Subsystems of Second Order Arithmetic, vol. 1. Cambridge University Press, Cambridge (2009)"},{"key":"3_CR33","unstructured":"Weaver, N.: Analysis in $${J}_2$$ J 2 . arXiv preprint arXiv:math\/0509245 (2005)"},{"key":"3_CR34","unstructured":"Weyl, H.: Das Kontinuum: Kritische Untersuchungen \u00fcber die Grundlagen der Analysis. W. de Gruyter (1932)"}],"container-title":["Lecture Notes in Computer Science","Logical Foundations of Computer Science"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-72056-2_3","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,10,6]],"date-time":"2019-10-06T21:30:15Z","timestamp":1570397415000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-72056-2_3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,11,28]]},"ISBN":["9783319720555","9783319720562"],"references-count":34,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-72056-2_3","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2017,11,28]]}}}