{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T19:43:25Z","timestamp":1725565405588},"publisher-location":"Berlin, Heidelberg","reference-count":26,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540221531"},{"type":"electronic","value":"9783540259794"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2004]]},"DOI":"10.1007\/978-3-540-25979-4_2","type":"book-chapter","created":{"date-parts":[[2010,9,11]],"date-time":"2010-09-11T01:32:53Z","timestamp":1284168773000},"page":"24-39","source":"Crossref","is-referenced-by-count":27,"title":["A Type-Based Termination Criterion for Dependently-Typed Higher-Order Rewrite Systems"],"prefix":"10.1007","author":[{"given":"Fr\u00e9d\u00e9ric","family":"Blanqui","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"2_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/3-540-44904-3_1","volume-title":"Typed Lambda Calculi and Applications","author":"A. Abel","year":"2003","unstructured":"Abel, A.: Termination and productivity checking with continuous types. In: Hofmann, M.O. (ed.) TLCA 2003. LNCS, vol.\u00a02701, pp. 1\u201315. Springer, Heidelberg (2003)"},{"key":"2_CR2","unstructured":"Abel, A.: Termination checking with types. Technical Report 0201, Ludwig Maximilians Universit\u00e4t, M\u00fcnchen, Germany (2002)"},{"key":"2_CR3","unstructured":"Abel, A.: Termination checking with types (2003) (Submitted to ITA)"},{"key":"2_CR4","volume-title":"Handbook of logic in computer science","author":"H. Barendregt","year":"1992","unstructured":"Barendregt, H.: Lambda calculi with types. In: Abramski, S., Gabbay, D., Maibaum, T. (eds.) Handbook of logic in computer science, vol.\u00a02, Oxford University Press, Oxford (1992)"},{"issue":"1","key":"2_CR5","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. Mathematical Structures in Computer Science\u00a014(1), 97\u2013141 (2004)","journal-title":"Mathematical Structures in Computer Science"},{"key":"2_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"46","DOI":"10.1007\/3-540-44904-3_4","volume-title":"Typed Lambda Calculi and Applications","author":"F. Blanqui","year":"2003","unstructured":"Blanqui, F.: Inductive types in the Calculus of Algebraic Constructions. In: Hofmann, M.O. (ed.) TLCA 2003. LNCS, vol.\u00a02701, pp. 46\u201359. Springer, Heidelberg (2003)"},{"key":"2_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-44881-0_28","volume-title":"Rewriting Techniques and Applications","author":"F. Blanqui","year":"2003","unstructured":"Blanqui, F.: Rewriting modulo in Deduction modulo. In: Nieuwenhuis, R. (ed.) RTA 2003. LNCS, vol.\u00a02706, Springer, Heidelberg (2003)"},{"key":"2_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/10721975_4","volume-title":"Rewriting Techniques and Applications","author":"F. Blanqui","year":"2000","unstructured":"Blanqui, F.: Termination and confluence of higher-order rewrite systems. In: Bachmair, L. (ed.) RTA 2000. LNCS, vol.\u00a01833, Springer, Heidelberg (2000)"},{"key":"2_CR9","unstructured":"Blanqui, F.: A type-based termination criterion for dependently-typed higher-order rewrite systems. Draft. 38 pages, \n                  \n                    http:\/\/www.loria.fr\/~blanqui\/"},{"key":"2_CR10","unstructured":"Blanqui, F.: Definitions by rewriting in the Calculus of Constructions. To appear in Mathematical Structures in Computer Science (2003)"},{"key":"2_CR11","doi-asserted-by":"publisher","first-page":"41","DOI":"10.1016\/S0304-3975(00)00347-9","volume":"272","author":"F. Blanqui","year":"2002","unstructured":"Blanqui, F., Jouannaud, J.-P., Okada, M.: Inductive-data-type Systems. Theoretical Computer Science\u00a0272, 41\u201368 (2002)","journal-title":"Theoretical Computer Science"},{"key":"2_CR12","unstructured":"Chen, G.: Subtyping, Type Conversion and Transitivity Elimination. PhD thesis, Universit\u00e9 Paris VII, France (1998)"},{"issue":"2\u20133","key":"2_CR13","doi-asserted-by":"publisher","first-page":"95","DOI":"10.1016\/0890-5401(88)90005-3","volume":"76","author":"T. Coquand","year":"1988","unstructured":"Coquand, T., Huet, G.: The Calculus of Constructions. Information and Computation\u00a076(2\u20133), 95\u2013120 (1988)","journal-title":"Information and Computation"},{"issue":"2","key":"2_CR14","doi-asserted-by":"publisher","first-page":"179","DOI":"10.1016\/0304-3975(94)00275-4","volume":"142","author":"N. Dershowitz","year":"1995","unstructured":"Dershowitz, N., Hoot, C.: Natural termination. Theoretical Computer Science\u00a0142(2), 179\u2013207 (1995)","journal-title":"Theoretical Computer Science"},{"key":"2_CR15","volume-title":"Handbook of Theoretical Computer Science","author":"N. Dershowitz","year":"1990","unstructured":"Dershowitz, N., Jouannaud, J.-P.: Rewrite systems. In: van Leeuwen, J. (ed.) Handbook of Theoretical Computer Science, vol.\u00a0B, ch. 6, North-Holland, Amsterdam (1990)"},{"key":"2_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"62","DOI":"10.1007\/3-540-48167-2_5","volume-title":"Types for Proofs and Programs","author":"G. Dowek","year":"1999","unstructured":"Dowek, G., Werner, B.: Proof normalization modulo. In: Altenkirch, T., Naraschewski, W., Reus, B. (eds.) TYPES 1998. LNCS, vol.\u00a01657, p. 62. Springer, Heidelberg (1999)"},{"issue":"1","key":"2_CR17","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1023\/A:1005797629953","volume":"19","author":"J. Giesl","year":"1997","unstructured":"Giesl, J.: Termination of nested and mutually recursive algorithms. Journal of Automated Reasoning\u00a019(1), 1\u201329 (1997)","journal-title":"Journal of Automated Reasoning"},{"key":"2_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"397","DOI":"10.1007\/BFb0055070","volume-title":"Automata, Languages and Programming","author":"E. Gim\u00e9nez","year":"1998","unstructured":"Gim\u00e9nez, E.: Structural recursive definitions in type theory. In: Larsen, K.G., Skyum, S., Winskel, G. (eds.) ICALP 1998. LNCS, vol.\u00a01443, p. 397. Springer, Heidelberg (1998)"},{"key":"2_CR19","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/S0020-0190(99)00036-8","volume":"70","author":"R. Harper","year":"1999","unstructured":"Harper, R., Mitchell, J.: Parametricity and variants of Girard\u2019s J operator. Information Processing Letters\u00a070, 1\u20135 (1999)","journal-title":"Information Processing Letters"},{"key":"2_CR20","doi-asserted-by":"crossref","unstructured":"Hughes, J., Pareto, L., Sabry, A.: Proving the correctness of reactive systems using sized types. In: Proc. of POPL (1996)","DOI":"10.1145\/237721.240882"},{"key":"2_CR21","doi-asserted-by":"crossref","unstructured":"Jouannaud, J.-P., Rubio, A.: The Higher-Order Recursive Path Ordering. In: Proc. of LICS 1999 (1999)","DOI":"10.1109\/LICS.1999.782635"},{"key":"2_CR22","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1016\/0304-3975(93)90091-7","volume":"121","author":"J.W. Klop","year":"1993","unstructured":"Klop, J.W., van Oostrom, V., van Raamsdonk, F.: Combinatory reduction systems: introduction and survey. Theoretical Comp. Science\u00a0121, 279\u2013308 (1993)","journal-title":"Theoretical Comp. Science"},{"key":"2_CR23","unstructured":"Mendler, N.P.: Inductive Definition in Type Theory. PhD thesis, Cornell University, United States (1987)"},{"key":"2_CR24","unstructured":"Stefanova, M.: Properties of Typing Systems. PhD thesis, Katholiecke Universiteit Nijmegen, The Netherlands (1998)"},{"issue":"2","key":"2_CR25","doi-asserted-by":"crossref","first-page":"339","DOI":"10.1017\/S0956796802004641","volume":"13","author":"D. Walukiewicz-Chrz\u0105szcz","year":"2003","unstructured":"Walukiewicz-Chrz\u0105szcz, D.: Termination of rewriting in the Calculus of Constructions. Journal of Functional Programming\u00a013(2), 339\u2013414 (2003)","journal-title":"Journal of Functional Programming"},{"issue":"1","key":"2_CR26","doi-asserted-by":"publisher","first-page":"91","DOI":"10.1023\/A:1019916231463","volume":"15","author":"H. Xi","year":"2002","unstructured":"Xi, H.: Dependent types for program termination verification. Journal of Higher- Order and Symbolic Computation\u00a015(1), 91\u2013131 (2002)","journal-title":"Journal of Higher- Order and Symbolic Computation"}],"container-title":["Lecture Notes in Computer Science","Rewriting Techniques and Applications"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-25979-4_2","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,3,20]],"date-time":"2019-03-20T09:50:20Z","timestamp":1553075420000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-25979-4_2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2004]]},"ISBN":["9783540221531","9783540259794"],"references-count":26,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-25979-4_2","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2004]]}}}