{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T17:47:12Z","timestamp":1725472032390},"publisher-location":"Berlin, Heidelberg","reference-count":22,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540482819"},{"type":"electronic","value":"9783540482826"}],"license":[{"start":{"date-parts":[[2006,1,1]],"date-time":"2006-01-01T00:00:00Z","timestamp":1136073600000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2006]]},"DOI":"10.1007\/11916277_8","type":"book-chapter","created":{"date-parts":[[2006,10,17]],"date-time":"2006-10-17T14:32:59Z","timestamp":1161095579000},"page":"105-119","source":"Crossref","is-referenced-by-count":7,"title":["Combining Typing and Size Constraints for Checking the Termination of Higher-Order Conditional Rewrite Systems"],"prefix":"10.1007","author":[{"given":"Fr\u00e9d\u00e9ric Blanqui","family":"(INRIA)","sequence":"first","affiliation":[]},{"given":"Colin Riba","family":"(INPL)","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"8_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)"},{"issue":"4","key":"8_CR2","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"},{"issue":"1","key":"8_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":"8_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":"8_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"135","DOI":"10.1007\/11538363_11","volume-title":"Computer Science Logic","author":"F. Blanqui","year":"2005","unstructured":"Blanqui, F.: Decidability of Type-Checking in the Calculus of Algebraic Constructions with Size Annotations. In: Ong, L. (ed.) CSL 2005. LNCS, vol.\u00a03634, pp. 135\u2013150. Springer, Heidelberg (2005)"},{"key":"8_CR6","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":"8_CR7","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":"8_CR8","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)"},{"issue":"1","key":"8_CR9","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":"8_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"382","DOI":"10.1007\/11690634_26","volume-title":"Foundations of Software Science and Computation Structures","author":"F. Blanqui","year":"2006","unstructured":"Blanqui, F., Kirchner, C., Riba, C.: On the confluence of \u03bb-calculus with conditional rewriting. In: Aceto, L., Ing\u00f3lfsd\u00f3ttir, A. (eds.) FOSSACS 2006. LNCS, vol.\u00a03921, pp. 382\u2013397. Springer, Heidelberg (2006)"},{"issue":"2-3","key":"8_CR11","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":"8_CR12","doi-asserted-by":"crossref","unstructured":"Davies, R., Pfenning, F.: Intersection types and computational effects. In: Proc. of ICFP 2000, SIGPLAN Notices 35(9) (2000)","DOI":"10.1145\/357766.351259"},{"key":"8_CR13","unstructured":"Fischer, M., Rabin, M.: Super-exponential complexity of presburger arithmetic. In: Proceedings of the SIAM-AMS Symposium in Applied Mathematics (1974)"},{"key":"8_CR14","volume-title":"Logic and Computer Science","author":"J. Gallier","year":"1990","unstructured":"Gallier, J.: On Girard\u2019s \u201cCandidats de R\u00e9ductibilit\u00e9\u201d. In: Odifreddi, P.-G. (ed.) Logic and Computer Science. North-Holland, Amsterdam (1990)"},{"key":"8_CR15","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":"8_CR16","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. Theoretical Computer Science\u00a0121, 279\u2013308 (1993)","journal-title":"Theoretical Computer Science"},{"issue":"2","key":"8_CR17","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1016\/S0304-3975(97)00143-6","volume":"192","author":"R. Mayr","year":"1998","unstructured":"Mayr, R., Nipkow, T.: Higher-order rewrite systems and their confluence. Theoretical Computer Science\u00a0192(2), 3\u201329 (1998)","journal-title":"Theoretical Computer Science"},{"key":"8_CR18","unstructured":"Presburger, M.: ber die vollst\u00a0ndigkeit eines gewissen systems der arithmetik ganzer zahlen, in welchem die addition als einzige operation hervortritt. In: Sprawozdanie z I Kongresu Matematykow Krajow Slowcanskich, Warszawa, Poland (1929)"},{"key":"8_CR19","doi-asserted-by":"crossref","unstructured":"Tait, W.W.: A realizability interpretation of the theory of species. In: Parikh, R. (ed.) AUSCRYPT 1990. Lecture Notes in Mathematics, vol.\u00a0453 (1975)","DOI":"10.1007\/BFb0064875"},{"key":"8_CR20","series-title":"Lecture Notes in Computer Science","volume-title":"Higher-Order Algebra, Logic, and Term Rewriting","author":"V. Oostrom van","year":"1994","unstructured":"van Oostrom, V., van Raamsdonk, F.: Comparing Combinatory Reduction Systems and Higher-order Rewrite Systems. In: Heering, J., Meinke, K., M\u00f6ller, B., Nipkow, T. (eds.) HOA 1993. LNCS, vol.\u00a0816, Springer, Heidelberg (1994)"},{"key":"8_CR21","unstructured":"Xi, H.: Dependent types in practical programming. PhD thesis, Carnegie-Mellon, Pittsburgh, United States (1998)"},{"issue":"1","key":"8_CR22","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","Logic for Programming, Artificial Intelligence, and Reasoning"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/11916277_8","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,19]],"date-time":"2019-05-19T13:05:10Z","timestamp":1558271110000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/11916277_8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2006]]},"ISBN":["9783540482819","9783540482826"],"references-count":22,"URL":"https:\/\/doi.org\/10.1007\/11916277_8","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2006]]}}}