{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2022,3,29]],"date-time":"2022-03-29T00:33:39Z","timestamp":1648514019880},"reference-count":22,"publisher":"Elsevier BV","issue":"7","license":[{"start":{"date-parts":[[2003,9,1]],"date-time":"2003-09-01T00:00:00Z","timestamp":1062374400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/tdm\/userlicense\/1.0\/"},{"start":{"date-parts":[[2013,7,29]],"date-time":"2013-07-29T00:00:00Z","timestamp":1375056000000},"content-version":"vor","delay-in-days":3619,"URL":"http:\/\/creativecommons.org\/licenses\/by-nc-nd\/3.0\/"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Electronic Notes in Theoretical Computer Science"],"published-print":{"date-parts":[[2003,9]]},"DOI":"10.1016\/s1571-0661(04)80760-6","type":"journal-article","created":{"date-parts":[[2004,9,29]],"date-time":"2004-09-29T12:47:47Z","timestamp":1096462067000},"page":"106-124","source":"Crossref","is-referenced-by-count":3,"title":["Remarks on Isomorphisms of Simple Inductive Types"],"prefix":"10.1016","volume":"85","author":[{"given":"David","family":"Chemouil","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Sergei","family":"Soloviev","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"78","reference":[{"key":"10.1016\/S1571-0661(04)80760-6_NEWBIB1","series-title":"\u201cTerm Rewriting and All That,\u201d","author":"Baader","year":"1998"},{"key":"10.1016\/S1571-0661(04)80760-6_NEWBIB2","doi-asserted-by":"crossref","unstructured":"Bachmair L. and N. Dershowitz, Commutation, transformation, and termination, in: J. H. Siekmann, editor, Proceedings of the Eighth International Conference on Automated Deduction (Oxford, England), Lecture Notes in Computer Science 230 (1986), pp. 5\u201320.","DOI":"10.1007\/3-540-16780-3_76"},{"key":"10.1016\/S1571-0661(04)80760-6_NEWBIB3","series-title":"\u201cThe Lambda Calculus - Its Syntax and Semantics,\u201d","author":"Barendregt","year":"1984"},{"key":"10.1016\/S1571-0661(04)80760-6_NEWBIB4","series-title":"Handbook of Logic in Computer Science","article-title":"Lambda calculi with types","author":"Barendregt","year":"1992"},{"key":"10.1016\/S1571-0661(04)80760-6_NEWBIB5","unstructured":"Barras B., S. Boutin, C. Cornes, J. Courant, J.-C. Filliatre, E. Gimenez, H. Herbelin, G. Huet, C. Munoz, C. Murthy, C. Parent, C. Paulin-Mohring, A. Saibi and B. Werner, The Coq proof assistant reference manual: Version 6.1, Technical Report RT-0203, Inria (Institut National de Recherche en Informatique et en Automatique), France (1997)."},{"key":"10.1016\/S1571-0661(04)80760-6_NEWBIB6","doi-asserted-by":"crossref","unstructured":"Barthe G. and O. Pons, Type isomorphisms and proof reuse in dependent type theory, in: F. Honsell and M. Miculan, editors, Proceedings 4th Int. Conf. on Found. of Software Science and Computation Structures, FoSSaCS'01, Genova, Italy, 2\u20136 Apr. 2001, Lecture Notes in Computer Science 2030, Springer-Verlag, Berlin, 2001, pp. 57\u201371.","DOI":"10.1007\/3-540-45315-6_4"},{"key":"10.1016\/S1571-0661(04)80760-6_NEWBIB7","doi-asserted-by":"crossref","unstructured":"Blanqui F., J.-P. Jouannaud and M. Okada, The calculus of algebraic constructions, in: P. Narendran and M. Rusinowitch, editors, Proceedings of the 10th International Conference on Rewriting Techniques and Applications (RTA-99) (1999), pp. 301\u2013316.","DOI":"10.1007\/3-540-48685-2_25"},{"key":"10.1016\/S1571-0661(04)80760-6_NEWBIB8","doi-asserted-by":"crossref","first-page":"41","DOI":"10.1016\/S0304-3975(00)00347-9","article-title":"Inductive-data type systems","volume":"272","author":"Blanqui","year":"2002","journal-title":"Theoretical Computer Science"},{"key":"10.1016\/S1571-0661(04)80760-6_NEWBIB9","unstructured":"Bruce K., R. Di Cosmo and G. Longo, Provable isomorphisms of types, Technical Report 90-14, LIENS, \u00c9cole Normale Sup\u00e9rieure, Paris (1990)."},{"key":"10.1016\/S1571-0661(04)80760-6_NEWBIB10","doi-asserted-by":"crossref","first-page":"323","DOI":"10.1016\/0304-3975(76)90085-2","article-title":"Characterization of normal forms possessing inverse in the \u03bb _ \u03b2 _ \u03b7-calculus","volume":"2","author":"Dezani-Ciancaglini","year":"1976","journal-title":"Theoretical Computer Science"},{"key":"10.1016\/S1571-0661(04)80760-6_NEWBIB11","series-title":"Progress in Theoretical Computer Science","article-title":"\u201cIsomorphisms of Types: From \u03bb-Calculus to Information Retrieval and Language Design,\u201d","author":"Di Cosmo","year":"1995"},{"key":"10.1016\/S1571-0661(04)80760-6_NEWBIB12","doi-asserted-by":"crossref","first-page":"195","DOI":"10.1093\/jigpal\/6.2.195","article-title":"On the union of well-founded relations","volume":"6","author":"Doornbos","year":"1998","journal-title":"Logic Journal of the IGPL"},{"key":"10.1016\/S1571-0661(04)80760-6_NEWBIB13","unstructured":"Dowek G., G. Huet and B. Werner, On the definition of the eta-long normal form in type systems of the cube, in: H. Geuvers, editor, Informal Proceedings of the Workshop on Types for Proofs and Programs, Nijmegen, The Netherlands, 1993."},{"key":"10.1016\/S1571-0661(04)80760-6_NEWBIB14","unstructured":"Geser A., \u201cRelative Termination,\u201d Ph.D. thesis, Universit\u00e4t Passau, Passau, Germany (1990)."},{"key":"10.1016\/S1571-0661(04)80760-6_NEWBIB15","doi-asserted-by":"crossref","unstructured":"Geuvers H., The Church-Rosser property for \u03b2\u03b7-reduction in typed \u03bb-calculi, in: Proceedings, Seventh Annual IEEE Symposium on Logic in Computer Science, IEEE Computer Society Press, Santa Cruz, California, 1992, pp. 453\u2013460.","DOI":"10.1109\/LICS.1992.185556"},{"key":"10.1016\/S1571-0661(04)80760-6_NEWBIB16","unstructured":"Geuvers H., \u201cLogics and Type Systems,\u201d Ph.D. thesis, Computer Science Institute, Katholieke Universiteit Nijmegen (1993)."},{"key":"10.1016\/S1571-0661(04)80760-6_NEWBIB17","unstructured":"Goguen H., A typed operational semantics for type theory, LFCS report ECS-LFCS-94-304, University of Edinburgh, Department of Computer Science (1994)."},{"key":"10.1016\/S1571-0661(04)80760-6_NEWBIB18","series-title":"\u201cComputation and Reasoning: A Type Theory for Computer Science\u201d","author":"Luo","year":"1994"},{"key":"10.1016\/S1571-0661(04)80760-6_NEWBIB19","unstructured":"Paulin-Mohring C., Inductive definitions in the system Coq. Rules and properties, in: M. Bezem and J. F. Groote, editors, Proceedings of the 1st International Conference on Typed Lambda Calculi and Applications, TCLA'93, Utrecht, The Netherlands, Lecture Notes in Computer Science 664 (1993), pp. 328\u2013345."},{"key":"10.1016\/S1571-0661(04)80760-6_NEWBIB20","doi-asserted-by":"crossref","unstructured":"Soloviev, S. V., The category of finite sets and Cartesian closed categories, in: Theoretical Applications of Methods of Mathematical Logic III, Zapiski Nauchnykh Seminarov LOMI 105, Nauka, Leningrad, 1981 pp. 174\u2013194, english translation in Journal of Soviet Mathematics, 22(3) (1983), 1387\u20131400.","DOI":"10.1007\/BF01084396"},{"key":"10.1016\/S1571-0661(04)80760-6_NEWBIB21","article-title":"Termination of rewriting in the calculus of constructions","volume":"1443","author":"Walukiewicz","year":"1998","journal-title":"Lecture Notes in Computer Science"},{"key":"10.1016\/S1571-0661(04)80760-6_NEWBIB22","unstructured":"Werner B., M\u00e9ta-th\u00e9orie du Calcul des Constructions Inductives, Th\u00e8se Univ. Paris VII, France (1994)."}],"container-title":["Electronic Notes in Theoretical Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S1571066104807606?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S1571066104807606?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2019,2,3]],"date-time":"2019-02-03T05:53:10Z","timestamp":1549173190000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/S1571066104807606"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2003,9]]},"references-count":22,"journal-issue":{"issue":"7","published-print":{"date-parts":[[2003,9]]}},"alternative-id":["S1571066104807606"],"URL":"https:\/\/doi.org\/10.1016\/s1571-0661(04)80760-6","relation":{},"ISSN":["1571-0661"],"issn-type":[{"value":"1571-0661","type":"print"}],"subject":[],"published":{"date-parts":[[2003,9]]}}}