{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,28]],"date-time":"2025-10-28T00:25:54Z","timestamp":1761611154801},"reference-count":23,"publisher":"Springer Science and Business Media LLC","issue":"1-2","license":[{"start":{"date-parts":[[1994,7,1]],"date-time":"1994-07-01T00:00:00Z","timestamp":773020800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Form Method Syst Des"],"published-print":{"date-parts":[[1994,7]]},"DOI":"10.1007\/bf01384233","type":"journal-article","created":{"date-parts":[[2005,4,2]],"date-time":"2005-04-02T02:09:32Z","timestamp":1112407772000},"page":"35-59","source":"Crossref","is-referenced-by-count":20,"title":["Constructing the real numbers in HOL"],"prefix":"10.1007","volume":"5","author":[{"given":"John","family":"Harrison","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"CR1","doi-asserted-by":"crossref","first-page":"345","DOI":"10.1007\/BF01187947","volume":"63","author":"F.A. Behrend","year":"1956","unstructured":"Behrend, F.A.,A Contribution to the Theory of Magnitudes and the Foundations of Analysis, Mathematische Zeitschrift, vol. 63, pp. 345?362, 1956.","journal-title":"Mathematische Zeitschrift"},{"key":"CR2","doi-asserted-by":"crossref","unstructured":"Bishop, E. and Bridges, D.,Constructive analysis, Springer-Verlag, 1985.","DOI":"10.1007\/978-3-642-61667-9"},{"key":"CR3","unstructured":"Bourbaki, N.,Elements of mathematics, vol. 3: General Topology, part 1, Hermann 1966."},{"key":"CR4","doi-asserted-by":"crossref","first-page":"100","DOI":"10.1016\/1385-7258(76)90055-X","volume":"38","author":"N.G. Bruijn de","year":"1976","unstructured":"de Bruijn, N.G.,Defining Reals Without the Use of Rationals, Indagationes Mathematicae, vol. 38, pp. 100?108, 1976.","journal-title":"Indagationes Mathematicae"},{"key":"CR5","unstructured":"Burkill, J.C.,A First Course in Mathematical Analysis, Cambridge 1962."},{"key":"CR6","unstructured":"Burkill, J.C. and Burkill, H.,A Second Course in Mathematical Analysis, Cambridge 1970."},{"key":"CR7","unstructured":"Burrill, C.W.,Foundations of Real Numbers, McGraw-Hill 1967."},{"key":"CR8","doi-asserted-by":"crossref","unstructured":"Chirimar, J., Howe and D.J.,Implementing Constructive Real Analysis, preprint 1992.","DOI":"10.1007\/BFb0021090"},{"key":"CR9","unstructured":"Cohen, L.W., and Ehrlich, G.,Structure of the real number system, Van Nostrand 1963."},{"key":"CR10","unstructured":"Conway, J.H.,On Numbers and Games, Academic Press 1976."},{"key":"CR11","doi-asserted-by":"crossref","first-page":"278","DOI":"10.1016\/0001-8708(75)90115-2","volume":"16","author":"F. Faltin","year":"1975","unstructured":"Faltin, F., Metropolis, N., Ross, B. and Rota, G.-C.,The Real Numbers as a Wreath Product Advances in Mathematics, vol. 16, pp. 278?304, 1975.","journal-title":"Advances in Mathematics"},{"key":"CR12","unstructured":"Golan, J.S.,The Theory of Semirings with Applications in Mathematics and Computer Science, Longman 1992."},{"key":"CR13","first-page":"351","volume":"698","author":"J.R. Harrison","year":"1993","unstructured":"Harrison, J.R. and Th\u00e9ry, L.,Reasoning About the Reals: The Marriage of HOL and Maple, Proceedings of the 4th International Conference on Logic Programming and Automated Reasoning (LPAR 93), Springer Lecture Notes in Artificial Intelligence vol. 698, pp. 351?353, 1993.","journal-title":"Proceedings of the 4th International Conference on Logic Programming and Automated Reasoning (LPAR 93), Springer Lecture Notes in Artificial Intelligence"},{"key":"CR14","unstructured":"IEEE,Standard for Binary Floating Point Arithmetic, ANSI\/IEEE Standard 754?1985."},{"key":"CR15","unstructured":"Jones, C.,Completing the Rationals and Metric Spaces in LEGO, Proceedings of the 2nd Workshop on Logical Frameworks, Edinburgh 1991."},{"key":"CR16","unstructured":"Jutting, L.S.,Checking Landau's ?Grundlagen? in the Automath System, PhD thesis, Eindhoven University of Technology 1977."},{"key":"CR17","unstructured":"Kelley, J.L.,General Topology, Van Nostrand 1955."},{"key":"CR18","first-page":"40","volume":"98","author":"S. Kuhn","year":"1991","unstructured":"Kuhn, S.,The Derivative \u00e0 la Carath\u00e9odory, American Mathematical Monthly, vol. 98, pp. 40?44, 1991.","journal-title":"American Mathematical Monthly"},{"key":"CR19","unstructured":"Landau, E.,Foundations of analysis, Chelsea 1951."},{"key":"CR20","unstructured":"Pnueli, A.,From Timed To Hybrid Systems, preprint 1992."},{"key":"CR21","unstructured":"Stoll, R.R.,Set theory and logic, Dover 1979."},{"key":"CR22","unstructured":"Thurston, H.A.,The number system, Blackie 1956."},{"key":"CR23","unstructured":"Wallis, P.J.L.,Improving floating-point programming, Wiley 1990."}],"container-title":["Formal Methods in System Design"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BF01384233.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/BF01384233\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BF01384233","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,4,6]],"date-time":"2020-04-06T16:22:54Z","timestamp":1586190174000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BF01384233"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1994,7]]},"references-count":23,"journal-issue":{"issue":"1-2","published-print":{"date-parts":[[1994,7]]}},"alternative-id":["BF01384233"],"URL":"https:\/\/doi.org\/10.1007\/bf01384233","relation":{},"ISSN":["0925-9856","1572-8102"],"issn-type":[{"value":"0925-9856","type":"print"},{"value":"1572-8102","type":"electronic"}],"subject":[],"published":{"date-parts":[[1994,7]]}}}