{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T20:27:36Z","timestamp":1725481656618},"publisher-location":"Berlin, Heidelberg","reference-count":25,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540402541"},{"type":"electronic","value":"9783540448815"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2003]]},"DOI":"10.1007\/3-540-44881-0_28","type":"book-chapter","created":{"date-parts":[[2007,3,5]],"date-time":"2007-03-05T16:39:56Z","timestamp":1173112796000},"page":"395-409","source":"Crossref","is-referenced-by-count":6,"title":["Rewriting Modulo in Deduction Modulo"],"prefix":"10.1007","author":[{"given":"Fr\u00e9d\u00e9ric","family":"Blanqui","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2003,6,18]]},"reference":[{"key":"28_CR1","doi-asserted-by":"crossref","unstructured":"H. Barendregt. Lambda calculi with types. In S. Abramski, D. Gabbay, and T. Maibaum, editors, Handbook of logic in computer science, volume 2. Oxford University Press, 1992.","DOI":"10.1093\/oso\/9780198537618.003.0002"},{"key":"28_CR2","volume-title":"Th\u00e9orie des Types et R\u00e9criture","author":"F. Blanqui","year":"2001","unstructured":"F. Blanqui. Th\u00e9orie des Types et R\u00e9criture. PhD thesis, Universit\u00e9 Paris XI, Orsay, France, 2001. Available in english as \u201cType Theory and Rewriting\u201d."},{"key":"28_CR3","unstructured":"F. Blanqui. Definitions by rewriting in the Calculus of Constructions (extended abstract). In Proc. of LICS\u201901."},{"key":"28_CR4","unstructured":"F. Blanqui. Definitions by rewriting in the Calculus of Constructions, 2002. Journal submission, 68 pages."},{"key":"28_CR5","doi-asserted-by":"publisher","first-page":"41","DOI":"10.1016\/S0304-3975(00)00347-9","volume":"272","author":"F. Blanqui","year":"2002","unstructured":"F. Blanqui, J.-P. Jouannaud, and M. Okada. Inductive-data-type Systems. Theoretical Computer Science, 272:41\u201368, 2002.","journal-title":"Theoretical Computer Science"},{"key":"28_CR6","unstructured":"F. Blanqui. A short and flexible strong normalization proof for the Calculus of Algebraic Constructions with curried rewriting, 2003. Draft."},{"key":"28_CR7","series-title":"Lect Notes Comput Sci","volume-title":"Proc. of ICALP\u201989","author":"V. Breazu-Tannen","year":"1989","unstructured":"V. Breazu-Tannen and J. Gallier. Polymorphic rewriting conserves algebraic strong normalization. In Proc. of ICALP\u201989, LNCS 372."},{"key":"28_CR8","unstructured":"E. Contejean, C. March\u00e9, B. Monate, and X. Urbain. CiME, 2000."},{"issue":"2\u20133","key":"28_CR9","doi-asserted-by":"publisher","first-page":"95","DOI":"10.1016\/0890-5401(88)90005-3","volume":"76","author":"T. Coquand","year":"1988","unstructured":"T. Coquand and G. Huet. The Calculus of Constructions. Information and Computation, 76(2\u20133):95\u2013120, 1988.","journal-title":"Information and Computation"},{"key":"28_CR10","doi-asserted-by":"crossref","unstructured":"T. Coquand. An algorithm for testing conversion in type theory. In G. Huet, G. Plotkin, editors, Logical Frameworks, p. 255\u2013279. Cambridge Univ. Press, 1991.","DOI":"10.1017\/CBO9780511569807.011"},{"key":"28_CR11","doi-asserted-by":"crossref","unstructured":"N. Dershowitz and J.-P. Jouannaud. Rewrite systems. In J. van Leeuwen, editor, Handbook of Theoretical Computer Science, vol. B, chap. 6. North-Holland, 1990.","DOI":"10.1016\/B978-0-444-88074-1.50011-1"},{"issue":"2","key":"28_CR12","doi-asserted-by":"publisher","first-page":"251","DOI":"10.1016\/0890-5401(92)90064-M","volume":"101","author":"D. Dougherty","year":"1992","unstructured":"D. Dougherty. Adding algebraic rewriting to the untyped lambda calculus. Information and Computation, 101(2):251\u2013267, 1992.","journal-title":"Information and Computation"},{"key":"28_CR13","series-title":"Technical Report","volume-title":"Theorem proving modulo","author":"G. Dowek","year":"1998","unstructured":"G. Dowek, T. Hardin, and C. Kirchner. Theorem proving modulo. Technical Report 3400, INRIA Rocquencourt, France, 1998."},{"key":"28_CR14","unstructured":"J.-Y. Girard, Y. Lafont and P. Taylor. Proofs and Types. Cambridge University Press, 1988."},{"issue":"4","key":"28_CR15","doi-asserted-by":"publisher","first-page":"797","DOI":"10.1145\/322217.322230","volume":"27","author":"G. Huet","year":"1980","unstructured":"G. Huet. Confluent reductions: Abstract properties and applications to term-rewriting systems. Journal of the ACM, 27(4):797\u2013821, 1980.","journal-title":"Journal of the ACM"},{"issue":"4","key":"28_CR16","doi-asserted-by":"publisher","first-page":"1155","DOI":"10.1137\/0215084","volume":"15","author":"J.-P. Jouannaud","year":"1986","unstructured":"J.-P. Jouannaud and H. Kirchner. Completion of a set of rules modulo a set of equations. SIAM Journal on Computing, 15(4):1155\u20131194, 1986.","journal-title":"SIAM Journal on Computing"},{"key":"28_CR17","doi-asserted-by":"crossref","unstructured":"J.-P. Jouannaud and A. Rubio. The Higher-Order Recursive Path Ordering. In Proc. of LICS\u201999.","DOI":"10.1109\/LICS.1999.782635"},{"key":"28_CR18","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1016\/0304-3975(93)90091-7","volume":"121","author":"J. W. Klop","year":"1993","unstructured":"J. W. Klop, V. van Oostrom, F. van Raamsdonk. Combinatory reduction systems: introduction and survey. Theoretical Computer Science, 121:279\u2013308, 1993.","journal-title":"Theoretical Computer Science"},{"key":"28_CR19","doi-asserted-by":"crossref","unstructured":"C. March\u00e9. Normalised rewriting and normalised completion. In Proc. of LICS\u201994.","DOI":"10.1109\/LICS.1994.316050"},{"key":"28_CR20","unstructured":"M. Okada. Strong normalizability for the combined system of the typed lambda calculus and an arbitrary convergent term rewrite system. In Proc. of ISSAC\u201989."},{"issue":"2","key":"28_CR21","doi-asserted-by":"publisher","first-page":"65","DOI":"10.1016\/0020-0190(87)90039-1","volume":"26","author":"M. Rusinowitch","year":"1987","unstructured":"M. Rusinowitch. On termination of the direct sum of term-rewriting systems. Information Processing Letters, 26(2):65\u201370, 1987.","journal-title":"Information Processing Letters"},{"key":"28_CR22","volume-title":"The Coq Proof Assistant Reference Manual \u2014 Version 7.4","author":"Coq Development Team.","year":"2003","unstructured":"Coq Development Team. The Coq Proof Assistant Reference Manual \u2014 Version 7.4. INRIA Rocquencourt, France, 2003. http:\/\/coq.inria.fr\/ ."},{"issue":"3","key":"28_CR23","doi-asserted-by":"publisher","first-page":"141","DOI":"10.1016\/0020-0190(87)90122-0","volume":"25","author":"Y. Toyama","year":"1987","unstructured":"Y. Toyama. Counterexamples to termination for the direct sum of term rewriting systems. Information Processing Letters, 25(3):141\u2013143, 1987.","journal-title":"Information Processing Letters"},{"key":"28_CR24","series-title":"Lect Notes Comput Sci","volume-title":"Proc. of LFCS\u201994","author":"V. Oostrom van","year":"1994","unstructured":"V. van Oostrom and F. van Raamsdonk. Weak orthogonality implies confluence: the higher-order case. In Proc. of LFCS\u201994, LNCS 813."},{"key":"28_CR25","doi-asserted-by":"crossref","unstructured":"D. Walukiewicz-Chrz\u0105szcz. Termination of rewriting in the Calculus of Constructions. Journal of Functional Programming, ?(?):?-?, 2002.","DOI":"10.1017\/S0956796802004641"}],"container-title":["Lecture Notes in Computer Science","Rewriting Techniques and Applications"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-44881-0_28","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,2,11]],"date-time":"2024-02-11T12:48:20Z","timestamp":1707655700000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-44881-0_28"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2003]]},"ISBN":["9783540402541","9783540448815"],"references-count":25,"URL":"https:\/\/doi.org\/10.1007\/3-540-44881-0_28","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2003]]}}}