{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T21:15:19Z","timestamp":1725484519667},"publisher-location":"Berlin, Heidelberg","reference-count":22,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540415176"},{"type":"electronic","value":"9783540445579"}],"license":[{"start":{"date-parts":[[2000,1,1]],"date-time":"2000-01-01T00:00:00Z","timestamp":946684800000},"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":[[2000]]},"DOI":"10.1007\/3-540-44557-9_7","type":"book-chapter","created":{"date-parts":[[2007,5,31]],"date-time":"2007-05-31T23:04:24Z","timestamp":1180652664000},"page":"114-130","source":"Crossref","is-referenced-by-count":6,"title":["A Co-inductive Approach to Real Numbers"],"prefix":"10.1007","author":[{"given":"Alberto","family":"Ciaffaglione","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Pietro","family":"Di Gianantonio","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2002,6,11]]},"reference":[{"key":"7_CR1","doi-asserted-by":"crossref","unstructured":"R. Amadio and S. Coupet. \u201cAnalysis of a guard condition in Type Theory\u201d. Technical report, INRIA, 1997.","DOI":"10.1007\/BFb0053541"},{"key":"7_CR2","volume-title":"Foundations of constructive analysis","author":"E. Bishop","year":"1967","unstructured":"E. Bishop. \u201cFoundations of constructive analysis\u201d. McGraw-Hill, New York, 1967."},{"key":"7_CR3","unstructured":"L.E.J. Brouwer. \u201cBeweis, dass jede volle Funktion gleichm\u00e4ssig stetig ist\u201d. In Proc. Amsterdam 27, pages 189\u2013194, 1924."},{"key":"7_CR4","unstructured":"J. Cederquist. \u201cA pointfree approach to Constructive Analysis in Type Theory\u201d. PhD thesis, G\u00f6teborg University, 1997."},{"key":"7_CR5","series-title":"Lect Notes Comput Sci","volume-title":"Implementing constructive real analysis: preliminar report","author":"J. Chirimar","year":"1992","unstructured":"J. Chirimar and D.J. Howe. \u201cImplementing constructive real analysis: preliminar report\u201d. LNCS, 613, 1992."},{"key":"7_CR6","unstructured":"R.L. Constable. \u201cImplementing mathematics with the Nuprl development system\u201d. Prentice-Hall, 1986."},{"key":"7_CR7","unstructured":"T. Coquand. \u201cPattern-matching in Type Theory\u201d. In Informal Proceedings of the 1992 Workshop on Types for Proofs and Programs, 1992."},{"key":"7_CR8","series-title":"Lect Notes Comput Sci","volume-title":"1st Workshop on Types for Proofs and Programs","author":"T. Coquand","year":"1993","unstructured":"T. Coquand. \u201cInfinite objects in Type Theory\u201d. In 1st Workshop on Types for Proofs and Programs, LNCS 806, 1993."},{"key":"7_CR9","series-title":"Lect Notes Comput Sci","volume-title":"5th Workshop on Types for Proofs and Programs","author":"E. Gim\u00e9nez","year":"1994","unstructured":"E. Gim\u00e9nez. \u201cCodifying guarded definitions with recursion schemes\u201d. In 5th Workshop on Types for Proofs and Programs, LNCS 996, 1994."},{"key":"7_CR10","unstructured":"E. Gim\u00e9nez. \u201cA tutorial on recursive types in Coq\u201d. Technical report, INRIA, 1998."},{"key":"7_CR11","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","DOI":"10.1007\/BFb0097782","volume-title":"Proceedings of ICALP\u201998","author":"E. Gim\u00e9nez","year":"1998","unstructured":"E. Gim\u00e9nez. \u201cStructural recursive definitions in Type Theory\u201d. In Proceedings of ICALP\u201998, LNCS 1443, 1998."},{"key":"7_CR12","unstructured":"M.J.C. Gordon and T.F. Melham. \u201cIntroduction to HOL: a theorem proving environment for higher order logic\u201d. Cambridge University Press, 1993."},{"key":"7_CR13","unstructured":"J.R. Harrison. \u201cTheorem proving with real numbers\u201d. PhD thesis, Universitiy of Cambridge, 1996."},{"key":"7_CR14","unstructured":"INRIA, project Coq. \u201cThe Coq proof assistant-Reference manual V6.3.1\u201d, May 2000."},{"key":"7_CR15","unstructured":"C. Jones. \u201cCompleting the rationals and metric spaces in Lego\u201d. In Cambridge Universitiy Press, editor, Logical Frameworks, pages 209\u2013222. 1991."},{"key":"7_CR16","volume-title":"The implementation of Alf","author":"L. Magnusson","year":"1995","unstructured":"L. Magnusson. \u201cThe implementation of Alf\u201d. PhD thesis, Chalmers University of Technology, G\u00f6teborg, 1995."},{"key":"7_CR17","doi-asserted-by":"crossref","unstructured":"P.J. Potts, A. Edalat, and M.H. Escardo. \u201cSemantics of exact real arithmetic\u201d. In IEEE Symposium on Logic in Computer Science, 1997.","DOI":"10.1109\/LICS.1997.614952"},{"key":"7_CR18","unstructured":"C. Paulin-Mohring. \u201cInductive definitions inthe system Coq: rules and properties\u201d. In Proceedings of the TLCA, 1993."},{"key":"7_CR19","unstructured":"R. Pollack. \u201cThe theory of Lego, a proof checker for the Extended Calculus of Constructions\u201d. PhD thesis, University of Edimburgh, 1994."},{"key":"7_CR20","doi-asserted-by":"crossref","unstructured":"A. Simpson. \u201cLazy functional algorithms for exact real functionals\u201d. In MFCS 1998. Springer Verlag, 1998.","DOI":"10.1007\/BFb0055795"},{"key":"7_CR21","unstructured":"A.S. Troelstra and D. van Dalen. \u201cConstructivism in Mathematics\u201d. North-Holland, 1988."},{"key":"7_CR22","unstructured":"K. Weihrauch. \u201cA foundation for computable analysis\u201d. In Proceedings of DMTCS 1996, 1996."}],"container-title":["Lecture Notes in Computer Science","Types for Proofs and Programs"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-44557-9_7","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,4,28]],"date-time":"2019-04-28T11:19:15Z","timestamp":1556450355000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-44557-9_7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2000]]},"ISBN":["9783540415176","9783540445579"],"references-count":22,"URL":"https:\/\/doi.org\/10.1007\/3-540-44557-9_7","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2000]]}}}