{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,31]],"date-time":"2026-03-31T20:06:35Z","timestamp":1774987595639,"version":"3.50.1"},"reference-count":33,"publisher":"Springer Science and Business Media LLC","issue":"3-4","license":[{"start":{"date-parts":[[2007,10,5]],"date-time":"2007-10-05T00:00:00Z","timestamp":1191542400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Theory Comput Syst"],"published-print":{"date-parts":[[2008,12]]},"DOI":"10.1007\/s00224-007-9056-z","type":"journal-article","created":{"date-parts":[[2007,10,4]],"date-time":"2007-10-04T21:04:19Z","timestamp":1191531859000},"page":"362-393","source":"Crossref","is-referenced-by-count":3,"title":["Datatype-Generic Termination Proofs"],"prefix":"10.1007","volume":"43","author":[{"given":"Roland","family":"Backhouse","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Henk","family":"Doornbos","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2007,10,5]]},"reference":[{"key":"9056_CR1","unstructured":"Backhouse, R.C.: Naturality of homomorphisms. In: International Summer School on Constructive Algorithmics, Lecture Notes, vol. 3 (1989) http:\/\/www.cs.uu.nl\/wiki\/Swiestra\/StopProject"},{"key":"9056_CR2","first-page":"287","volume-title":"Proceedings of the IFIP TC2\/WG2.1 Working Conference on Constructing Programs from Specifications","author":"R.C. Backhouse","year":"1991","unstructured":"Backhouse, R.C., de Bruin, P., Malcolm, G., Voermans, T.S., van der Woude, J.: Relational catamorphisms. In: M\u00f6ller, B. (ed.) Proceedings of the IFIP TC2\/WG2.1 Working Conference on Constructing Programs from Specifications, pp. 287\u2013318. Elsevier Science, Amsterdam (1991)"},{"key":"9056_CR3","series-title":"Workshops in Computing","first-page":"303","volume-title":"Proceedings of the 2nd Conference on Algebraic Methodology and Software Technology, AMAST\u201991","author":"R.C. Backhouse","year":"1992","unstructured":"Backhouse, R.C., de Bruin, P., Hoogendijk, P., Malcolm, G., Voermans, T.S., van der Woude, J.: Polynomial relators. In: Nivat, M., Rattray, C.S., Rus, T., Scollo, G. (eds.) Proceedings of the 2nd Conference on Algebraic Methodology and Software Technology, AMAST\u201991. Workshops in Computing, pp. 303\u2013326. Springer, Berlin (1992)"},{"issue":"4\/5","key":"9056_CR4","doi-asserted-by":"crossref","first-page":"401","DOI":"10.1051\/ita:1999126","volume":"33","author":"R. Backhouse","year":"1999","unstructured":"Backhouse, R., Hoogendijk, P.: Final dialgebras: from categories to allegories. Theor. Inform. Appl. 33(4\/5), 401\u2013426 (1999)","journal-title":"Theor. Inform. Appl."},{"key":"9056_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"28","DOI":"10.1007\/10704973_2","volume-title":"3rd International Summer School on Advanced Functional Programming","author":"R. Backhouse","year":"1999","unstructured":"Backhouse, R., Jansson, P., Jeuring, J., Meertens, L.: Generic programming. An introduction. In: Swierstra, S.D. (ed.) 3rd International Summer School on Advanced Functional Programming, Braga, Portugal, 12\u201319 September 1998. Lecture Notes in Computer Science, vol. 1608, pp. 28\u2013115. Springer, Berlin (1999)"},{"issue":"4","key":"9056_CR6","doi-asserted-by":"crossref","first-page":"417","DOI":"10.1017\/S096012950000030X","volume":"3","author":"R.C. Backhouse","year":"1993","unstructured":"Backhouse, R.C., van der Woude, J.: Demonic operators and monotype factors. Math. Struct. Comput. Sci. 3(4), 417\u2013433 (1993)","journal-title":"Math. Struct. Comput. Sci."},{"key":"9056_CR7","volume-title":"Algebra of Programming","author":"R.S. Bird","year":"1996","unstructured":"Bird, R.S., de Moor, O.: Algebra of Programming. Prentice-Hall, Englewood Cliffs (1996)"},{"key":"9056_CR8","unstructured":"Doornbos, H.: Reductivity arguments and program construction. Ph.D. thesis, Department of Mathematics and Computing Science, Eindhoven University of Technology (June 1996)"},{"key":"9056_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"242","DOI":"10.1007\/3-540-60117-1_14","volume-title":"Mathematics of Program Construction, 3rd International Conference","author":"H. Doornbos","year":"1995","unstructured":"Doornbos, H., Backhouse, R.: Induction and recursion on datatypes. In: M\u00f6ller, B. (ed.) Mathematics of Program Construction, 3rd International Conference. Lecture Notes in Computer Science, vol. 947, pp. 242\u2013256. Springer, Berlin (1995)"},{"key":"9056_CR10","doi-asserted-by":"crossref","first-page":"103","DOI":"10.1016\/S0304-3975(96)00154-5","volume":"179","author":"H. Doornbos","year":"1997","unstructured":"Doornbos, H., Backhouse, R.C., van der Woude, J.: A calculational approach to mathematical induction. Theor. Comput. Sci. 179, 103\u2013135 (1997)","journal-title":"Theor. Comput. Sci."},{"issue":"1\u20133","key":"9056_CR11","doi-asserted-by":"crossref","first-page":"217","DOI":"10.1016\/0167-6423(95)00027-5","volume":"26","author":"H. Doornbos","year":"1996","unstructured":"Doornbos, H., Backhouse, R.: Reductivity. Sci. Comput. Program. 26(1\u20133), 217\u2013236 (1996)","journal-title":"Sci. Comput. Program."},{"key":"9056_CR12","unstructured":"Fokkinga, M.M.: Law and order in algorithmics. Ph.D. thesis, Universiteit Twente, The Netherlands (1992)"},{"key":"9056_CR13","series-title":"Lecture Notes in Mathematics","first-page":"95","volume-title":"Category Theory, Proceedings of COMO 1990","author":"P. Freyd","year":"1990","unstructured":"Freyd, P.: Algebraically complete categories. In: Rosolini, G., Carboni, A., Pedicchio, M.C. (eds.) Category Theory, Proceedings of COMO 1990. Lecture Notes in Mathematics, vol. 1488, pp. 95\u2013104. Springer, New York (1990)"},{"key":"9056_CR14","volume-title":"Categories, Allegories","author":"P.J. Freyd","year":"1990","unstructured":"Freyd, P.J., \u0160\u010dedrov, A.: Categories, Allegories. North-Holland, Amsterdam (1990)"},{"key":"9056_CR15","unstructured":"Gibbons, J.: Patterns in datatype-generic programming. In: Striegnitz, J., Davis, K. (eds.) First International Workshop on Declarative Programming in the Context of Object-Oriented Languages (DPCOOL). Multiparadigm Programming, vol. 27. John von Neumann Institute for Computing (NIC) (2003)"},{"issue":"2\u20133","key":"9056_CR16","doi-asserted-by":"crossref","first-page":"129","DOI":"10.1016\/S0167-6423(02)00025-4","volume":"43","author":"R. Hinze","year":"2002","unstructured":"Hinze, R.: Polytypic values possess polykinded types. Sci. Comput. Program. 43(2\u20133), 129\u2013159 (2002)","journal-title":"Sci. Comput. Program"},{"issue":"1\/2","key":"9056_CR17","doi-asserted-by":"crossref","first-page":"117","DOI":"10.1016\/j.scico.2003.07.001","volume":"51","author":"R. Hinze","year":"2004","unstructured":"Hinze, R., Jeuring, J., L\u00f6h, A.: Type-indexed data types. Sci. Comput. Program. 51(1\/2), 117\u2013151 (2004)","journal-title":"Sci. Comput. Program."},{"key":"9056_CR18","doi-asserted-by":"crossref","first-page":"51","DOI":"10.3233\/FI-1986-9104","volume":"9","author":"C.A.R. Hoare","year":"1986","unstructured":"Hoare, C.A.R., He, J.: The weakest prespecification. Fundamenta Informaticae 9, 51\u201384 (1986). 217\u2013252","journal-title":"Fundamenta Informaticae"},{"key":"9056_CR19","unstructured":"Hoogendijk, P.: A generic theory of datatypes. Ph.D. thesis, Department of Mathematics and Computing Science, Eindhoven University of Technology (1997)"},{"issue":"2","key":"9056_CR20","doi-asserted-by":"crossref","first-page":"191","DOI":"10.1017\/S0956796899003640","volume":"10","author":"P. Hoogendijk","year":"2000","unstructured":"Hoogendijk, P., de\u00a0Moor, O.: Container types categorically. J. Funct. Program. 10(2), 191\u2013225 (2000)","journal-title":"J. Funct. Program."},{"key":"9056_CR21","doi-asserted-by":"crossref","first-page":"470","DOI":"10.1145\/263699.263763","volume-title":"POPL \u201997: the 24th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages","author":"P. Jansson","year":"1997","unstructured":"Jansson, P., Jeuring, J.: PolyP\u2014a polytypic programming language extension. In: POPL \u201997: the 24th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 470\u2013482. ACM, New York (1997)"},{"issue":"5","key":"9056_CR22","doi-asserted-by":"crossref","first-page":"527","DOI":"10.1017\/S095679689800313X","volume":"8","author":"P. Jansson","year":"1998","unstructured":"Jansson, P., Jeuring, J.: Functional pearl: Polytypic unification. J. Funct. Program. 8(5), 527\u2013536 (1998)","journal-title":"J. Funct. Program."},{"key":"9056_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"68","DOI":"10.1007\/3-540-61628-4_3","volume-title":"Proceedings of the Second International Summer School on Advanced Functional Programming Techniques","author":"J. Jeuring","year":"1996","unstructured":"Jeuring, J., Jansson, P.: Polytypic programming. In: Launchbury, J., Meijer, E., Sheard, T. (eds.) Proceedings of the Second International Summer School on Advanced Functional Programming Techniques. Lecture Notes in Computer Science, vol. 1129, pp. 68\u2013114. Springer, Berlin (1996)"},{"key":"9056_CR24","first-page":"141","volume-title":"Proceedings of the International Conference, ICFP\u201903","author":"A. L\u00f6h","year":"2003","unstructured":"L\u00f6h, A., Clarke, D., Jeuring, J.: Dependency-style generic Haskell. In: Shivers, O. (ed.) Proceedings of the International Conference, ICFP\u201903, pp. 141\u2013152. ACM, New York (2003)"},{"key":"9056_CR25","unstructured":"Malcolm, G.: Algebraic data types and program transformation. Ph.D. thesis, Groningen University (1990)"},{"issue":"2\u20133","key":"9056_CR26","doi-asserted-by":"crossref","first-page":"255","DOI":"10.1016\/0167-6423(90)90023-7","volume":"14","author":"G. Malcolm","year":"1990","unstructured":"Malcolm, G.: Data structures and program transformation. Sci. Comput. Program. 14(2\u20133), 255\u2013280 (1990)","journal-title":"Sci. Comput. Program."},{"issue":"3","key":"9056_CR27","doi-asserted-by":"crossref","first-page":"131","DOI":"10.1016\/0020-0190(94)00195-5","volume":"53","author":"Mathematics of Program Construction Group, Eindhoven University of Technology","year":"1995","unstructured":"Mathematics of Program Construction Group, Eindhoven University of Technology: Fixed point calculus. Inf. Proc. Lett. 53(3), 131\u2013136 (1995)","journal-title":"Inf. Proc. Lett."},{"issue":"5","key":"9056_CR28","doi-asserted-by":"crossref","first-page":"413","DOI":"10.1007\/BF01211391","volume":"4","author":"L. Meertens","year":"1992","unstructured":"Meertens, L.: Paramorphisms. Formal Aspects Comput. 4(5), 413\u2013424 (1992)","journal-title":"Formal Aspects Comput."},{"key":"9056_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"124","DOI":"10.1007\/3540543961_7","volume-title":"FPCA \u201991: Functional Programming Languages and Computer Architecture","author":"E. Meijer","year":"1991","unstructured":"Meijer, E., Fokkinga, M., Paterson, R.: Functional programming with bananas, lenses, envelopes and barbed wire. In: FPCA \u201991: Functional Programming Languages and Computer Architecture. Lecture Notes in Computer Science, vol. 523, pp. 124\u2013144. Springer, Berlin (1991)"},{"key":"9056_CR30","unstructured":"Meijer, E.: Calculating compilers. Ph.D. thesis, University of Nijmegen (1992)"},{"issue":"1","key":"9056_CR31","doi-asserted-by":"crossref","first-page":"55","DOI":"10.1016\/0890-5401(91)90052-4","volume":"93","author":"E. Moggi","year":"1991","unstructured":"Moggi, E.: Notions of computation and monads. Inf. Comput. 93(1), 55\u201392 (1991)","journal-title":"Inf. Comput."},{"key":"9056_CR32","first-page":"513","volume-title":"IFIP \u201983","author":"J.C. Reynolds","year":"1983","unstructured":"Reynolds, J.C.: Types, abstraction and parametric polymorphism. In: Mason, R.E. (ed.) IFIP \u201983, pp.\u00a0513\u2013523. Elsevier Science, Amsterdam (1983)"},{"key":"9056_CR33","volume-title":"4th Symposium on Functional Programming Languages and Computer Architecture","author":"P. Wadler","year":"1989","unstructured":"Wadler, P.: Theorems for free!. In: 4th Symposium on Functional Programming Languages and Computer Architecture. ACM, London (1989)"}],"container-title":["Theory of Computing Systems"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00224-007-9056-z.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s00224-007-9056-z\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00224-007-9056-z","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,8,25]],"date-time":"2021-08-25T06:22:29Z","timestamp":1629872549000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s00224-007-9056-z"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2007,10,5]]},"references-count":33,"journal-issue":{"issue":"3-4","published-print":{"date-parts":[[2008,12]]}},"alternative-id":["9056"],"URL":"https:\/\/doi.org\/10.1007\/s00224-007-9056-z","relation":{},"ISSN":["1432-4350","1433-0490"],"issn-type":[{"value":"1432-4350","type":"print"},{"value":"1433-0490","type":"electronic"}],"subject":[],"published":{"date-parts":[[2007,10,5]]}}}