{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T00:22:48Z","timestamp":1725495768079},"publisher-location":"Berlin, Heidelberg","reference-count":17,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540766360"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/978-3-540-76637-7_19","type":"book-chapter","created":{"date-parts":[[2007,11,20]],"date-time":"2007-11-20T07:47:52Z","timestamp":1195544872000},"page":"286-301","source":"Crossref","is-referenced-by-count":9,"title":["Mixed Inductive\/Coinductive Types and Strong Normalization"],"prefix":"10.1007","author":[{"given":"Andreas","family":"Abel","sequence":"first","affiliation":[]}],"member":"297","reference":[{"key":"19_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"381","DOI":"10.1007\/11753728_39","volume-title":"Computer Science \u2013 Theory and Applications","author":"A. Abel","year":"2006","unstructured":"Abel, A.: Polarized subtyping for sized types. In: Grigoriev, D., Harrison, J., Hirsch, E.A. (eds.) CSR 2006. LNCS, vol.\u00a03967, pp. 381\u2013392. Springer, Heidelberg (2006)"},{"key":"19_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"72","DOI":"10.1007\/11874683_5","volume-title":"Computer Science Logic","author":"A. Abel","year":"2006","unstructured":"Abel, A.: Semi-continuous sized types and termination. In: \u00c9sik, Z. (ed.) CSL 2006. LNCS, vol.\u00a04207, pp. 72\u201388. Springer, Heidelberg (2006)"},{"key":"19_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"10","DOI":"10.1007\/11783596_4","volume-title":"Mathematics of Program Construction","author":"A. Abel","year":"2006","unstructured":"Abel, A.: Towards generic programming with sized types. In: Uustalu, T. (ed.) MPC 2006. LNCS, vol.\u00a04014, pp. 10\u201328. Springer, Heidelberg (2006)"},{"key":"19_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"8","DOI":"10.1007\/978-3-540-73228-0_3","volume-title":"TLCA 2007","author":"A. Abel","year":"2007","unstructured":"Abel, A.: Strong normalization and equi-(co)inductive types. In: Ronchi Della Rocca, S. (ed.) TLCA 2007. LNCS, vol.\u00a04583, pp. 8\u201322. Springer, Heidelberg (2007)"},{"key":"19_CR5","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1016\/j.tcs.2004.10.017","volume":"333","author":"A. Abel","year":"2005","unstructured":"Abel, A., Matthes, R., Uustalu, T.: Iteration schemes for higher-order and nested datatypes. Theor. Comput. Sci.\u00a0333, 3\u201366 (2005)","journal-title":"Theor. Comput. Sci."},{"key":"19_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"48","DOI":"10.1007\/BFb0053541","volume-title":"Foundations of Software Science and Computation Structures","author":"R.M. Amadio","year":"1998","unstructured":"Amadio, R.M., Coupet-Grimal, S.: Analysis of a guard condition in type theory (extended abstract). In: Nivat, M. (ed.) ETAPS 1998 and FOSSACS 1998. LNCS, vol.\u00a01378, pp. 48\u201362. Springer, Heidelberg (1998)"},{"key":"19_CR7","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1017\/S0960129503003943","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\u201345 (2004)","journal-title":"Math. Struct. in Comput. Sci."},{"key":"19_CR8","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"257","DOI":"10.1007\/11916277_18","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"G. Barthe","year":"2006","unstructured":"Barthe, G., Gr\u00e9goire, B., Pastawski, F.: CIC^: Type-based termination of recursive definitions in the Calculus of Inductive Constructions. In: Hermann, M., Voronkov, A. (eds.) LPAR 2006. LNCS (LNAI), vol.\u00a04246, pp. 257\u2013271. Springer, Heidelberg (2006)"},{"key":"19_CR9","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"105","DOI":"10.1007\/11916277_1","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"F. Blanqui","year":"2006","unstructured":"Blanqui, F., Riba, C.: Combining typing and size constraints for checking the termination of higher-order conditional rewrite systems. In: Hermann, M., Voronkov, A. (eds.) LPAR 2006. LNCS (LNAI), vol.\u00a04246, pp. 105\u2013119. Springer, Heidelberg (2006)"},{"key":"19_CR10","doi-asserted-by":"publisher","first-page":"141","DOI":"10.1016\/j.entcs.2006.06.009","volume":"164","author":"N. Ghani","year":"2006","unstructured":"Ghani, N., Hancock, P., Pattinson, D.: Continuous functions on final coalgebras. Electr. Notes in Theor. Comp. Sci.\u00a0164, 141\u2013155 (2006)","journal-title":"Electr. Notes in Theor. Comp. Sci."},{"key":"19_CR11","doi-asserted-by":"crossref","unstructured":"Hughes, J., Pareto, L., Sabry, A.: Proving the correctness of reactive systems using sized types. In: POPL 1996, pp. 410\u2013423 (1996)","DOI":"10.1145\/237721.240882"},{"key":"19_CR12","doi-asserted-by":"publisher","first-page":"159","DOI":"10.1016\/0168-0072(91)90069-X","volume":"51","author":"N.P. Mendler","year":"1991","unstructured":"Mendler, N.P.: Inductive types and type constraints in the second-order lambda calculus. Annals of Pure and Applied Logic\u00a051, 159\u2013172 (1991)","journal-title":"Annals of Pure and Applied Logic"},{"key":"19_CR13","doi-asserted-by":"publisher","first-page":"335","DOI":"10.1016\/0304-3975(92)90042-E","volume":"94","author":"M. Parigot","year":"1992","unstructured":"Parigot, M.: Recursive programming with proofs. Theor. Comput. Sci.\u00a094, 335\u2013356 (1992)","journal-title":"Theor. Comput. Sci."},{"key":"19_CR14","doi-asserted-by":"publisher","first-page":"1461","DOI":"10.2307\/2275652","volume":"62","author":"M. Parigot","year":"1997","unstructured":"Parigot, M.: Proofs of strong normalization for second order classical natural deduction. The Journal of Symbolic Logic\u00a062, 1461\u20131479 (1997)","journal-title":"The Journal of Symbolic Logic"},{"key":"19_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"280","DOI":"10.1007\/BFb0049337","volume-title":"Computer Science Logic","author":"C. Raffalli","year":"1994","unstructured":"Raffalli, C.: Data types, infinity and equality in system AF2. In: Meinke, K., B\u00f6rger, E., Gurevich, Y. (eds.) CSL 1993. LNCS, vol.\u00a0832, pp. 280\u2013294. Springer, Heidelberg (1994)"},{"key":"19_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"317","DOI":"10.1007\/978-3-540-71389-0_23","volume-title":"FOSSACS 2007","author":"C. Riba","year":"2007","unstructured":"Riba, C.: On the stability by union of reducibility candidates. In: Seidl, H. (ed.) FOSSACS 2007. LNCS, vol.\u00a04423, pp. 317\u2013331. Springer, Heidelberg (2007)"},{"key":"19_CR17","unstructured":"Swierstra, W.: I\/O in a dependently typed programming language. Talk presented at TYPES 2007 (2007)"}],"container-title":["Lecture Notes in Computer Science","Programming Languages and Systems"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-76637-7_19.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,27]],"date-time":"2021-04-27T10:56:23Z","timestamp":1619520983000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-76637-7_19"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540766360"],"references-count":17,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-76637-7_19","relation":{},"subject":[]}}