{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,9,29]],"date-time":"2025-09-29T11:54:15Z","timestamp":1759146855957,"version":"3.40.3"},"publisher-location":"Cham","reference-count":47,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030003883"},{"type":"electronic","value":"9783030003890"}],"license":[{"start":{"date-parts":[[2018,1,1]],"date-time":"2018-01-01T00:00:00Z","timestamp":1514764800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2018,1,1]],"date-time":"2018-01-01T00:00:00Z","timestamp":1514764800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/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-00389-0_4","type":"book-chapter","created":{"date-parts":[[2018,9,19]],"date-time":"2018-09-19T19:12:43Z","timestamp":1537384363000},"page":"34-55","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Undecidability of Equality for Codata Types"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-7677-3582","authenticated-orcid":false,"given":"Ulrich","family":"Berger","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0001-5322-6060","authenticated-orcid":false,"given":"Anton","family":"Setzer","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2018,9,20]]},"reference":[{"key":"4_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"23","DOI":"10.1007\/3-540-36576-1_2","volume-title":"Foundations of Software Science and Computation Structures","author":"M Abbott","year":"2003","unstructured":"Abbott, M., Altenkirch, T., Ghani, N.: Categories of containers. In: Gordon, A.D. (ed.) FoSSaCS 2003. LNCS, vol. 2620, pp. 23\u201338. Springer, Heidelberg (2003). https:\/\/doi.org\/10.1007\/3-540-36576-1_2"},{"key":"4_CR2","unstructured":"Abel, A., Adelsberger, S., Setzer, A.: ooAgda. Agda Library (2016). https:\/\/github.com\/agda\/ooAgda"},{"key":"4_CR3","doi-asserted-by":"crossref","unstructured":"Abel, A., Adelsberger, S., Setzer, A.: Interactive programming in Agda - Objects and graphical user interfaces. J. Funct. Program. 27, January 2017. https:\/\/doi.org\/10.1017\/S0956796816000319","DOI":"10.1017\/S0956796816000319"},{"key":"4_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"40","DOI":"10.1007\/978-3-642-12251-4_5","volume-title":"Functional and Logic Programming","author":"T Altenkirch","year":"2010","unstructured":"Altenkirch, T., Danielsson, N.A., L\u00f6h, A., Oury, N.: \n$$\\varPi \\varSigma $$\n: dependent types without the sugar. In: Blume, M., Kobayashi, N., Vidal, G. (eds.) FLOPS 2010. LNCS, vol. 6009, pp. 40\u201355. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-12251-4_5"},{"key":"4_CR5","unstructured":"Agda Wiki: Coinductive data types, 1 January 2011. http:\/\/wiki.portal.chalmers.se\/agda\/pmwiki.php?n=ReferenceManual.Codatatypes"},{"key":"4_CR6","unstructured":"Agda team: The Agda Wiki (2014). http:\/\/wiki.portal.chalmers.se\/agda\/pmwiki.php"},{"key":"4_CR7","unstructured":"Altenkirch, T.: Codata. Talk given at the TYPES Workshop in Jouy-en-Josas, December 2004. http:\/\/www.cs.nott.ac.uk\/~txa\/talks\/types04.pdf"},{"key":"4_CR8","doi-asserted-by":"publisher","unstructured":"Abel, A., Pientka, B., Thibodeau, D., Setzer, A.: Copatterns: programming infinite structures by observations. In: Giacobazzi, R., Cousot, R., (eds.) Proceedings of POPL 2013, pp. 27\u201338. ACM, New York (2013). https:\/\/doi.org\/10.1145\/2429069.2429075","DOI":"10.1145\/2429069.2429075"},{"key":"4_CR9","doi-asserted-by":"crossref","unstructured":"Bertot, Y., Cast\u00e9ran, P.: Interactive theorem proving and program development. Coq\u2019Art: The Calculus of Inductive Constructions. Texts in Theoretical Computer Science. An EATCS Series. Springer (2004). ISBN 3-540-20854-2","DOI":"10.1007\/978-3-662-07964-5"},{"key":"4_CR10","unstructured":"Bertot, Y.: CoInduction in Coq, March 2006. arxiv:0603119"},{"key":"4_CR11","doi-asserted-by":"publisher","unstructured":"Basold, H., Geuvers, H.: Type theory based on dependent inductive and coinductive types. In: Proceedings of the 31st Annual ACM\/IEEE Symposium on Logic in Computer Science, LICS 2016, pp 327\u2013336. ACM, New York (2016). https:\/\/doi.org\/10.1145\/2933575.2934514","DOI":"10.1145\/2933575.2934514"},{"key":"4_CR12","unstructured":"Cockett, R., Fukushima, T.: About charity. Technical report, Department of Computer Science, The University of Calgary, June 1992. Yellow Series Report No. 92\/480\/18. ftp:\/\/ftp.cpsc.ucalgary.ca\/pub\/projects\/charity\/literature\/papers_and_reports\/about_charity.ps.gz"},{"key":"4_CR13","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). https:\/\/doi.org\/10.1007\/3-540-58085-9_72"},{"key":"4_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"100","DOI":"10.1007\/978-3-642-13321-3_8","volume-title":"Mathematics of Program Construction","author":"NA Danielsson","year":"2010","unstructured":"Danielsson, N.A., Altenkirch, T.: Subtyping, declaratively. In: Bolduc, C., Desharnais, J., Ktari, B. (eds.) MPC 2010. LNCS, vol. 6120, pp. 100\u2013118. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-13321-3_8"},{"key":"4_CR15","unstructured":"Danielsson, N.A.: Changes to coinduction, 17 March 2009. Message posted on gmane.comp.lang.agda. http:\/\/article.gmane.org\/gmane.comp.lang.agda\/763\/"},{"key":"4_CR16","doi-asserted-by":"publisher","first-page":"1041","DOI":"10.1016\/S0049-237X(98)80049-9","volume-title":"Studies in Logic and the Foundations of Mathematics","author":"W. Gasarch","year":"1998","unstructured":"Gasarch, W.: Chapter 16: A survey of recursive combinatorics. In: Ershov, Yu.L., Goncharov, S.S., Nerode, A., Remmel, J.B., Marek, V.W. (eds.) Handbook of Recursive Mathematics - Volume 2: Recursive Algebra, Analysis and Combinatorics, vol. 139, pp. 1041\u20131176. Elsevier (1998). https:\/\/doi.org\/10.1016\/S0049-237X(98)80049-9"},{"key":"4_CR17","unstructured":"Geuvers, H.: Inductive and coinductive types with iteration and recursion. In: Nordstr\u00f6m, B., Petersson, K., Plotkin, G. (eds.) Informal Proceedings of the 1992 Workshop on Types for Proofs and Programs, Bastad 1992, Sweden, pp. 183\u2013207 (1992). http:\/\/www.lfcs.inf.ed.ac.uk\/research\/types-bra\/proc\/proc92.ps.gz"},{"key":"4_CR18","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). https:\/\/doi.org\/10.1007\/3-540-60579-7_3"},{"key":"4_CR19","unstructured":"Gim\u00e9nez, C.E.: Un calcul de constructions infinies et son application \u00e0 la v\u00e9rification de syst\u00e8mes communicants. (English: A calculus of infinite constructions and its application to the verification of communicating systems). Ph.D. thesis, Ecole normale sup\u00e9rieure de Lyon, Lyon, France (1996). http:\/\/citeseerx.ist.psu.edu\/viewdoc\/summary?doi=10.1.1.16.9849&rank=1"},{"key":"4_CR20","unstructured":"Granstr\u00f6m, J.G.: Reference and Computation in Intuitionistic Type Theory. Ph.D. thesis, Department of Mathematics, Uppsala University, Sweden (2008). http:\/\/intuitionistic.files.wordpress.com\/2010\/07\/theses_published_uppsala.pdf"},{"key":"4_CR21","unstructured":"Greiner, J.: Programming with inductive and co-inductive types. Technical report CMU-CS-92-109, ADA249562, Dept. of Computer Science, Carnegie-Mellon University Pittburgh, Pittburgh, PA, USA, January 27 1992. 37 p. http:\/\/www.dtic.mil\/docs\/citations\/ADA249562"},{"key":"4_CR22","unstructured":"Hagino, T.: A Categorical Programming Language. Ph.D. thesis, Laboratory for Foundations of Computer Science, University of Edinburgh (1987). http:\/\/www.tom.sfc.keio.ac.jp\/~hagino\/thesis.pdf"},{"issue":"6","key":"4_CR23","doi-asserted-by":"publisher","first-page":"629","DOI":"10.1016\/S0747-7171(89)80065-3","volume":"8","author":"T Hagino","year":"1989","unstructured":"Hagino, T.: Codatatypes in ML. J. Symb. Comput. 8(6), 629\u2013650 (1989). https:\/\/doi.org\/10.1016\/S0747-7171(89)80065-3","journal-title":"J. Symb. Comput."},{"key":"4_CR24","doi-asserted-by":"publisher","unstructured":"Howard, B.T.: Inductive, coinductive, and pointed types. In: Proceedings of the First ACM SIGPLAN International Conference on Functional Programming, ICFP 1996, pp. 102\u2013109. ACM, New York (1996). https:\/\/doi.org\/10.1145\/232627.232640","DOI":"10.1145\/232627.232640"},{"key":"4_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"317","DOI":"10.1007\/3-540-44622-2_21","volume-title":"Computer Science Logic","author":"P Hancock","year":"2000","unstructured":"Hancock, P., Setzer, A.: Interactive programs in dependent type theory. In: Clote, P.G., Schwichtenberg, H. (eds.) CSL 2000. LNCS, vol. 1862, pp. 317\u2013331. Springer, Heidelberg (2000). https:\/\/doi.org\/10.1007\/3-540-44622-2_21"},{"key":"4_CR26","unstructured":"Hancock, P., Setzer, A.: Interactive programs and weakly final coalgebras (extended version). In: Altenkirch, T., Hofmann, M., Hughes, J. (eds.) Dependently typed programming, number 04381 in Dagstuhl Seminar Proceedings. Internationales Begegnungs- und Forschungszentrum (IBFI), Schloss Dagstuhl, Germany (2004). http:\/\/drops.dagstuhl.de\/opus\/"},{"key":"4_CR27","doi-asserted-by":"publisher","first-page":"115","DOI":"10.1093\/acprof:oso\/9780198566519.003.0007","volume-title":"From Sets and Types to Topology and Analysis","author":"Peter Hancock","year":"2005","unstructured":"Hancock, P., Setzer, A.: Interactive programs 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, pp. 115\u2013134. Oxford. Clarendon Press (2005). https:\/\/doi.org\/10.1093\/acprof:oso\/9780198566519.003.0007"},{"key":"4_CR28","unstructured":"INRIA. The Coq Proof Assistant Reference Manual. INRIA, version 8.7.1 edition (2017). https:\/\/coq.inria.fr\/refman\/"},{"key":"4_CR29","doi-asserted-by":"publisher","unstructured":"Igried, B., Setzer, A.: Programming with monadic CSP-style processes in dependent type theory. In: Proceedings of the 1st International Workshop on Type-Driven Development, TyDe 2016, pp. 28\u201338. ACM, New York (2016). https:\/\/doi.org\/10.1145\/2976022.2976032","DOI":"10.1145\/2976022.2976032"},{"key":"4_CR30","doi-asserted-by":"publisher","first-page":"36","DOI":"10.4204\/EPTCS.258.3","volume":"258","author":"Bashar Igried","year":"2017","unstructured":"Igried, B., Setzer, A.: Trace and stable failures semantics for CSP-Agda. In: Komendantskaya, E., Power, J. (eds.) Proceedings of the First Workshop on Coalgebra, Horn Clause Logic Programming and Types. Electronic Proceedings in Theoretical Computer Science, vol. 258, Edinburgh, UK, 28\u201329 November 2016, pp. 36\u201351. Open Publishing Association (2017). https:\/\/doi.org\/10.4204\/EPTCS.258.3","journal-title":"Electronic Proceedings in Theoretical Computer Science"},{"key":"4_CR31","unstructured":"Igried, B., Setzer, A.: Defining trace semantics for CSP-Agda, 30 Jan 2018. Accepted for publication in Postproceedings TYPES 2016, 23 pp. http:\/\/www.cs.swan.ac.uk\/~csetzer\/articles\/types2016PostProceedings\/igriedSetzerTypes2016Postproceedings.pdf"},{"key":"4_CR32","unstructured":"Jacobs, B., Rutten, J.: A tutorial on (co)algebras and (co)induction. EATCS Bull. 62, 62\u2013222 (1997). http:\/\/www.cs.ru.nl\/B.Jacobs\/PAPERS\/JR.pdf"},{"key":"4_CR33","doi-asserted-by":"publisher","first-page":"244","DOI":"10.2307\/2266709","volume":"12","author":"SC Kleene","year":"1950","unstructured":"Kleene, S.C.: A symmetric form of G\u00f6del\u2019s theorem. Ind. Math. 12, 244\u2013246 (1950). https:\/\/doi.org\/10.2307\/2266709","journal-title":"Ind. Math."},{"key":"4_CR34","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"113","DOI":"10.1007\/978-3-642-03741-2_9","volume-title":"Algebra and Coalgebra in Computer Science","author":"C McBride","year":"2009","unstructured":"McBride, C.: Let\u2019s see how things unfold: reconciling the infinite with the intensional (extended abstract). In: Kurz, A., Lenisa, M., Tarlecki, A. (eds.) CALCO 2009. LNCS, vol. 5728, pp. 113\u2013126. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-03741-2_9"},{"key":"4_CR35","unstructured":"Mendler, N.P.: Recursive types and type constraints in second-order lambda calculus. In: Gries, D. (eds.) Proceedings of the Second Annual IEEE Symposium on Logic in Computer Science, LICS 1987, pp. 30\u201336. IEEE Computer Society Press, June 1987"},{"issue":"1\u20132","key":"4_CR36","doi-asserted-by":"publisher","first-page":"159","DOI":"10.1016\/0168-0072(91)90069-X","volume":"51","author":"NP Mendler","year":"1991","unstructured":"Mendler, N.P.: Inductive types and type constraints in the second-order lambda calculus. Ann. Pure Appl. Logic 51(1\u20132), 159\u2013172 (1991). https:\/\/doi.org\/10.1016\/0168-0072(91)90069-X","journal-title":"Ann. Pure Appl. Logic"},{"key":"4_CR37","unstructured":"Norell, U.: Towards a practical programming language based on dependent type theory. Ph.D. thesis, Department of Computer Science and Engineering, Chalmers University of Technology, G\u00f6teborg, Sweden, September 2007. http:\/\/www.cse.chalmers.se\/~ulfn\/papers\/thesis.pdf"},{"key":"4_CR38","doi-asserted-by":"publisher","unstructured":"Odifreddi, P.: Classical Recursion Theory, vol. 125. Elsevier (1992). https:\/\/doi.org\/10.1016\/S0049-237X(08)70011-9","DOI":"10.1016\/S0049-237X(08)70011-9"},{"key":"4_CR39","unstructured":"Oury, N.: Coinductive types and type preservation. Email posted 6 June 2008 at science.mathematics.logic.coq.club. (2008).https:\/\/sympa-roc.inria.fr\/wws\/arc\/coq-club\/2008-06\/msg00022.html?checked_cas=2"},{"issue":"03","key":"4_CR40","doi-asserted-by":"publisher","first-page":"87","DOI":"10.2307\/2269028","volume":"1","author":"Barkley Rosser","year":"1936","unstructured":"Rosser, B.: Extensions of some theorems of G\u00f6del and church. J. Symb. Logic 1(3), 87\u201391 (1936). http:\/\/www.jstor.org\/stable\/2269028","journal-title":"The Journal of Symbolic Logic"},{"issue":"1","key":"4_CR41","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1016\/S0304-3975(00)00056-6","volume":"249","author":"J Rutten","year":"2000","unstructured":"Rutten, J.: Universal coalgebra: a theory of systems. Theor. Comput. Sci. 249(1), 3\u201380 (2000). https:\/\/doi.org\/10.1016\/S0304-3975(00)00056-6","journal-title":"Theor. Comput. Sci."},{"key":"4_CR42","doi-asserted-by":"publisher","first-page":"351","DOI":"10.1007\/978-94-007-4435-6_16","volume-title":"Epistemology versus Ontology","author":"Anton Setzer","year":"2012","unstructured":"Setzer, A.: Coalgebras as types determined by their elimination rules. In: Dybjer, P., Lindstr\u00f6m, S., Palmgren, E., Sundholm, G. (eds.) Epistemology versus Ontology. Logic, Epistemology, and the Unity of Science, vol. 27, pp. 351\u2013369. Springer (2012). https:\/\/doi.org\/10.1007\/978-94-007-4435-6_16"},{"key":"4_CR43","series-title":"Progress in Computer Science and Applied Logic","doi-asserted-by":"publisher","first-page":"377","DOI":"10.1007\/978-3-319-29198-7_12","volume-title":"Advances in Proof Theory","author":"A Setzer","year":"2016","unstructured":"Setzer, A.: How to reason coinductively informally. In: Kahle, R., Strahm, T., Studer, T. (eds.) Advances in Proof Theory. PCSAL, vol. 28, pp. 377\u2013408. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-29198-7_12"},{"key":"4_CR44","first-page":"953","volume":"88","author":"BA Trakhtenbrot","year":"1953","unstructured":"Trakhtenbrot, B.A.: On recursive separability. Dokl. Acad. Nauk 88, 953\u2013956 (1953)","journal-title":"Dokl. Acad. Nauk"},{"key":"4_CR45","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/3-540-60675-0_35","volume-title":"Funtional Programming Languages in Education","author":"DA Turner","year":"1995","unstructured":"Turner, D.A.: Elementary strong functional programming. In: Hartel, P.H., Plasmeijer, R. (eds.) FPLE 1995. LNCS, vol. 1022, pp. 1\u201313. Springer, Heidelberg (1995). https:\/\/doi.org\/10.1007\/3-540-60675-0_35"},{"key":"4_CR46","unstructured":"Turner, D.A.: Total functional programming. J. Univ. Comput. Sci. 10(7), 751\u2013768 (2004). http:\/\/www.jucs.org\/jucs_10_7\/total_functional_programming"},{"key":"4_CR47","unstructured":"Vene, V., Uustalu, T.: Functional programming with apomorphisms (corecursion). Proc. Estonian Acad. Sci. Phys. Math. 47(3), 147\u2013161 (1998). http:\/\/cs.ioc.ee\/~tarmo\/papers\/nwpt97-peas.pdf"}],"container-title":["Lecture Notes in Computer Science","Coalgebraic Methods in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-00389-0_4","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,9,19]],"date-time":"2022-09-19T00:03:33Z","timestamp":1663545813000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-030-00389-0_4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018]]},"ISBN":["9783030003883","9783030003890"],"references-count":47,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-00389-0_4","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":"20 September 2018","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"CMCS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Workshop on Coalgebraic Methods in Computer Science","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Thessaloniki","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Greece","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":"14 April 2018","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"15 April 2018","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"14","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"cmcs2018","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/www.coalg.org\/cmcs18\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"This content has been made available to all.","name":"free","label":"Free to read"}]}}