{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,5]],"date-time":"2026-02-05T09:46:58Z","timestamp":1770284818105,"version":"3.49.0"},"publisher-location":"Berlin, Heidelberg","reference-count":24,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783662496299","type":"print"},{"value":"9783662496305","type":"electronic"}],"license":[{"start":{"date-parts":[[2016,1,1]],"date-time":"2016-01-01T00:00:00Z","timestamp":1451606400000},"content-version":"tdm","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":[[2016]]},"DOI":"10.1007\/978-3-662-49630-5_2","type":"book-chapter","created":{"date-parts":[[2016,3,21]],"date-time":"2016-03-21T09:04:32Z","timestamp":1458551072000},"page":"20-35","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":30,"title":["Guarded Dependent Type Theory with Coinductive Types"],"prefix":"10.1007","author":[{"given":"Ale\u0161","family":"Bizjak","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Hans Bugge","family":"Grathwohl","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ranald","family":"Clouston","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Rasmus E.","family":"M\u00f8gelberg","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Lars","family":"Birkedal","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"2_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"},{"issue":"1","key":"2_CR2","doi-asserted-by":"crossref","first-page":"109","DOI":"10.1145\/1190215.1190235","volume":"42","author":"Andrew W. Appel","year":"2007","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)","journal-title":"ACM SIGPLAN Notices"},{"key":"2_CR3","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"},{"key":"2_CR4","doi-asserted-by":"crossref","unstructured":"Birkedal, L., M\u00f8gelberg, R.E.: Intensional type theory with guarded recursive types qua fixed points on universes. In: LICS, pp. 213\u2013222 (2013)","DOI":"10.1109\/LICS.2013.27"},{"key":"2_CR5","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":"2_CR6","first-page":"20","volume-title":"Lecture Notes in Computer Science","author":"Ale\u0161 Bizjak","year":"2016","unstructured":"Bizjak, A., Grathwohl, H.B., Clouston, R., M\u00f8gelberg, R.E., Birkedal, L.: Guarded dependent type theory with coinductive types (2016). http:\/\/arxiv.org\/abs\/1601.01586"},{"key":"2_CR7","doi-asserted-by":"crossref","first-page":"83","DOI":"10.1016\/j.entcs.2015.12.007","volume":"319","author":"Ale\u0161 Bizjak","year":"2015","unstructured":"Bizjak, A., M\u00f8gelberg, R.E.: A model of guarded recursion with clock synchronisation. In: MFPS (2015)","journal-title":"Electronic Notes in Theoretical Computer Science"},{"issue":"5","key":"2_CR8","doi-asserted-by":"publisher","first-page":"552","DOI":"10.1017\/S095679681300018X","volume":"23","author":"E Brady","year":"2013","unstructured":"Brady, E.: Idris, a general-purpose dependently typed programming language: design and implementation. J. Funct. Program. 23(5), 552\u2013593 (2013)","journal-title":"J. Funct. Program."},{"key":"2_CR9","doi-asserted-by":"crossref","unstructured":"Clouston, R., Bizjak, A., Grathwohl, H.B., Birkedal, L.: Programming and reasoning with guarded recursion for coinductive types. In: FoSSaCS (2015)","DOI":"10.1007\/978-3-662-46678-0_26"},{"key":"2_CR10","unstructured":"Cohen, C., Coquand, T., Huber, S., M\u00f6rtberg, A.: Cubical type theory: a constructive interpretation of the univalence axiom, unpublished (2015)"},{"key":"2_CR11","volume-title":"Implementing Mathematics with the Nuprl Proof Development System","author":"RL Constable","year":"1986","unstructured":"Constable, R.L., Allen, S.F., Bromley, H.M., Cleaveland, W.R., Cremer, J.F., Harper, R.W., Howe, D.J., Knoblock, T.B., Mendler, N.P., Panangaden, P., Sasaki, J.T., Smith, S.F.: Implementing Mathematics with the Nuprl Proof Development System. Prentice-Hall Inc, Upper Saddle River, NJ, USA (1986)"},{"key":"2_CR12","first-page":"62","volume-title":"Lecture Notes in Computer Science","author":"Thierry Coquand","year":"1994","unstructured":"Coquand, T.: Infinite objects in type theory. In: TYPES, pp. 62\u201378 (1993)"},{"key":"2_CR13","doi-asserted-by":"crossref","unstructured":"Gim\u00e9nez, E.: Codifying guarded definitions with recursive schemes. In: TYPES, pp. 39\u201359 (1995)","DOI":"10.1007\/3-540-60579-7_3"},{"key":"2_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":"2_CR15","series-title":"Studies in Logic and the Foundations of Mathematics","volume-title":"Categorical Logic and Type Theory","author":"B Jacobs","year":"1999","unstructured":"Jacobs, B.: Categorical Logic and Type Theory. Studies in Logic and the Foundations of Mathematics, vol. 141. North Holland, Amsterdam (1999)"},{"key":"2_CR16","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"},{"key":"2_CR17","unstructured":"The Coq development team: the coq proof assistant reference manual. LogiCal Project (2004). version 8.0. http:\/\/coq.inria.fr"},{"issue":"1","key":"2_CR18","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. Program. 18(1), 1\u201313 (2008)","journal-title":"J. Funct. Program."},{"key":"2_CR19","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":"2_CR20","doi-asserted-by":"crossref","unstructured":"Nakano, H.: A modality for recursion. In: LICS, pp. 255\u2013266 (2000)","DOI":"10.1109\/LICS.2000.855774"},{"key":"2_CR21","unstructured":"Norell, U.: Towards a practical programming language based on dependent type theory. Ph.D. thesis, Chalmers University of Technology (2007)"},{"key":"2_CR22","doi-asserted-by":"crossref","unstructured":"Paviotti, M., M\u00f8gelberg, R.E., Birkedal, L.: A model of PCF in guarded type theory. In: MFPS (2015)","DOI":"10.1016\/j.entcs.2015.12.020"},{"key":"2_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"149","DOI":"10.1007\/978-3-642-54833-8_9","volume-title":"Programming Languages and Systems","author":"K Svendsen","year":"2014","unstructured":"Svendsen, K., Birkedal, L.: Impredicative concurrent abstract predicates. In: Shao, Z. (ed.) ESOP 2014 (ETAPS). LNCS, vol. 8410, pp. 149\u2013168. Springer, Heidelberg (2014)"},{"key":"2_CR24","unstructured":"The Univalent Foundations Program: Homotopy Type Theory: Univalent Foundations of Mathematics, Institute for Advanced Study (2013). http:\/\/homotopytypetheory.org\/book"}],"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-49630-5_2","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,1]],"date-time":"2025-06-01T21:30:00Z","timestamp":1748813400000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-662-49630-5_2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016]]},"ISBN":["9783662496299","9783662496305"],"references-count":24,"URL":"https:\/\/doi.org\/10.1007\/978-3-662-49630-5_2","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2016]]},"assertion":[{"value":"This content has been made available to all.","name":"free","label":"Free to read"}]}}