{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,5]],"date-time":"2026-02-05T07:06:02Z","timestamp":1770275162782,"version":"3.49.0"},"publisher-location":"Berlin, Heidelberg","reference-count":22,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783662466773","type":"print"},{"value":"9783662466780","type":"electronic"}],"license":[{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2015]]},"DOI":"10.1007\/978-3-662-46678-0_26","type":"book-chapter","created":{"date-parts":[[2015,4,1]],"date-time":"2015-04-01T13:42:21Z","timestamp":1427895741000},"page":"407-421","source":"Crossref","is-referenced-by-count":19,"title":["Programming and Reasoning with Guarded Recursion for Coinductive Types"],"prefix":"10.1007","author":[{"given":"Ranald","family":"Clouston","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ale\u0161","family":"Bizjak","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Hans Bugge","family":"Grathwohl","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Lars","family":"Birkedal","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"26_CR1","doi-asserted-by":"crossref","unstructured":"Abel, A., Pientka, B.: Wellfounded recursion with copatterns: A unified approach to termination and productivity. In: ICFP, pp. 185\u2013196 (2013)","DOI":"10.1145\/2544174.2500591"},{"key":"26_CR2","doi-asserted-by":"crossref","unstructured":"Abel, A., Vezzosi, A.: A formalized proof of strong normalization for guarded recursive types. In: APLAS, pp. 140\u2013158 (2014)","DOI":"10.1007\/978-3-319-12736-1_8"},{"key":"26_CR3","doi-asserted-by":"crossref","unstructured":"Appel, A.W., Melli\u00e8s, P.A., Richards, C.D., Vouillon, J.: A very modal model of a modern, major, general type system. In: POPL, pp. 109\u2013122 (2007)","DOI":"10.1145\/1190215.1190235"},{"key":"26_CR4","doi-asserted-by":"crossref","unstructured":"Atkey, R., McBride, C.: Productive coprogramming with guarded recursion. In: ICFP, pp. 197\u2013208 (2013)","DOI":"10.1145\/2544174.2500597"},{"issue":"3","key":"26_CR5","doi-asserted-by":"publisher","first-page":"383","DOI":"10.1023\/A:1005291931660","volume":"65","author":"G.M. Bierman","year":"2000","unstructured":"Bierman, G.M., de Paiva, V.C.: On an intuitionistic modal logic. Studia Logica\u00a065(3), 383\u2013416 (2000)","journal-title":"Studia Logica"},{"key":"26_CR6","doi-asserted-by":"crossref","unstructured":"Birkedal, L., M\u00f8gelberg, R.E., Schwinghammer, J., St\u00f8vring, K.: First steps in synthetic guarded domain theory: step-indexing in the topos of trees. LMCS 8(4) (2012)","DOI":"10.2168\/LMCS-8(4:1)2012"},{"key":"26_CR7","unstructured":"Birkedal, L., Schwinghammer, J., St\u00f8vring, K.: A metric model of lambda calculus with guarded recursion. In: FICS, pp. 19\u201325 (2010)"},{"key":"26_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"108","DOI":"10.1007\/978-3-319-08918-8_8","volume-title":"Rewriting and Typed Lambda Calculi","author":"A. Bizjak","year":"2014","unstructured":"Bizjak, A., Birkedal, L., Miculan, M.: A model of countable nondeterminism in guarded type theory. In: Dowek, G. (ed.) RTA-TLCA 2014. LNCS, vol.\u00a08560, pp. 108\u2013123. Springer, Heidelberg (2014)"},{"key":"26_CR9","doi-asserted-by":"crossref","unstructured":"Clouston, R., Bizjak, A., Grathwohl, H.B., Birkedal, L.: Programming and reasoning with guarded recursion for coinductive types. arXiv:1501.02925 (2015)","DOI":"10.1007\/978-3-662-46678-0_26"},{"key":"26_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"133","DOI":"10.1007\/978-3-662-46678-0_9","volume-title":"Foundations of Software Science and Computation Structures","author":"R. Clouston","year":"2015","unstructured":"Clouston, R., Gor\u00e9, R.: Sequent calculus in the topos of trees. In: Pitts, A. (ed.) FoSSaCS 2015. LNCS, vol.\u00a09034, pp. 133\u2013147. Springer, Heidelberg (2015)"},{"key":"26_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"62","DOI":"10.1007\/3-540-58085-9_72","volume-title":"Types for Proofs and Programs","author":"T. Coquand","year":"1994","unstructured":"Coquand, T.: Infinite objects in type theory. In: Barendregt, H., Nipkow, T. (eds.) TYPES 1993. LNCS, vol.\u00a0806, pp. 62\u201378. Springer, Heidelberg (1994)"},{"key":"26_CR12","doi-asserted-by":"crossref","unstructured":"Endrullis, J., Grabmayer, C., Hendriks, D.: Mix-automatic sequences. In: Fields Workshop on Combinatorics on Words, contributed talk (2013)","DOI":"10.1007\/978-3-642-37064-9_24"},{"key":"26_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"39","DOI":"10.1007\/3-540-60579-7_3","volume-title":"Types for Proofs and Programs","author":"E. Gim\u00e9nez","year":"1995","unstructured":"Gim\u00e9nez, E.: Codifying guarded definitions with recursive schemes. In: Smith, J., Dybjer, P., Nordstr\u00f6m, B. (eds.) TYPES 1994. LNCS, vol.\u00a0996, pp. 39\u201359. Springer, Heidelberg (1995)"},{"key":"26_CR14","doi-asserted-by":"crossref","unstructured":"Hughes, J., Pareto, L., Sabry, A.: Proving the correctness of reactive systems using sized types. In: POPL, pp. 410\u2013423 (1996)","DOI":"10.1145\/237721.240882"},{"key":"26_CR15","doi-asserted-by":"crossref","unstructured":"Krishnaswami, N.R., Benton, N.: Ultrametric semantics of reactive programs. In: LICS, pp. 257\u2013266 (2011)","DOI":"10.1109\/LICS.2011.38"},{"issue":"1","key":"26_CR16","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1017\/S0956796807006326","volume":"18","author":"C. McBride","year":"2008","unstructured":"McBride, C., Paterson, R.: Applicative programming with effects. J. Funct. Programming\u00a018(1), 1\u201313 (2008)","journal-title":"J. Funct. Programming"},{"key":"26_CR17","doi-asserted-by":"crossref","unstructured":"Milius, S., Moss, L.S., Schwencke, D.: Abstract GSOS rules and a modular treatment of recursive definitions. LMCS 9(3) (2013)","DOI":"10.2168\/LMCS-9(3:28)2013"},{"key":"26_CR18","doi-asserted-by":"crossref","unstructured":"M\u00f8gelberg, R.E.: A type theory for productive coprogramming via guarded recursion. In: CSL-LICS (2014)","DOI":"10.1145\/2603088.2603132"},{"key":"26_CR19","doi-asserted-by":"crossref","unstructured":"Nakano, H.: A modality for recursion. In: LICS, pp. 255\u2013266 (2000)","DOI":"10.1109\/LICS.2000.855774"},{"key":"26_CR20","unstructured":"Prawitz, D.: Natural Deduction: A Proof-Theoretical Study. Dover Publ. (1965)"},{"issue":"1-3","key":"26_CR21","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/S0304-3975(02)00895-2","volume":"308","author":"J.J.M.M. Rutten","year":"2003","unstructured":"Rutten, J.J.M.M.: Behavioural differential equations: A coinductive calculus of streams, automata, and power series. Theor. Comput. Sci.\u00a0308(1-3), 1\u201353 (2003)","journal-title":"Theor. Comput. Sci."},{"key":"26_CR22","doi-asserted-by":"crossref","unstructured":"Severi, P.G., de Vries, F.J.J.: Pure type systems with corecursion on streams: from finite to infinitary normalisation. In: ICFP, pp. 141\u2013152 (2012)","DOI":"10.1145\/2398856.2364550"}],"container-title":["Lecture Notes in Computer Science","Foundations of Software Science and Computation Structures"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-662-46678-0_26","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,21]],"date-time":"2025-05-21T19:57:43Z","timestamp":1747857463000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-662-46678-0_26"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783662466773","9783662466780"],"references-count":22,"URL":"https:\/\/doi.org\/10.1007\/978-3-662-46678-0_26","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2015]]}}}