{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T20:05:28Z","timestamp":1725566728718},"publisher-location":"Berlin, Heidelberg","reference-count":30,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540282310"},{"type":"electronic","value":"9783540318972"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2005]]},"DOI":"10.1007\/11538363_11","type":"book-chapter","created":{"date-parts":[[2005,9,27]],"date-time":"2005-09-27T13:35:33Z","timestamp":1127828133000},"page":"135-150","source":"Crossref","is-referenced-by-count":13,"title":["Decidability of Type-Checking in the Calculus of Algebraic Constructions with Size Annotations"],"prefix":"10.1007","author":[{"given":"Fr\u00e9d\u00e9ric","family":"Blanqui","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"issue":"4","key":"11_CR1","doi-asserted-by":"publisher","first-page":"277","DOI":"10.1051\/ita:2004015","volume":"38","author":"A. Abel","year":"2004","unstructured":"Abel, A.: Termination checking with types. Theoretical Informatics and Applications\u00a038(4), 277\u2013319 (2004)","journal-title":"Theoretical Informatics and Applications"},{"key":"11_CR2","volume-title":"Handbook of logic in computer science","author":"H. Barendregt","year":"1992","unstructured":"Barendregt, H.: Lambda calculi with types. In: Abramsky, S., Gabbay, D., Maibaum, T. (eds.) Handbook of logic in computer science, vol.\u00a02, Oxford University Press, Oxford (1992)"},{"issue":"1","key":"11_CR3","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":"11_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"71","DOI":"10.1007\/11417170_7","volume-title":"Typed Lambda Calculi and Applications","author":"G. Barthe","year":"2005","unstructured":"Barthe, G., Gr\u00e9goire, B., Pastawski, F.: Practical inference for type-based termination in a polymorphic setting. In: Urzyczyn, P. (ed.) TLCA 2005. LNCS, vol.\u00a03461, pp. 71\u201385. Springer, Heidelberg (2005)"},{"key":"11_CR5","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":"11_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"24","DOI":"10.1007\/978-3-540-25979-4_2","volume-title":"Rewriting Techniques and Applications","author":"F. Blanqui","year":"2004","unstructured":"Blanqui, F.: A type-based termination criterion for dependently-typed higher-order rewrite systems. In: van Oostrom, V. (ed.) RTA 2004. LNCS, vol.\u00a03091, pp. 24\u201339. Springer, Heidelberg (2004)"},{"key":"11_CR7","unstructured":"Blanqui,F.: Full version of [6], See \n                    \n                      http:\/\/www.loria.fr\/~blanqui\/"},{"issue":"1","key":"11_CR8","doi-asserted-by":"publisher","first-page":"37","DOI":"10.1017\/S0960129504004426","volume":"15","author":"F. Blanqui","year":"2005","unstructured":"Blanqui, F.: Definitions by rewriting in the Calculus of Constructions. Mathematical Structures in Computer Science\u00a015(1), 37\u201392 (2005)","journal-title":"Mathematical Structures in Computer Science"},{"key":"11_CR9","unstructured":"Blanqui, F.: Full version, See \n                    \n                      http:\/\/www.loria.fr\/~blanqui\/"},{"issue":"1-2","key":"11_CR10","first-page":"61","volume":"65","author":"F. Blanqui","year":"2005","unstructured":"Blanqui, F.: Inductive types in the Calculus of Algebraic Constructions. Fundamenta Informaticae\u00a065(1-2), 61\u201386 (2005)","journal-title":"Fundamenta Informaticae"},{"key":"11_CR11","unstructured":"Breazu-Tannen, V.: Combining algebra and higher-order types. In: Proc. of LICS 1988 (1998)"},{"key":"11_CR12","unstructured":"Chen, G.: Subtyping, Type Conversion and Transitivity Elimination. PhD thesis, Universit\u00e9 Paris VII, France (1998)"},{"issue":"2-3","key":"11_CR13","doi-asserted-by":"publisher","first-page":"261","DOI":"10.1023\/A:1012996816178","volume":"14","author":"W.N. Chin","year":"2001","unstructured":"Chin, W.N., Khoo, S.C.: Calculating sized types. Journal of Higher-Order and Symbolic Computation\u00a014(2-3), 261\u2013300 (2001)","journal-title":"Journal of Higher-Order and Symbolic Computation"},{"key":"11_CR14","unstructured":"Coq-Development-Team. The Coq Proof Assistant Reference Manual - Version 8.0. INRIA Rocquencourt, France (2004) \n                    \n                      http:\/\/coq.inria.fr\/"},{"key":"11_CR15","doi-asserted-by":"publisher","first-page":"255","DOI":"10.1017\/CBO9780511569807.011","volume-title":"Logical Frameworks","author":"T. Coquand","year":"1991","unstructured":"Coquand, T.: An algorithm for testing conversion in type theory. In: Huet, G., Plotkin, G. (eds.) Logical Frameworks, pp. 255\u2013279. Cambridge University Press, Cambridge (1991)"},{"issue":"2-3","key":"11_CR16","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-3), 95\u2013120 (1988)","journal-title":"Information and Computation"},{"key":"11_CR17","series-title":"Lecture Notes in Computer Science","volume-title":"COLOG-88","author":"T. Coquand","year":"1990","unstructured":"Coquand, T., Paulin-Mohring, C.: Inductively defined types. In: Martin-L\u00f6f, P., Mints, G. (eds.) COLOG 1988. LNCS, vol.\u00a0417, Springer, Heidelberg (1990)"},{"key":"11_CR18","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":"11_CR19","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":"11_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 (1996)","DOI":"10.1145\/237721.240882"},{"key":"11_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"},{"issue":"6","key":"11_CR22","doi-asserted-by":"publisher","first-page":"1000","DOI":"10.1137\/0219068","volume":"19","author":"G. Lueker","year":"1990","unstructured":"Lueker, G., Megiddo, N., Ramachandran, V.: Linear programming with two variables per inequality in poly-log time. SIAM Journal on Computing\u00a019(6), 1000\u20131010 (1990)","journal-title":"SIAM Journal on Computing"},{"issue":"6","key":"11_CR23","doi-asserted-by":"publisher","first-page":"293","DOI":"10.1016\/0020-0190(92)90155-O","volume":"41","author":"F. M\u00fcller","year":"1992","unstructured":"M\u00fcller, F.: Confluence of the lambda calculus with left-linear algebraic rewriting. Information Processing Letters\u00a041(6), 293\u2013299 (1992)","journal-title":"Information Processing Letters"},{"issue":"1","key":"11_CR24","doi-asserted-by":"publisher","first-page":"35","DOI":"10.1002\/(SICI)1096-9942(199901\/03)5:1<35::AID-TAPO4>3.0.CO;2-4","volume":"5","author":"M. Odersky","year":"1999","unstructured":"Odersky, M., Sulzmann, M., Wehr, M.: Type inference with constrained types. Theory and Practice of Object Systems\u00a05(1), 35\u201355 (1999)","journal-title":"Theory and Practice of Object Systems"},{"key":"11_CR25","unstructured":"Pratt, V.: Two easy theories whose combination is hard. Technical report, MIT, United States (1977)"},{"key":"11_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"248","DOI":"10.1007\/3-540-44716-4_16","volume-title":"Functional and Logic Programming","author":"M. Sulzmann","year":"2001","unstructured":"Sulzmann, M.: A general type inference framework for Hindley\/Milner style systems. In: Kuchen, H., Ueda, K. (eds.) FLOPS 2001. LNCS, vol.\u00a02024, p. 248. Springer, Heidelberg (2001)"},{"issue":"2","key":"11_CR27","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"},{"key":"11_CR28","unstructured":"Xi, H.: Dependent types in practical programming. PhD thesis, Carnegie-Mellon, Pittsburgh, United States (1998)"},{"issue":"1","key":"11_CR29","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"},{"issue":"1-2","key":"11_CR30","doi-asserted-by":"publisher","first-page":"147","DOI":"10.1016\/S0304-3975(97)00062-5","volume":"187","author":"C. Zenger","year":"1997","unstructured":"Zenger, C.: Indexed types. Theoretical Computer Science\u00a0187(1-2), 147\u2013165 (1997)","journal-title":"Theoretical Computer Science"}],"container-title":["Lecture Notes in Computer Science","Computer Science Logic"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/11538363_11.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,27]],"date-time":"2021-04-27T06:54:12Z","timestamp":1619506452000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/11538363_11"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2005]]},"ISBN":["9783540282310","9783540318972"],"references-count":30,"URL":"https:\/\/doi.org\/10.1007\/11538363_11","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2005]]}}}