{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,10]],"date-time":"2026-04-10T03:12:00Z","timestamp":1775790720507,"version":"3.50.1"},"publisher-location":"Berlin, Heidelberg","reference-count":15,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540664635","type":"print"},{"value":"9783540482567","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1999]]},"DOI":"10.1007\/3-540-48256-3_6","type":"book-chapter","created":{"date-parts":[[2007,8,3]],"date-time":"2007-08-03T20:15:22Z","timestamp":1186172122000},"page":"73-90","source":"Crossref","is-referenced-by-count":12,"title":["Recursive Function Definition over Coinductive Types"],"prefix":"10.1007","author":[{"given":"John","family":"Matthews","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[1999,9,17]]},"reference":[{"key":"6_CR1","series-title":"UTM Series","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4612-0665-1","volume-title":"Topological Spaces: from distance to neighborhood","author":"G. a. Buskes","year":"1997","unstructured":"Buskes, G., and van Rooij, A. Topological Spaces: from distance to neighborhood. UTM Series. Springer, New York, 1997."},{"key":"6_CR2","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"89","DOI":"10.1007\/BFb0028388","volume-title":"Theorem Proving in Higher Order Logics: 10th International Conference, TPHOLs\u2019 97","author":"M. Devillers","year":"1997","unstructured":"Devillers, M., Griffioen, D., AND M\u00fcLLER, O. Possibly in finite sequences in theorem provers: A comparative study. In Theorem Proving in Higher Order Logics: 10th International Conference, TPHOLs\u2019 97 (Murray Hill, NJ, Aug. 1997), vol. 1275 of LNCS, Springer-Verlag, pp. 89\u2013104."},{"key":"6_CR3","unstructured":"Gordon, M. J. C., and Melham, t. F. Introduction to HOL: A theorem proving environment for higher order logic. Cambridge University Press, 1993."},{"key":"6_CR4","unstructured":"Gunter, C. A. Semantics of Programming Languages: Structures and Techniques. Foundations of Computing Science. The MIT Press, 1992."},{"key":"6_CR5","doi-asserted-by":"crossref","unstructured":"Matthews, J., and Launchbury, J. Elementary microarchitecture algebra. To appear in CAV99, International Conference on Computer Aided Verification, July 1999.","DOI":"10.1007\/3-540-48683-6_26"},{"key":"6_CR6","unstructured":"Matthews, J., Launchbury, J., and Cook, B. Specifying microprocessors in Hawk. In IEEE International Conference on Computer Languages (Chicago, Illinois, May 1998), pp. 90\u2013101."},{"key":"6_CR7","unstructured":"Miner, P. Hardware Verification Using Coinductive Assertions. PhD thesis, Indiana University, 1998."},{"key":"6_CR8","doi-asserted-by":"crossref","unstructured":"M\u00fcller, O., Nipkow, T., V. Oheimb, D., and Slotosch, O. HOLCF = HOL + LCF. To appear in Journal of Functional Programming, 1999.","DOI":"10.1017\/S095679689900341X"},{"key":"6_CR9","doi-asserted-by":"crossref","unstructured":"Paulson, L. Isabelle: A Generic Theorem Prover. Springer-Verlag, 1994.","DOI":"10.1007\/BFb0030541"},{"issue":"2","key":"6_CR10","doi-asserted-by":"publisher","first-page":"175","DOI":"10.1093\/logcom\/7.2.175","volume":"7","author":"L. C. Paulson","year":"1997","unstructured":"Paulson, L. C. Mechanizing coinduction and corecursion in higher-order logic. Journal of Logic and Computation 7,2 (Apr. 1997), 175\u2013204.","journal-title":"Journal of Logic and Computation"},{"key":"6_CR11","unstructured":"Rudin, W. Principles of Mathematical Analysis, 3 ed. McGraw-Hill, 1976."},{"key":"6_CR12","unstructured":"Rushby, J., and Stringer-calvert, D. W. J. A less elementary tutorial for the PVS specification and verification system. Tech. Rep. SRI-CSL-95-10, SRI International, Menlo Park, CA, June 1995. Revised, July 1996."},{"key":"6_CR13","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"381","DOI":"10.1007\/BFb0105417","volume-title":"Ninth international Conference on Theorem Proving in Higher Order Logics TPHOL","author":"K. Slind","year":"1996","unstructured":"Slind, K. Function definition in higher order logic. In Ninth international Conference on Theorem Proving in Higher Order Logics TPHOL (Turku, Finland, Aug. 1996), J. Von Wright, J. Grundy, and J. Harrison, Eds., vol. 1125 of Lecture Notes in Computer Science, Springer Verlag, pp. 381\u2013398."},{"key":"6_CR14","doi-asserted-by":"publisher","first-page":"275","DOI":"10.1007\/BFb0028400","volume":"1275","author":"K. Slind","year":"1997","unstructured":"Slind, K. Derivation and use of induction schemes in higher-order logic. Lecture Notes in Computer Science 1275 (1997), 275\u2013290.","journal-title":"Lecture Notes in Computer Science"},{"key":"6_CR15","volume-title":"Semantics of Programming Languages","author":"R. D. Tennent","year":"1991","unstructured":"Tennent, R. D. Semantics of Programming Languages. Prentice Hall, New York, 1991."}],"container-title":["Lecture Notes in Computer Science","Theorem Proving in Higher Order Logics"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-48256-3_6","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,1]],"date-time":"2019-05-01T18:58:35Z","timestamp":1556737115000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-48256-3_6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1999]]},"ISBN":["9783540664635","9783540482567"],"references-count":15,"URL":"https:\/\/doi.org\/10.1007\/3-540-48256-3_6","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[1999]]}}}