{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,27]],"date-time":"2026-02-27T03:47:27Z","timestamp":1772164047301,"version":"3.50.1"},"publisher-location":"New York, NY, USA","reference-count":40,"publisher":"ACM","license":[{"start":{"date-parts":[[2013,1,23]],"date-time":"2013-01-23T00:00:00Z","timestamp":1358899200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2013,1,23]]},"DOI":"10.1145\/2429069.2429075","type":"proceedings-article","created":{"date-parts":[[2013,1,22]],"date-time":"2013-01-22T10:29:29Z","timestamp":1358850569000},"page":"27-38","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":62,"title":["Copatterns"],"prefix":"10.1145","author":[{"given":"Andreas","family":"Abel","sequence":"first","affiliation":[{"name":"Ludwig-Maximilians-University, Munich, Germany"}]},{"given":"Brigitte","family":"Pientka","sequence":"additional","affiliation":[{"name":"McGill University, Montreal, PQ, Canada"}]},{"given":"David","family":"Thibodeau","sequence":"additional","affiliation":[{"name":"McGill University, Montreal, PQ, Canada"}]},{"given":"Anton","family":"Setzer","sequence":"additional","affiliation":[{"name":"Swansea University, Swansea, Wales Uk"}]}],"member":"320","published-online":{"date-parts":[[2013,1,23]]},"reference":[{"key":"e_1_3_2_2_1_1","series-title":"Lect","doi-asserted-by":"crossref","first-page":"296","DOI":"10.1007\/3-540-57887-0_101","volume-title":"Theoretical Aspects of Computer Software","author":"Abadi M.","year":"1994","unstructured":"M. Abadi and L. Cardelli . A theory of primitive objects. Untyped and first-order systems . In M. Hagiya and J. Mitchell, editors, Theoretical Aspects of Computer Software , volume 789 of Lect . Notes in Comput. Sci., pages 296 -- 320 . Springer , 1994 . M. Abadi and L. Cardelli. A theory of primitive objects. Untyped and first-order systems. In M. Hagiya and J. Mitchell, editors, Theoretical Aspects of Computer Software, volume 789 of Lect. Notes in Comput. Sci., pages 296--320. Springer, 1994."},{"key":"e_1_3_2_2_2_1","series-title":"Lect","doi-asserted-by":"crossref","first-page":"286","DOI":"10.1007\/978-3-540-76637-7_19","volume-title":"Proc. of the 5th Asian Symp. on Programming Languages and Systems, APLAS","author":"Abel A.","year":"2007","unstructured":"A. Abel . Mixed inductive\/coinductive types and strong normalization . In Z. Shao, editor, Proc. of the 5th Asian Symp. on Programming Languages and Systems, APLAS 2007 , volume 4807 of Lect . Notes in Comput. Sci., pages 286 -- 301 . Springer , 2007. ISBN 978--3--540--76636-0. A. Abel. Mixed inductive\/coinductive types and strong normalization. In Z. Shao, editor, Proc. of the 5th Asian Symp. on Programming Languages and Systems, APLAS 2007, volume 4807 of Lect. Notes in Comput. Sci., pages 286--301. Springer, 2007. ISBN 978--3--540--76636-0."},{"key":"e_1_3_2_2_3_1","doi-asserted-by":"publisher","DOI":"10.4204\/EPTCS.77.1"},{"key":"e_1_3_2_2_4_1","volume-title":"The Agda Wiki","author":"Agda","year":"2012","unstructured":"Agda team. The Agda Wiki , 2012 . Agda team. The Agda Wiki, 2012."},{"key":"e_1_3_2_2_5_1","volume-title":"Workshop on Partiality and Recursion in Interactive Theorem Provers, FLoC 2010","author":"Altenkirch T.","year":"2010","unstructured":"T. Altenkirch and N. A. Danielsson . Termination checking in the presence of nested inductive and coinductive types. Short note supporting a talk given at PAR 2010 , Workshop on Partiality and Recursion in Interactive Theorem Provers, FLoC 2010 , 2010 . T. Altenkirch and N. A. Danielsson. Termination checking in the presence of nested inductive and coinductive types. Short note supporting a talk given at PAR 2010, Workshop on Partiality and Recursion in Interactive Theorem Provers, FLoC 2010, 2010."},{"key":"e_1_3_2_2_6_1","doi-asserted-by":"publisher","DOI":"10.1093\/logcom\/2.3.297"},{"key":"e_1_3_2_2_7_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129503004122"},{"key":"e_1_3_2_2_8_1","series-title":"phLect","doi-asserted-by":"crossref","first-page":"75","DOI":"10.1007\/BFb0037099","volume-title":"Proc. of the 1st Int. Conf. on Typed Lambda Calculi and Applications, TLCA'93","author":"Benton N.","year":"1993","unstructured":"N. Benton , G. M. Bierman , V. de Paiva , and M. Hyland . A term calculus for intuitionistic linear logic . In M. Bezem and J. F. Groote, editors, Proc. of the 1st Int. Conf. on Typed Lambda Calculi and Applications, TLCA'93 , volume 664 of phLect . Notes in Comput. Sci., pages 75 -- 90 . Springer , 1993 . ISBN 3--540--56517--5. N. Benton, G. M. Bierman, V. de Paiva, and M. Hyland. A term calculus for intuitionistic linear logic. In M. Bezem and J. F. Groote, editors, Proc. of the 1st Int. Conf. on Typed Lambda Calculi and Applications, TLCA'93, volume 664 of phLect. Notes in Comput. Sci., pages 75--90. Springer, 1993. ISBN 3--540--56517--5."},{"key":"e_1_3_2_2_9_1","volume-title":"Certified Programming with Dependent Types","author":"Chlipala A.","year":"2012","unstructured":"A. Chlipala . Certified Programming with Dependent Types . MIT Press , June 2012 . Unpublished draft. A. Chlipala. Certified Programming with Dependent Types. MIT Press, June 2012. Unpublished draft."},{"key":"e_1_3_2_2_10_1","volume-title":"Department of Computer Science","author":"Cockett R.","year":"1992","unstructured":"R. Cockett and T. Fukushima . About charity. Technical report , Department of Computer Science , The University of Calgary , June 1992 . Yellow Series Report No. 92\/480\/18. R. Cockett and T. Fukushima. About charity. Technical report, Department of Computer Science, The University of Calgary, June 1992. Yellow Series Report No. 92\/480\/18."},{"key":"e_1_3_2_2_11_1","first-page":"71","volume-title":"B\u00e5stad","author":"Coquand T.","year":"1992","unstructured":"T. Coquand . Pattern matching with dependent types. In B. Nordstr\u00f6m, K. Pettersson, and G. Plotkin, editors, Types for Proofs and Programs (TYPES'92) , B\u00e5stad , Sweden , pages 71 -- 83 , 1992 . T. Coquand. Pattern matching with dependent types. In B. Nordstr\u00f6m, K. Pettersson, and G. Plotkin, editors, Types for Proofs and Programs (TYPES'92), B\u00e5stad, Sweden, pages 71--83, 1992."},{"key":"e_1_3_2_2_12_1","series-title":"phLect","first-page":"62","volume-title":"Types for Proofs and Programs (TYPES'93)","author":"Coquand T.","year":"1993","unstructured":"T. Coquand . Infinite objects in type theory . In H. Barendregt and T. Nipkow, editors, Types for Proofs and Programs (TYPES'93) , volume 806 of phLect . Notes in Comput. Sci., pages 62 -- 78 . Springer , 1993 . T. Coquand. Infinite objects in type theory. In H. Barendregt and T. Nipkow, editors, Types for Proofs and Programs (TYPES'93), volume 806 of phLect. Notes in Comput. Sci., pages 62--78. Springer, 1993."},{"key":"e_1_3_2_2_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/351240.351262"},{"key":"e_1_3_2_2_14_1","series-title":"phLect","doi-asserted-by":"crossref","first-page":"100","DOI":"10.1007\/978-3-642-13321-3_8","volume-title":"Proc. of the 10th Int. Conf. on Mathematics of Program Construction, MPC","author":"Danielsson N. A.","year":"2010","unstructured":"N. A. Danielsson and T. Altenkirch . Subtyping, declaratively . In C. Bolduc, J. Desharnais, and B. Ktari, editors, Proc. of the 10th Int. Conf. on Mathematics of Program Construction, MPC 2010 , volume 6120 of phLect . Notes in Comput. Sci., pages 100 -- 118 . Springer , 2010. ISBN 978--3--642--13320--6. N. A. Danielsson and T. Altenkirch. Subtyping, declaratively. In C. Bolduc, J. Desharnais, and B. Ktari, editors, Proc. of the 10th Int. Conf. on Mathematics of Program Construction, MPC 2010, volume 6120 of phLect. Notes in Comput. Sci., pages 100--118. Springer, 2010. ISBN 978--3--642--13320--6."},{"key":"e_1_3_2_2_15_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2008.12.117"},{"key":"e_1_3_2_2_16_1","volume-title":"Ecole Normale Sup\u00e9rieure de Lyon","author":"Gim\u00e9nez E.","year":"1996","unstructured":"E. Gim\u00e9nez . phUn Calcul de Constructions Infinies et son application a la v\u00e9rification de syst\u00e8mes communicants. PhD thesis , Ecole Normale Sup\u00e9rieure de Lyon , Dec. 1996 . Th\u00e8se d'universit\u00e9. E. Gim\u00e9nez. phUn Calcul de Constructions Infinies et son application a la v\u00e9rification de syst\u00e8mes communicants. PhD thesis, Ecole Normale Sup\u00e9rieure de Lyon, Dec. 1996. Th\u00e8se d'universit\u00e9."},{"key":"e_1_3_2_2_17_1","series-title":"phLect","first-page":"521","volume-title":"K. Futatsugi, J.-P","author":"Goguen H.","year":"2006","unstructured":"H. Goguen , C. McBride , and J. McKinna . Eliminating dependent pattern matching . In K. Futatsugi, J.-P . Jouannaud, and J. Meseguer, editors, Algebra, Meaning , and Computation, Essays Dedicated to Joseph A. Goguen on the Occasion of His 65th Birthday, volume 4060 of phLect . Notes in Comput. Sci., pages 521 -- 540 . Springer , 2006 . ISBN 3--540--35462-X. H. Goguen, C. McBride, and J. McKinna. Eliminating dependent pattern matching. In K. Futatsugi, J.-P. Jouannaud, and J. Meseguer, editors, Algebra, Meaning, and Computation, Essays Dedicated to Joseph A. Goguen on the Occasion of His 65th Birthday, volume 4060 of phLect. Notes in Comput. Sci., pages 521--540. Springer, 2006. ISBN 3--540--35462-X."},{"key":"e_1_3_2_2_19_1","series-title":"phLect","doi-asserted-by":"crossref","first-page":"140","DOI":"10.1007\/3-540-18508-9_24","volume-title":"Category Theory and Computer Science","author":"Hagino T.","year":"1987","unstructured":"T. Hagino . A typed lambda calculus with categorical type constructors . In D. H. Pitt, A. Poign\u00e9, and D. E. Rydeheard, editors, Category Theory and Computer Science , volume 283 of phLect . Notes in Comput. Sci., pages 140 -- 157 . Springer , 1987 . T. Hagino. A typed lambda calculus with categorical type constructors. In D. H. Pitt, A. Poign\u00e9, and D. E. Rydeheard, editors, Category Theory and Computer Science, volume 283 of phLect. Notes in Comput. Sci., pages 140--157. Springer, 1987."},{"key":"e_1_3_2_2_20_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0747-7171(89)80065-3"},{"key":"e_1_3_2_2_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/237721.240882"},{"key":"e_1_3_2_2_22_1","volume-title":"The Coq Proof Assistant Reference Manual. INRIA, version 8.3 edition","author":"INRIA.","year":"2010","unstructured":"INRIA. The Coq Proof Assistant Reference Manual. INRIA, version 8.3 edition , 2010 . INRIA. The Coq Proof Assistant Reference Manual. INRIA, version 8.3 edition, 2010."},{"key":"e_1_3_2_2_23_1","unstructured":"J.\n      Kennaway\n     and \n      F.\n      de Vries\n    . \n      Infinitary\n      Rewriting volume \n  55\n   of \n  phCambridge Tracts in Theoretical Computer Science chapter Chapter 12 in Term Rewriting Systems pages \n  668\n  --\n  711\n  . \n  Cambridge University Press 2003\n  .  J. Kennaway and F. de Vries. Infinitary Rewriting volume 55 of phCambridge Tracts in Theoretical Computer Science chapter Chapter 12 in Term Rewriting Systems pages 668--711. Cambridge University Press 2003."},{"key":"e_1_3_2_2_24_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-02348-4_16"},{"key":"e_1_3_2_2_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/1480881.1480927"},{"key":"e_1_3_2_2_26_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2008.48"},{"key":"e_1_3_2_2_27_1","unstructured":"C.\n      McBride\n    .\n  Let's see how things unfold: Reconciling the infinite with the intensional\n  . In A. Kurz M. Lenisa and A. Tarlecki editors 3rd Int. Conf. on Algebra and Coalgebra in Computer Science CALCO \n  2009 volume \n  5728\n   of \n  phLect\n  . Notes in Comput. Sci. pages \n  113\n  --\n  126\n  . \n  Springer 2009. ISBN 978--3--642-03740--5.   C. McBride. Let's see how things unfold: Reconciling the infinite with the intensional. In A. Kurz M. Lenisa and A. Tarlecki editors 3rd Int. Conf. on Algebra and Coalgebra in Computer Science CALCO 2009 volume 5728 of phLect. Notes in Comput. Sci. pages 113--126. Springer 2009. ISBN 978--3--642-03740--5."},{"key":"e_1_3_2_2_28_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796803004829"},{"key":"e_1_3_2_2_29_1","doi-asserted-by":"publisher","DOI":"10.1016\/0022-0000(78)90014-4"},{"key":"e_1_3_2_2_31_1","volume-title":"June","author":"Oury N.","year":"2008","unstructured":"N. Oury . Coinductive types and type preservation. Message on the coq-club mailing list , June 2008 . N. Oury. Coinductive types and type preservation. Message on the coq-club mailing list, June 2008."},{"key":"e_1_3_2_2_32_1","doi-asserted-by":"publisher","DOI":"10.2307\/2275652"},{"key":"e_1_3_2_2_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/268946.268967"},{"key":"e_1_3_2_2_34_1","series-title":"Lect","doi-asserted-by":"crossref","first-page":"120","DOI":"10.1007\/10930755_8","volume-title":"Proceedings of the 16th International Conference on Theorem Proving in Higher Order Logics (TPHOLs","author":"Sch\u00fcrmann C.","year":"2003","unstructured":"C. Sch\u00fcrmann and F. Pfenning . A coverage checking algorithm for LF . In D. Basin and B. Wolff, editors, Proceedings of the 16th International Conference on Theorem Proving in Higher Order Logics (TPHOLs 2003 ), volume 2758 of Lect . Notes in Comput. Sci., pages 120 -- 135 , Rome, Italy, September 2003. Springer . C. Sch\u00fcrmann and F. Pfenning. A coverage checking algorithm for LF. In D. Basin and B. Wolff, editors, Proceedings of the 16th International Conference on Theorem Proving in Higher Order Logics (TPHOLs 2003), volume 2758 of Lect. Notes in Comput. Sci., pages 120--135, Rome, Italy, September 2003. Springer."},{"key":"e_1_3_2_2_35_1","volume-title":"Epistemology versus ontology: Essays on the foundations of mathematics in honour of Per Martin-L\u00f6f","author":"Setzer A.","year":"2012","unstructured":"A. Setzer . Coalgebras as types determined by their elimination rules . In P. Dybjer, S. Lindstr\u00f6m, E. Palmgren, and G. Sundholm, editors, Epistemology versus ontology: Essays on the foundations of mathematics in honour of Per Martin-L\u00f6f . Springer , 2012 . To appear. A. Setzer. Coalgebras as types determined by their elimination rules. In P. Dybjer, S. Lindstr\u00f6m, E. Palmgren, and G. Sundholm, editors, Epistemology versus ontology: Essays on the foundations of mathematics in honour of Per Martin-L\u00f6f. Springer, 2012. To appear."},{"key":"e_1_3_2_2_36_1","volume-title":"Pattern matching in Charity. Master's thesis","author":"Tuckey C.","year":"1997","unstructured":"C. Tuckey . Pattern matching in Charity. Master's thesis , The University of Calgary , July 1997 . C. Tuckey. Pattern matching in Charity. Master's thesis, The University of Calgary, July 1997."},{"key":"e_1_3_2_2_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/964001.964006"},{"key":"e_1_3_2_2_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/944705.944723"},{"key":"e_1_3_2_2_39_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-32033-3_15"},{"key":"e_1_3_2_2_40_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1994.1093"},{"key":"e_1_3_2_2_41_1","doi-asserted-by":"publisher","DOI":"10.1145\/1328438.1328482"},{"key":"e_1_3_2_2_42_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.apal.2008.01.001"}],"event":{"name":"POPL '13: The 40th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages","location":"Rome Italy","acronym":"POPL '13","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages","SIGACT ACM Special Interest Group on Algorithms and Computation Theory"]},"container-title":["Proceedings of the 40th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2429069.2429075","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2429069.2429075","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T04:35:35Z","timestamp":1750221335000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2429069.2429075"}},"subtitle":["programming infinite structures by observations"],"short-title":[],"issued":{"date-parts":[[2013,1,23]]},"references-count":40,"alternative-id":["10.1145\/2429069.2429075","10.1145\/2429069"],"URL":"https:\/\/doi.org\/10.1145\/2429069.2429075","relation":{"is-identical-to":[{"id-type":"doi","id":"10.1145\/2480359.2429075","asserted-by":"object"}]},"subject":[],"published":{"date-parts":[[2013,1,23]]},"assertion":[{"value":"2013-01-23","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}