{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,12,31]],"date-time":"2025-12-31T02:57:18Z","timestamp":1767149838177,"version":"build-2238731810"},"reference-count":51,"publisher":"Elsevier BV","issue":"1-2","license":[{"start":{"date-parts":[[2002,2,1]],"date-time":"2002-02-01T00:00:00Z","timestamp":1012521600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/tdm\/userlicense\/1.0\/"},{"start":{"date-parts":[[2002,2,1]],"date-time":"2002-02-01T00:00:00Z","timestamp":1012521600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/legal\/tdmrep-license"},{"start":{"date-parts":[[2013,7,17]],"date-time":"2013-07-17T00:00:00Z","timestamp":1374019200000},"content-version":"vor","delay-in-days":4184,"URL":"http:\/\/www.elsevier.com\/open-access\/userlicense\/1.0\/"}],"content-domain":{"domain":["elsevier.com","sciencedirect.com"],"crossmark-restriction":true},"short-container-title":["Theoretical Computer Science"],"published-print":{"date-parts":[[2002,2]]},"DOI":"10.1016\/s0304-3975(00)00347-9","type":"journal-article","created":{"date-parts":[[2002,7,25]],"date-time":"2002-07-25T06:11:15Z","timestamp":1027577475000},"page":"41-68","update-policy":"https:\/\/doi.org\/10.1016\/elsevier_cm_policy","source":"Crossref","is-referenced-by-count":36,"title":["Inductive-data-type systems"],"prefix":"10.1016","volume":"272","author":[{"given":"Fr\u00e9d\u00e9ric","family":"Blanqui","sequence":"first","affiliation":[]},{"given":"Jean-Pierre","family":"Jouannaud","sequence":"additional","affiliation":[]},{"given":"Mitsuhiro","family":"Okada","sequence":"additional","affiliation":[]}],"member":"78","reference":[{"key":"10.1016\/S0304-3975(00)00347-9_BIB1","unstructured":"F. Barbanera, M. Fern\u00e1ndez, Combining first and higher order rewrite systems with type assignment systems, Proc. 1st Internat. Conf. on Typed Lambda Calculi and Applications, Lecture Notes in Computer Science, vol. 664, Springer, Berlin, 1993."},{"key":"10.1016\/S0304-3975(00)00347-9_BIB2","doi-asserted-by":"crossref","unstructured":"F. Barbanera, M. Fern\u00e1ndez, Modularity of termination and confluence in combinations of rewrite systems with \u03bb\u03c9, Proc. 20th Internat. Colloq. on Automata, Languages, and Programming, Lecture Notes in Computer Science, vol. 700, Springer, Berlin, 1993.","DOI":"10.1007\/3-540-56939-1_110"},{"key":"10.1016\/S0304-3975(00)00347-9_BIB3","unstructured":"F. Barbanera, M. Fern\u00e1ndez, H. Geuvers, Modularity of strong normalization and confluence in the algebraic-\u03bb-cube, Proc. 9th Symp. on Logic in Computer Science, IEEE Computer Society, 1994."},{"key":"10.1016\/S0304-3975(00)00347-9_BIB4","article-title":"Lambda calculi with types","volume":"vol. 2","author":"Barendregt","year":"1992"},{"key":"10.1016\/S0304-3975(00)00347-9_BIB5","doi-asserted-by":"crossref","unstructured":"F. Blanqui, Termination and confluence of higher-order rewrite systems, Proc. 11th Internat. Conf. on Rewriting Techniques and Applications, 2000. Lecture Notes in Computer Science, to appear. Available at http:\/\/www.lri.fr\/b\u0303lanqui\/.","DOI":"10.1007\/10721975_4"},{"key":"10.1016\/S0304-3975(00)00347-9_BIB6","doi-asserted-by":"crossref","unstructured":"F. Blanqui, J.-P. Jouannaud, M. Okada, The calculus of algebraic constructions, Proc. 10th Internat. Conf. on Rewriting Techniques and Applications, Lecture Notes in Computer Science, vol. 1631, Springer, Berlin, 1999.","DOI":"10.1007\/3-540-48685-2_25"},{"key":"10.1016\/S0304-3975(00)00347-9_BIB7","doi-asserted-by":"crossref","unstructured":"A. Bouhoula, J.-P. Jouannaud, J. Meseguer, Specification and proof in membership equational logic, Theoret. Comput. Sci. 236 (1999).","DOI":"10.1016\/S0304-3975(99)00206-6"},{"key":"10.1016\/S0304-3975(00)00347-9_BIB8","unstructured":"V. Breazu-Tannen, Combining algebra and higher-order types, Proc. 3rd Symp. on Logic in Computer Science, IEEE Computer Society, 1988."},{"key":"10.1016\/S0304-3975(00)00347-9_BIB9","doi-asserted-by":"crossref","unstructured":"V. Breazu-Tannen, J. Gallier, Polymorphic rewriting conserves algebraic strong normalization, Proc. 16th Internat. Colloq. on Automata, Languages, and Programming, Lecture Notes in Computer Science, vol. 372, Springer, Berlin, 1989.","DOI":"10.1007\/BFb0035757"},{"key":"10.1016\/S0304-3975(00)00347-9_BIB10","doi-asserted-by":"crossref","unstructured":"V. Breazu-Tannen, J. Gallier, Polymorphic rewriting conserves algebraic strong normalization, Theoret. Comput. Sci. 83(1) (1991).","DOI":"10.1016\/0304-3975(91)90037-3"},{"key":"10.1016\/S0304-3975(00)00347-9_BIB11","unstructured":"H. Comon, M. Dauchet, R. Gilleron, F. Jacquemard, D. Lugiez, S. Tison, M. Tommasi, Tree automata techniques and applications. Available at http:\/\/www.grappa.univ-lille3.fr\/tata\/, 1997."},{"key":"10.1016\/S0304-3975(00)00347-9_BIB12","series-title":"Pattern matching with dependent types, Proc. 3rd Work. on Types for Proofs and Programs","author":"Coquand","year":"1992"},{"key":"10.1016\/S0304-3975(00)00347-9_BIB13","doi-asserted-by":"crossref","unstructured":"T. Coquand, G. Huet, Constructions: a higher order proof system for mechanizing mathematics, Proc. 1985 European Conf. on Computer Algebra, Lecture Notes in Computer Science, vol. 203, Springer, Berlin, 1985.","DOI":"10.1007\/3-540-15983-5_13"},{"key":"10.1016\/S0304-3975(00)00347-9_BIB14","unstructured":"T. Coquand, C. Paulin-Mohring, Inductively defined types, Proc. 1988 Internat. Conf. on Computer Logic, Lecture Notes in Computer Science, vol. 417, Springer, Berlin, 1988."},{"key":"10.1016\/S0304-3975(00)00347-9_BIB15","doi-asserted-by":"crossref","unstructured":"N. de Bruijn, The mathematical language Automath, its usage, and some of its extensions, Proc. Symp. on Automatic Demonstration, Lecture Notes in Computer Science, vol. 125, Springer, Berlin, 1970. (Reprinted in: Selected Papers on Automath, in: R.P. Nederpelt, J.H. Geuvers, R.C. de Vrijer (Eds.), Studies in Logic, vol. 133. North-Holland, Amsterdam, 1994).","DOI":"10.1007\/BFb0060623"},{"key":"10.1016\/S0304-3975(00)00347-9_BIB16","doi-asserted-by":"crossref","unstructured":"N. Dershowitz, J.-P. Jouannaud, Rewrite systems, in: J. van Leeuwen (Ed.), Handbook of Theoretical Computer Science, vol. B: Formal Models and Semantics, chapter 6: Rewrite Systems, North-Holland, Amsterdam, 1990.","DOI":"10.1016\/B978-0-444-88074-1.50011-1"},{"key":"10.1016\/S0304-3975(00)00347-9_BIB17","series-title":"Theorem proving modulo, Tech. Report 3400","author":"Dowek","year":"1998"},{"key":"10.1016\/S0304-3975(00)00347-9_BIB18","series-title":"Proof normalization modulo, Tech. Report 3542","author":"Dowek","year":"1998"},{"key":"10.1016\/S0304-3975(00)00347-9_BIB19","series-title":"Logic and Computer Science","article-title":"On Girard's \u201cCandidats de R\u00e9ductibilit\u00e9\u201d","author":"Gallier","year":"1990"},{"key":"10.1016\/S0304-3975(00)00347-9_BIB20","doi-asserted-by":"crossref","unstructured":"E. Gim\u00e9nez, Codifying guarded definitions with recursion schemes, Proc. 5th Work. on Types for Proofs and Programs, Lecture Notes in Computer Science, vol. 996, Springer, Berlin, 1994.","DOI":"10.1007\/3-540-60579-7_3"},{"key":"10.1016\/S0304-3975(00)00347-9_BIB21","doi-asserted-by":"crossref","unstructured":"E. Gim\u00e9nez, Structural recursive definitions in type theory, Proc. 25th Internat. Colloq. on Automata, Languages, and Programming, Lecture Notes in Computer Science, vol. 1443, Springer, Berlin, 1998.","DOI":"10.1007\/BFb0055070"},{"key":"10.1016\/S0304-3975(00)00347-9_BIB22","doi-asserted-by":"crossref","unstructured":"J.-Y. Girard, Une extension de l'interpr\u00e9tation de G\u00f6del \u00e0 l'analyse, et son application \u00e0 l\u2019\u00e9limination des coupures dans l'analyse et la th\u00e9orie des types, in: J.E. Fenstad (Ed.), Proc. 2nd Scandinavian Logic Symp., of Studies in Logic and the Foundations of Mathematics, vol. 63, North-Holland, Amsterdam, 1971.","DOI":"10.1016\/S0049-237X(08)70843-7"},{"key":"10.1016\/S0304-3975(00)00347-9_BIB23","unstructured":"J.-Y. Girard, Interpr\u00e9tation fonctionelle et \u00e9limination des coupures dans l'arithmetique d'ordre sup\u00e9rieur. Ph.D. Thesis, Universit\u00e9 Paris VII, France, 1972."},{"key":"10.1016\/S0304-3975(00)00347-9_BIB24","series-title":"Proofs and Types","author":"Girard","year":"1988"},{"key":"10.1016\/S0304-3975(00)00347-9_BIB25","unstructured":"K. G\u00f6del, On intuitionistic arithmetic and number theory, in: M. Davis (Ed.), The Undecidable, Raven Press, New York, 1965."},{"key":"10.1016\/S0304-3975(00)00347-9_BIB26","unstructured":"K. Hasebe, On extensions of G\u00f6del's System T, Master's Thesis, Keio University, Japan, 2000 (in Japanese)."},{"key":"10.1016\/S0304-3975(00)00347-9_BIB27","unstructured":"J.-P. Jouannaud, M. Okada, Executable higher-order algebraic specification languages, Proc. 6th Symp. on Logic in Computer Science, IEEE Computer Society, 1991."},{"key":"10.1016\/S0304-3975(00)00347-9_BIB28","doi-asserted-by":"crossref","unstructured":"J.-P. Jouannaud, M. Okada, Abstract data type systems, Theoret. Comput. Sci. 173(2) (1997).","DOI":"10.1016\/S0304-3975(96)00161-2"},{"key":"10.1016\/S0304-3975(00)00347-9_BIB29","unstructured":"J.-P. Jouannaud, A. Rubio. The higher-order recursive path ordering, Proc. 14th Symp. on Logic in Computer Science, IEEE Computer Society, 1999."},{"key":"10.1016\/S0304-3975(00)00347-9_BIB30","unstructured":"J.W. Klop, Combinatory reduction systems, Ph.D. Thesis, University of Utrecht, Netherlands, 1980. Published as Mathematical Center Tract 129."},{"key":"10.1016\/S0304-3975(00)00347-9_BIB31","doi-asserted-by":"crossref","unstructured":"J.W. Klop, V. van Oostrom, F. van Raamsdonk, Combinatory reduction systems: introduction and survey, Theoret. Comput. Sci. 121 (1\u20132) (1993).","DOI":"10.1016\/0304-3975(93)90091-7"},{"key":"10.1016\/S0304-3975(00)00347-9_BIB32","doi-asserted-by":"crossref","unstructured":"P. Martin-L\u00f6f, An intuitionistic theory of types: predicative part, in: H.E. Rose, J.C. Shepherdson (Eds.), Proc 73\u2019 Logic Colloq., Studies in Logic and the Foundations of Mathematics, vol. 80, North-Holland, Amsterdam, 1975.","DOI":"10.1016\/S0049-237X(08)71945-1"},{"key":"10.1016\/S0304-3975(00)00347-9_BIB33","series-title":"Intuitionistic Type Theory","author":"Martin-L\u00f6f","year":"1984"},{"key":"10.1016\/S0304-3975(00)00347-9_BIB34","doi-asserted-by":"crossref","unstructured":"R. Mayr, T. Nipkow, Higher-order rewrite systems and their confluence, Theoret. Comput. Sci. 192 (1998).","DOI":"10.1016\/S0304-3975(97)00143-6"},{"key":"10.1016\/S0304-3975(00)00347-9_BIB35","unstructured":"N.P. Mendler, First- and second-order lambda calculi with recursive types, Tech. Report TR 86-764, Cornell University, United States, 1986."},{"key":"10.1016\/S0304-3975(00)00347-9_BIB36","unstructured":"N.P. Mendler, Inductive definition in type theory, Ph.D. Thesis, Cornell University, United States, 1987."},{"key":"10.1016\/S0304-3975(00)00347-9_BIB37","unstructured":"D. Miller, A logic programming language with lambda-abstraction, function variables, and simple unification, Proc. 1989 Internat. Work. on Extensions of Logic Programming, Lecture Notes in Computer Science, vol. 475, Springer, Berlin, 1989."},{"key":"10.1016\/S0304-3975(00)00347-9_BIB38","unstructured":"B. Monate, Automates de formes normales et r\u00e9ductibilit\u00e9 inductive, Master's Thesis, Universit\u00e9 Paris-Sud, France, 1997."},{"key":"10.1016\/S0304-3975(00)00347-9_BIB39","unstructured":"T. Nipkow, Higher-order critical pairs, Proc. 6th Symp. on Logic in Computer Science, IEEE Computer Society, 1991."},{"key":"10.1016\/S0304-3975(00)00347-9_BIB40","series-title":"Strong normalizability for the combined system of the typed lambda calculus and an arbitrary convergent term rewrite system, Proc. 1989 Internat. Symp. on Symbolic and Algebraic Computation","author":"Okada","year":"1989"},{"key":"10.1016\/S0304-3975(00)00347-9_BIB41","unstructured":"M. Okada, P.J. Scott, A note on rewriting theory for uniqueness of iteration, Theory Appl. Categories, 6(4) (2000)."},{"key":"10.1016\/S0304-3975(00)00347-9_BIB42","unstructured":"C. Prehofer, Solving higher-order equations: from logic to programming, Ph.D. Thesis, Technische Universit\u00e4t M\u00fcnchen, Germany, 1995."},{"key":"10.1016\/S0304-3975(00)00347-9_BIB43","doi-asserted-by":"crossref","unstructured":"Z. Qian, Linear unification of higher-order patterns, Proc. 7th Internat. Joint Conf. CAAP\/FASE on Theory and Practice of Software Development, Lecture Notes in Computer Science, vol. 668, Springer, Berlin, 1993.","DOI":"10.1007\/3-540-56610-4_78"},{"key":"10.1016\/S0304-3975(00)00347-9_BIB44","doi-asserted-by":"crossref","unstructured":"M.P.A. Sellink, Verifying process algebra proofs in type theory, Proc. Internat. Work. on Semantics of Specification Languages, Workshops in Computing, 1993.","DOI":"10.1007\/978-1-4471-3229-5_18"},{"key":"10.1016\/S0304-3975(00)00347-9_BIB45","series-title":"Combinators, Lambda-Terms and Proof Theory","author":"Stenlund","year":"1972"},{"key":"10.1016\/S0304-3975(00)00347-9_BIB46","doi-asserted-by":"crossref","unstructured":"W.W. Tait, Intensional interpretations of functionals of finite type I, J. Symbolic Logic 32(2) (1967).","DOI":"10.2307\/2271658"},{"key":"10.1016\/S0304-3975(00)00347-9_BIB47","doi-asserted-by":"crossref","unstructured":"Y. Toyama, Counterexamples to terminating for the direct sum of term rewriting systems, Inform. Process. Lett. 25(3) (1986).","DOI":"10.1016\/0020-0190(87)90122-0"},{"key":"10.1016\/S0304-3975(00)00347-9_BIB48","unstructured":"J. van de Pol, Termination proofs for higher-order rewrite systems, Proc. 1st Internat. Work. on Higher-Order Algebra, Logic and Term Rewriting, Lecture Notes in Computer Science, vol. 816, Springer, Berlin, 1993."},{"key":"10.1016\/S0304-3975(00)00347-9_BIB49","unstructured":"V. van Oostrom, Confluence for abstract and higher-order rewriting, Ph.D. Thesis, Vrije Universiteit, Netherlands, 1994."},{"key":"10.1016\/S0304-3975(00)00347-9_BIB50","unstructured":"F. van Raamsdonk, Confluence and normalization for higher-order rewriting, Ph.D. Thesis, Vrije Universiteit, Netherlands, 1996."},{"key":"10.1016\/S0304-3975(00)00347-9_BIB51","unstructured":"B. Werner, Une Th\u00e9orie des Constructions Inductives, Ph.D. Thesis, Universit\u00e9 Paris VII, France, 1994."}],"updated-by":[{"DOI":"10.1016\/j.tcs.2018.01.010","type":"erratum","label":"Erratum","source":"publisher","updated":{"date-parts":[[2020,5,12]],"date-time":"2020-05-12T00:00:00Z","timestamp":1589241600000}}],"container-title":["Theoretical Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S0304397500003479?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S0304397500003479?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2025,10,5]],"date-time":"2025-10-05T00:52:39Z","timestamp":1759625559000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/S0304397500003479"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2002,2]]},"references-count":51,"journal-issue":{"issue":"1-2","published-print":{"date-parts":[[2002,2]]}},"alternative-id":["S0304397500003479"],"URL":"https:\/\/doi.org\/10.1016\/s0304-3975(00)00347-9","relation":{},"ISSN":["0304-3975"],"issn-type":[{"value":"0304-3975","type":"print"}],"subject":[],"published":{"date-parts":[[2002,2]]},"assertion":[{"value":"Elsevier","name":"publisher","label":"This article is maintained by"},{"value":"Inductive-data-type systems","name":"articletitle","label":"Article Title"},{"value":"Theoretical Computer Science","name":"journaltitle","label":"Journal Title"},{"value":"https:\/\/doi.org\/10.1016\/S0304-3975(00)00347-9","name":"articlelink","label":"CrossRef DOI link to publisher maintained version"},{"value":"converted-article","name":"content_type","label":"Content Type"},{"value":"Copyright \u00a9 2002 Elsevier Science B.V. All rights reserved.","name":"copyright","label":"Copyright"}]}}