{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,28]],"date-time":"2025-11-28T21:09:10Z","timestamp":1764364150842},"publisher-location":"Cham","reference-count":13,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319089171"},{"type":"electronic","value":"9783319089188"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2014]]},"DOI":"10.1007\/978-3-319-08918-8_3","type":"book-chapter","created":{"date-parts":[[2014,7,2]],"date-time":"2014-07-02T05:44:22Z","timestamp":1404279862000},"page":"31-45","source":"Crossref","is-referenced-by-count":9,"title":["Unnesting of Copatterns"],"prefix":"10.1007","author":[{"given":"Anton","family":"Setzer","sequence":"first","affiliation":[]},{"given":"Andreas","family":"Abel","sequence":"additional","affiliation":[]},{"given":"Brigitte","family":"Pientka","sequence":"additional","affiliation":[]},{"given":"David","family":"Thibodeau","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"3_CR1","unstructured":"Abel, A.: A Polymorphic Lambda-Calculus with Sized Higher-Order Types. PhD thesis, Ludwig-Maximilians-Universit\u00e4t M\u00fcnchen (2006)"},{"key":"3_CR2","doi-asserted-by":"crossref","unstructured":"Abel, A., Pientka, B., Thibodeau, D., Setzer, A.: Copatterns: Programming infinite structures by observations. In: Proc. of the 40th ACM Symp. on Principles of Programming Languages, POPL 2013, pp. 27\u201338. ACM Press (2013)","DOI":"10.1145\/2480359.2429075"},{"key":"3_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"368","DOI":"10.1007\/3-540-15975-4_48","volume-title":"Functional Programming Languages and Computer Architecture (FPCA 1985)","author":"L. Augustsson","year":"1985","unstructured":"Augustsson, L.: Compiling pattern matching. In: Jouannaud, J.-P. (ed.) FPCA 1985. LNCS, vol.\u00a0201, pp. 368\u2013381. Springer, Heidelberg (1985)"},{"issue":"1","key":"3_CR4","doi-asserted-by":"publisher","first-page":"97","DOI":"10.1017\/S0960129503004122","volume":"14","author":"G. Barthe","year":"2004","unstructured":"Barthe, G., Frade, M.J., Gim\u00e9nez, E., Pinto, L., Uustalu, T.: Type-based termination of recursive definitions. Math. Struct. in Comput. Sci.\u00a014(1), 97\u2013141 (2004)","journal-title":"Math. Struct. in Comput. Sci."},{"key":"3_CR5","doi-asserted-by":"crossref","unstructured":"Brady, E.: Idris, a general purpose dependently typed programming language: Design and implementation (2013), \n                  \n                    http:\/\/www.cs.st-andrews.ac.uk\/~eb\/drafts\/impldtp.pdf","DOI":"10.1017\/S095679681300018X"},{"key":"3_CR6","unstructured":"Cockett, R., Fukushima, T.: About Charity. Technical report, Department of Computer Science, The University of Calgary, Yellow Series Report No. 92\/480\/18 (June 1992)"},{"key":"3_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"140","DOI":"10.1007\/3-540-18508-9_24","volume-title":"Category Theory and Computer Science","author":"T. Hagino","year":"1987","unstructured":"Hagino, T.: A typed lambda calculus with categorical type constructors. In: Pitt, D.H., Rydeheard, D.E., Poign\u00e9, A. (eds.) Category Theory and Computer Science. LNCS, vol.\u00a0283, pp. 140\u2013157. Springer, Heidelberg (1987)"},{"issue":"6","key":"3_CR8","first-page":"629","volume":"8","author":"T. Hagino","year":"1989","unstructured":"Hagino, T.: Codatatypes in ML. J. Symb. Logic\u00a08(6), 629\u2013650 (1989)","journal-title":"J. Symb. Logic"},{"key":"3_CR9","unstructured":"INRIA. The Coq Proof Assistant Reference Manual. INRIA, version 8.4 edition (2012)"},{"key":"3_CR10","unstructured":"Norell, U.: Towards a Practical Programming Language Based on Dependent Type Theory. PhD thesis, Dept. of Computer Science and Engineering, Chalmers, G\u00f6teborg, Sweden (2007)"},{"key":"3_CR11","unstructured":"Severi, P.G.: Normalisation in lambda calculus and its relation to type inference. PhD thesis, Technische Universiteit Eindhoven, Eindhoven, The Netherlands (1996)"},{"key":"3_CR12","unstructured":"Terese. Term Rewriting Systems. Cambridge University Press (2003)"},{"key":"3_CR13","unstructured":"van Raamsdonk, F.: Concluence and Normalisation for Higher-Order Rewriting. PhD thesis, Vrije Universiteit, Amsterdam, The Netherlands (1996)"}],"container-title":["Lecture Notes in Computer Science","Rewriting and Typed Lambda Calculi"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-08918-8_3","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,27]],"date-time":"2019-05-27T05:28:20Z","timestamp":1558934900000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-08918-8_3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014]]},"ISBN":["9783319089171","9783319089188"],"references-count":13,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-08918-8_3","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2014]]}}}