{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,5]],"date-time":"2025-10-05T04:35:47Z","timestamp":1759638947417,"version":"3.40.3"},"publisher-location":"Cham","reference-count":37,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030025076"},{"type":"electronic","value":"9783030025083"}],"license":[{"start":{"date-parts":[[2018,1,1]],"date-time":"2018-01-01T00:00:00Z","timestamp":1514764800000},"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":[[2018]]},"DOI":"10.1007\/978-3-030-02508-3_11","type":"book-chapter","created":{"date-parts":[[2018,10,13]],"date-time":"2018-10-13T14:22:47Z","timestamp":1539440567000},"page":"191-210","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["A Metalanguage for Guarded Iteration"],"prefix":"10.1007","author":[{"given":"Sergey","family":"Goncharov","sequence":"first","affiliation":[]},{"given":"Christoph","family":"Rauch","sequence":"additional","affiliation":[]},{"given":"Lutz","family":"Schr\u00f6der","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2018,10,15]]},"reference":[{"key":"11_CR1","doi-asserted-by":"publisher","first-page":"121","DOI":"10.1007\/978-3-319-06025-5_5","volume-title":"Johan van Benthem on Logic and Information Dynamics","author":"S Abramsky","year":"2014","unstructured":"Abramsky, S.: Intensionality, definability and computation. In: Baltag, A., Smets, S. (eds.) Johan van Benthem on Logic and Information Dynamics, pp. 121\u2013142. Springer, Cham (2014). \n                      https:\/\/doi.org\/10.1007\/978-3-319-06025-5_5"},{"key":"11_CR2","doi-asserted-by":"publisher","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: Proceedings of 34th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. POPL 2007, January 2007, Nice, pp. 109\u2013122. ACM Press, New York (2007). \n                      https:\/\/doi.org\/10.1145\/1190216.1190235","DOI":"10.1145\/1190216.1190235"},{"issue":"4","key":"11_CR3","doi-asserted-by":"publisher","first-page":"395","DOI":"10.1017\/s0956796801004099","volume":"11","author":"N Benton","year":"2001","unstructured":"Benton, N., Kennedy, A.: Exceptional syntax. J. Funct. Program. 11(4), 395\u2013410 (2001). \n                      https:\/\/doi.org\/10.1017\/s0956796801004099","journal-title":"J. Funct. Program."},{"key":"11_CR4","doi-asserted-by":"publisher","DOI":"10.1016\/b978-0-444-82830-9.x5017-6","volume-title":"Handbook of Process Algebra","year":"2001","unstructured":"Bergstra, J., Ponse, A., Smolka, S. (eds.): Handbook of Process Algebra. Elsevier, New York City (2001). \n                      https:\/\/doi.org\/10.1016\/b978-0-444-82830-9.x5017-6"},{"issue":"4","key":"11_CR5","doi-asserted-by":"publisher","first-page":"1","DOI":"10.2168\/lmcs-8(4:1)2012","volume":"8","author":"L Birkedal","year":"2012","unstructured":"Birkedal, L., M\u00f8gelberg, R., Schwinghammer, J., St\u00f8vring, K.: First steps in synthetic guarded domain theory: step-indexing in the topos of trees. Log. Methods Comput. Sci. 8(4), 1 (2012). \n                      https:\/\/doi.org\/10.2168\/lmcs-8(4:1)2012","journal-title":"Log. Methods Comput. Sci."},{"key":"11_CR6","series-title":"EATCS Monographs on Theoretical Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-78034-9","volume-title":"Iteration Theories: The Equational Logic of Iterative Processes","author":"S Bloom","year":"1993","unstructured":"Bloom, S., \u00c9sik, Z.: Iteration Theories: The Equational Logic of Iterative Processes. EATCS Monographs on Theoretical Computer Science. Springer, Heidelberg (1993). \n                      https:\/\/doi.org\/10.1007\/978-3-642-78034-9"},{"key":"11_CR7","doi-asserted-by":"crossref","unstructured":"Brookes, S., Van Stone, K.: Monads and comonads in intensional semantics. Technical report CMU-CS-93-140, Department of Computer Science, Carnegie-Mellon University, Pittsburgh, PA (1993)","DOI":"10.21236\/ADA266522"},{"key":"11_CR8","doi-asserted-by":"publisher","first-page":"145","DOI":"10.1016\/0022-4049(93)90035-r","volume":"84","author":"A Carboni","year":"1993","unstructured":"Carboni, A., Lack, S., Walters, R.: Introduction to extensive and distributive categories. J. Pure. Appl. Algebra 84, 145\u2013158 (1993). \n                      https:\/\/doi.org\/10.1016\/0022-4049(93)90035-r","journal-title":"J. Pure. Appl. Algebra"},{"issue":"3","key":"11_CR9","doi-asserted-by":"publisher","first-page":"7","DOI":"10.2168\/lmcs-12(3:7)2016","volume":"12","author":"R Clouston","year":"2016","unstructured":"Clouston, R., Bizjak, A., Grathwohl, H.B., Birkedal, L.: The guarded lambda-calculus: programming and reasoning with guarded recursion for coinductive types. Log. Methods Comput. Sci. 12(3), 7 (2016). \n                      https:\/\/doi.org\/10.2168\/lmcs-12(3:7)2016","journal-title":"Log. Methods Comput. Sci."},{"issue":"3","key":"11_CR10","doi-asserted-by":"publisher","first-page":"277","DOI":"10.1017\/s0960129500000232","volume":"3","author":"JRB Cockett","year":"1993","unstructured":"Cockett, J.R.B.: Introduction to distributive categories. Math. Struct. Comput. Sci. 3(3), 277\u2013307 (1993). \n                      https:\/\/doi.org\/10.1017\/s0960129500000232","journal-title":"Math. Struct. Comput. Sci."},{"key":"11_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. 806, pp. 62\u201378. Springer, Heidelberg (1994). \n                      https:\/\/doi.org\/10.1007\/3-540-58085-9_72"},{"key":"11_CR12","unstructured":"Escard\u00f3, M.: A metric model of PCF. Paper Presented at Workshop on Realizability Semantics and Applications, June\u2013July 1999, Trento (1999). \n                      http:\/\/www.cs.bham.ac.uk\/~mhe\/papers\/metricpcf.pdf"},{"key":"11_CR13","doi-asserted-by":"publisher","first-page":"127","DOI":"10.1016\/j.entcs.2016.09.035","volume":"325","author":"B Geron","year":"2016","unstructured":"Geron, B., Levy, P.B.: Iteration and labelled iteration. Electron. Notes Theor. Comput. Sci. 325, 127\u2013146 (2016). \n                      https:\/\/doi.org\/10.1016\/j.entcs.2016.09.035","journal-title":"Electron. Notes Theor. Comput. Sci."},{"key":"11_CR14","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: Dybjer, P., Nordstr\u00f6m, B., Smith, J. (eds.) TYPES 1994. LNCS, vol. 996, pp. 39\u201359. Springer, Heidelberg (1995). \n                      https:\/\/doi.org\/10.1007\/3-540-60579-7_3"},{"key":"11_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"397","DOI":"10.1007\/BFb0055070","volume-title":"Automata, Languages and Programming","author":"E Gim\u00e9nez","year":"1998","unstructured":"Gim\u00e9nez, E.: Structural recursive definitions in type theory. In: Larsen, K.G., Skyum, S., Winskel, G. (eds.) ICALP 1998. LNCS, vol. 1443, pp. 397\u2013408. Springer, Heidelberg (1998). \n                      https:\/\/doi.org\/10.1007\/BFb0055070"},{"key":"11_CR16","doi-asserted-by":"publisher","first-page":"147","DOI":"10.1016\/j.entcs.2016.09.036","volume":"325","author":"S Goncharov","year":"2016","unstructured":"Goncharov, S., Milius, S., Rauch, C.: Complete Elgot monads and coalgebraic resumptions. Electron. Notes Theor. Comput. Sci. 325, 147\u2013168 (2016). \n                      https:\/\/doi.org\/10.1016\/j.entcs.2016.09.036","journal-title":"Electron. Notes Theor. Comput. Sci."},{"key":"11_CR17","doi-asserted-by":"publisher","first-page":"183","DOI":"10.1016\/j.entcs.2015.12.012","volume":"319","author":"S Goncharov","year":"2015","unstructured":"Goncharov, S., Rauch, C., Schr\u00f6der, L.: Unguarded recursion on coinductive resumptions. Electron. Notes Theor. Comput. Sci. 319, 183\u2013198 (2015). \n                      https:\/\/doi.org\/10.1016\/j.entcs.2015.12.012","journal-title":"Electron. Notes Theor. Comput. Sci."},{"key":"11_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"313","DOI":"10.1007\/978-3-319-89366-2_17","volume-title":"Foundations of Software Science and Computation Structures","author":"S Goncharov","year":"2018","unstructured":"Goncharov, S., Schr\u00f6der, L.: Guarded traced categories. In: Baier, C., Dal Lago, U. (eds.) FoSSaCS 2018. LNCS, vol. 10803, pp. 313\u2013330. Springer, Cham (2018). \n                      https:\/\/doi.org\/10.1007\/978-3-319-89366-2_17"},{"key":"11_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"517","DOI":"10.1007\/978-3-662-54458-7_30","volume-title":"Foundations of Software Science and Computation Structures","author":"S Goncharov","year":"2017","unstructured":"Goncharov, S., Schr\u00f6der, L., Rauch, C., Pir\u00f3g, M.: Unifying guarded and unguarded iteration. In: Esparza, J., Murawski, A.S. (eds.) FoSSaCS 2017. LNCS, vol. 10203, pp. 517\u2013533. Springer, Heidelberg (2017). \n                      https:\/\/doi.org\/10.1007\/978-3-662-54458-7_30"},{"key":"11_CR20","doi-asserted-by":"crossref","unstructured":"Hancock, P., Setzer, A.: Guarded induction and weakly final coalgebras in dependent type theory. In: Crosilla, L., Schuster, P. (eds.) From Sets and Types to Topology and Analysis. Towards Practicable Foundations for Constructive Mathematics. Oxford Logic Guides, vol. 48, pp. 115\u2013134. Clarendon Press, Oxford (2005)","DOI":"10.1093\/acprof:oso\/9780198566519.003.0007"},{"issue":"1\u20133","key":"11_CR21","doi-asserted-by":"publisher","first-page":"70","DOI":"10.1016\/j.tcs.2006.03.013","volume":"357","author":"M Hyland","year":"2006","unstructured":"Hyland, M., Plotkin, G., Power, J.: Combining effects: sum and tensor. Theor. Comput. Sci. 357(1\u20133), 70\u201399 (2006). \n                      https:\/\/doi.org\/10.1016\/j.tcs.2006.03.013","journal-title":"Theor. Comput. Sci."},{"key":"11_CR22","unstructured":"Jones, S.P., et al.: Haskell 98: a non-strict, purely functional language (1999)"},{"key":"11_CR23","doi-asserted-by":"publisher","unstructured":"Krishnaswami, K., Benton, N.: Ultrametric semantics of reactive programs. In: Proceedings of 26th Annual IEEE Symposium on Logic in Computer Science. LICS 2011, June 2011, Toronto, ON, pp. 257\u2013266. IEEE CS Press, Washington, DC (2011). \n                      https:\/\/doi.org\/10.1109\/lics.2011.38","DOI":"10.1109\/lics.2011.38"},{"issue":"2","key":"11_CR24","doi-asserted-by":"publisher","first-page":"182","DOI":"10.1016\/s0890-5401(03)00088-9","volume":"185","author":"PB Levy","year":"2003","unstructured":"Levy, P.B., Power, J., Thielecke, H.: Modelling environments in call-by-value programming languages. Inf. Comput. 185(2), 182\u2013210 (2003). \n                      https:\/\/doi.org\/10.1016\/s0890-5401(03)00088-9","journal-title":"Inf. Comput."},{"key":"11_CR25","series-title":"Graduate Texts in Mathematics","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4612-9839-7","volume-title":"Categories for the Working Mathematician","author":"S Mac Lane","year":"1971","unstructured":"Mac Lane, S.: Categories for the Working Mathematician. Graduate Texts in Mathematics, vol. 5. Springer, New York (1971). \n                      https:\/\/doi.org\/10.1007\/978-1-4612-9839-7"},{"issue":"1","key":"11_CR26","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/j.ic.2004.05.003","volume":"196","author":"S Milius","year":"2005","unstructured":"Milius, S.: Completely iterative algebras and completely iterative monads. Inf. Comput. 196(1), 1\u201341 (2005). \n                      https:\/\/doi.org\/10.1016\/j.ic.2004.05.003","journal-title":"Inf. Comput."},{"key":"11_CR27","volume-title":"Communication and Concurrency","author":"R Milner","year":"1989","unstructured":"Milner, R.: Communication and Concurrency. Prentice-Hall, Upper Saddle River (1989)"},{"key":"11_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"138","DOI":"10.1007\/BFb0013462","volume-title":"Category Theory and Computer Science","author":"E Moggi","year":"1991","unstructured":"Moggi, E.: A modular approach to denotational semantics. In: Pitt, D.H., Curien, P.-L., Abramsky, S., Pitts, A.M., Poign\u00e9, A., Rydeheard, D.E. (eds.) CTCS 1991. LNCS, vol. 530, pp. 138\u2013139. Springer, Heidelberg (1991). \n                      https:\/\/doi.org\/10.1007\/BFb0013462"},{"key":"11_CR29","doi-asserted-by":"publisher","unstructured":"Nakano, H.: A modality for recursion. In: Proceedings of 15th Annual IEEE Symposium on Logic in Computer Science. LICS 2000, June 2000, Santa Barbara, CA, pp. 255\u2013266. IEEE CS Press, Washington, DC (2000). \n                      https:\/\/doi.org\/10.1109\/lics.2000.855774","DOI":"10.1109\/lics.2000.855774"},{"key":"11_CR30","doi-asserted-by":"publisher","first-page":"226","DOI":"10.4204\/EPTCS.66.12","volume":"66","author":"Keiko Nakata","year":"2011","unstructured":"Nakata, K.: Resumption-based big-step and small-step interpreters for While with interactive I\/O. In: Danvy, O., Shan, C. (eds.) Proceedings of IFIP Working Conference on Domain-Specific Languages. DSL 2011, Electronic Proceedings in Theoretical Computer Science, September 2011, Bordeaux, vol. 66, pp. 226\u2013235. Open Publishing Association, Sydney (2011). \n                      https:\/\/doi.org\/10.4204\/eptcs.66.12","journal-title":"Electronic Proceedings in Theoretical Computer Science"},{"key":"11_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"488","DOI":"10.1007\/978-3-642-11957-6_26","volume-title":"Programming Languages and Systems","author":"K Nakata","year":"2010","unstructured":"Nakata, K., Uustalu, T.: A Hoare logic for the coinductive trace-based big-step semantics of While. In: Gordon, A.D. (ed.) ESOP 2010. LNCS, vol. 6012, pp. 488\u2013506. Springer, Heidelberg (2010). \n                      https:\/\/doi.org\/10.1007\/978-3-642-11957-6_26"},{"key":"11_CR32","doi-asserted-by":"publisher","first-page":"57","DOI":"10.4204\/EPTCS.32.5","volume":"32","author":"Keiko Nakata","year":"2010","unstructured":"Nakata, K., Uustalu, T.: Resumptions, weak bisimilarity and big-step semantics for While with interactive I\/O: an exercise in mixed induction-coinduction. In: Aceto, L., Sobocinski, P. (eds.) Proceedings of 7th Workshop on Structural Operational Semantics. SOS 2010, Electronic Proceedings in Theoretical Computer Science, August 2010, Paris. vol. 32, pp. 57\u201375. Open Publishing Association, Sydney (2010). \n                      https:\/\/doi.org\/10.4204\/eptcs.32.5","journal-title":"Electronic Proceedings in Theoretical Computer Science"},{"issue":"1","key":"11_CR33","doi-asserted-by":"publisher","first-page":"1","DOI":"10.2168\/lmcs-11(1:1)2015","volume":"11","author":"K Nakata","year":"2015","unstructured":"Nakata, K., Uustalu, T.: A Hoare logic for the coinductive trace-based big-step semantics of While. Log. Methods Comput. Sci. 11(1), 1 (2015). \n                      https:\/\/doi.org\/10.2168\/lmcs-11(1:1)2015","journal-title":"Log. Methods Comput. Sci."},{"key":"11_CR34","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/3-540-45315-6_1","volume-title":"Foundations of Software Science and Computation Structures","author":"G Plotkin","year":"2001","unstructured":"Plotkin, G., Power, J.: Adequacy for algebraic effects. In: Honsell, F., Miculan, M. (eds.) FoSSaCS 2001. LNCS, vol. 2030, pp. 1\u201324. Springer, Heidelberg (2001). \n                      https:\/\/doi.org\/10.1007\/3-540-45315-6_1"},{"issue":"2","key":"11_CR35","doi-asserted-by":"publisher","first-page":"198","DOI":"10.2307\/2271658","volume":"32","author":"WW Tait","year":"1967","unstructured":"Tait, W.W.: Intensional interpretations of functionals of finite type I. J. Symb. Log. 32(2), 198\u2013212 (1967). \n                      https:\/\/doi.org\/10.2307\/2271658","journal-title":"J. Symb. Log."},{"key":"11_CR36","doi-asserted-by":"publisher","unstructured":"Turi, D., Plotkin, G.: Towards a mathematical operational semantics. In: Proceedings of 12th Annual IEEE Symposium on Logic in Computer Science. LICS 1997, June\u2013July 1997, Warsaw, pp. 280\u2013291. IEEE CS Press, Washington, DC (1997). \n                      https:\/\/doi.org\/10.1109\/lics.1997.614955","DOI":"10.1109\/lics.1997.614955"},{"key":"11_CR37","doi-asserted-by":"crossref","DOI":"10.7551\/mitpress\/3054.001.0001","volume-title":"The Formal Semantics of Programming Languages","author":"G Winskel","year":"1993","unstructured":"Winskel, G.: The Formal Semantics of Programming Languages. MIT Press, Cambridge (1993)"}],"container-title":["Lecture Notes in Computer Science","Theoretical Aspects of Computing \u2013 ICTAC 2018"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-02508-3_11","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,3,3]],"date-time":"2020-03-03T02:49:39Z","timestamp":1583203779000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-02508-3_11"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018]]},"ISBN":["9783030025076","9783030025083"],"references-count":37,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-02508-3_11","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2018]]},"assertion":[{"value":"15 October 2018","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"ICTAC","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Colloquium on Theoretical Aspects of Computing","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Stellenbosch","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"South Africa","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2018","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"16 October 2018","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"19 October 2018","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"15","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"ictac2018","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/www.ictac.org.za\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}