{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T13:20:57Z","timestamp":1725456057446},"publisher-location":"Berlin, Heidelberg","reference-count":15,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540590484"},{"type":"electronic","value":"9783540491781"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1995]]},"DOI":"10.1007\/bfb0014061","type":"book-chapter","created":{"date-parts":[[2005,11,23]],"date-time":"2005-11-23T02:50:31Z","timestamp":1132714231000},"page":"312-327","source":"Crossref","is-referenced-by-count":4,"title":["Termination proof of term rewriting system with the multiset path ordering. A complete development in the system Coq"],"prefix":"10.1007","author":[{"given":"Fran\u00e7ois","family":"Leclerc","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,6,9]]},"reference":[{"key":"21_CR1","unstructured":"E. A. Cichon. Bounds on derivation lenghts from termination proofs. Technical Report CSD-TR-622, Royal Holloway and Bedford New College, 1990."},{"key":"21_CR2","doi-asserted-by":"crossref","unstructured":"E. A. Cichon and P. Lescanne. Polynomial interpretations and the complexity of algorithms. In D. Kapur, editor, Proceedings 11th International Conference on Automated Deduction, Saratoga Springs (N. Y., USA), volume 607 of Lecture Notes in Computer Science, pages 139\u2013147. Springer-Verlag, June 1992.","DOI":"10.1007\/3-540-55602-8_161"},{"key":"21_CR3","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1016\/0304-3975(82)90026-3","volume":"17","author":"N. Dershowitz","year":"1982","unstructured":"N. Dershowitz. Orderings for term-rewriting systems. Theoretical Computer Science, 17:279\u2013301, 1982.","journal-title":"Theoretical Computer Science"},{"key":"21_CR4","unstructured":"G. Dowek, A. Felty, H. Herbelin, G. Huet, C. Paulin-Mohring, and B. Werner. The Coq Proof Assistant. User's guide, INRIA-CNRS-ENS, 1991."},{"key":"21_CR5","doi-asserted-by":"crossref","unstructured":"N. Dershowitz and M. Okada. Proof-theoretic techniques and the theory of rewriting. In Proceedings 3rd IEEE Symposium on Logic in Computer Science, Edinburgh (UK), pages 104\u201311. IEEE, 1988.","DOI":"10.1109\/LICS.1988.5108"},{"issue":"3","key":"21_CR6","doi-asserted-by":"publisher","first-page":"199","DOI":"10.1016\/0168-0072(91)90022-E","volume":"53","author":"J. Gallier","year":"1991","unstructured":"J. Gallier. What's so special about Kruskal's theorem and the ordinal \u0393 0? A survey of some results in proof theory. Annals of Pure and Applied Logic, 53(3):199\u2013261, September 1991.","journal-title":"Annals of Pure and Applied Logic"},{"key":"21_CR7","doi-asserted-by":"crossref","unstructured":"D. Hofbauer. Termination proofs by multiset path orderings imply primitive recursive derivation lenghts. In H\u00e9l\u00e8ne Kirchner and W. Wechler, editors, Proceedings 2nd International Conference on Algebraic and Logic Programming, Nancy (France), volume 463 of Lecture Notes in Computer Science, pages 347\u2013358, 1990.","DOI":"10.1007\/3-540-53162-9_50"},{"issue":"36","key":"21_CR8","first-page":"129","volume":"1","author":"C. Lautemann","year":"1988","unstructured":"C. Lautemann. A note on polynomial interpretation. Bulletin of European Association for Theoretical Computer Science, 1(36):129\u2013131, October 1988.","journal-title":"Bulletin of European Association for Theoretical Computer Science"},{"key":"21_CR9","doi-asserted-by":"publisher","first-page":"39","DOI":"10.1007\/BF00302640","volume":"6","author":"P. Lescanne","year":"1990","unstructured":"P. Lescanne. On the recursive decomposition ordering with lexicographical status and other related orderings. Journal of Automated Reasoning, 6:39\u201349, 1990.","journal-title":"Journal of Automated Reasoning"},{"key":"21_CR10","doi-asserted-by":"crossref","unstructured":"Catherine Parent. Developing certified programs in the system coq-the program tactic. RR 93-29, ENS, October 1993.","DOI":"10.1007\/3-540-58085-9_81"},{"key":"21_CR11","unstructured":"C. Paulin-Mohring. Inductive Definitions in the System Coq \u2014 Rules and Properties. In Proceedings of the conference Typed Lambda Calculus and Applications, Lecture Notes in Computer Science. Springer-Verlag, 1993."},{"key":"21_CR12","doi-asserted-by":"publisher","first-page":"49","DOI":"10.1016\/0168-0072(93)90192-G","volume":"60","author":"M. Rathjen","year":"1993","unstructured":"Rathjen, M. and Weiermann A. Proof-theoretic investigations on kruskal's theorem. Annals of pure and applied logic, 60:49\u201388, 1993.","journal-title":"Annals of pure and applied logic"},{"key":"21_CR13","unstructured":"Joseph Rouyer and Pierre Lescanne. Verification and programming of first-order unification in the calculus of constructions with inductive types, November 1992."},{"key":"21_CR14","unstructured":"Joseph Rouyer. D\u00e9veloppement de l'algorithme d'unification dans le calcul des constructions avec types inductifs. RR 1795, INRIA, November 1992."},{"key":"21_CR15","unstructured":"Andreas Weiermann. Bounds for derivation lengths from termination proofs with rpo and rlpo. Private communication, 1993."}],"container-title":["Lecture Notes in Computer Science","Typed Lambda Calculi and Applications"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BFb0014061","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,5,5]],"date-time":"2023-05-05T11:43:54Z","timestamp":1683287034000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BFb0014061"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1995]]},"ISBN":["9783540590484","9783540491781"],"references-count":15,"URL":"https:\/\/doi.org\/10.1007\/bfb0014061","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1995]]}}}