{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,7,30]],"date-time":"2025-07-30T15:36:51Z","timestamp":1753889811953,"version":"3.41.2"},"reference-count":0,"publisher":"Centre pour la Communication Scientifique Directe (CCSD)","license":[{"start":{"date-parts":[[2008,9,15]],"date-time":"2008-09-15T00:00:00Z","timestamp":1221436800000},"content-version":"unspecified","delay-in-days":0,"URL":"https:\/\/arxiv.org\/licenses\/nonexclusive-distrib\/1.0"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"abstract":"<jats:p>Adding rewriting to a proof assistant based on the Curry-Howard isomorphism,\nsuch as Coq, may greatly improve usability of the tool. Unfortunately adding an\narbitrary set of rewrite rules may render the underlying formal system\nundecidable and inconsistent. While ways to ensure termination and confluence,\nand hence decidability of type-checking, have already been studied to some\nextent, logical consistency has got little attention so far. In this paper we\nshow that consistency is a consequence of canonicity, which in turn follows\nfrom the assumption that all functions defined by rewrite rules are complete.\nWe provide a sound and terminating, but necessarily incomplete algorithm to\nverify this property. The algorithm accepts all definitions that follow\ndependent pattern matching schemes presented by Coquand and studied by McBride\nin his PhD thesis. It also accepts many definitions by rewriting, containing\nrules which depart from standard pattern matching.<\/jats:p>","DOI":"10.2168\/lmcs-4(3:8)2008","type":"journal-article","created":{"date-parts":[[2009,1,9]],"date-time":"2009-01-09T10:23:10Z","timestamp":1231496590000},"source":"Crossref","is-referenced-by-count":2,"title":["Consistency and Completeness of Rewriting in the Calculus of Constructions"],"prefix":"10.46298","volume":"Volume 4, Issue 3","author":[{"given":"Daria","family":"Walukiewicz-Chrzaszcz","sequence":"first","affiliation":[]},{"given":"Jacek","family":"Chrzaszcz","sequence":"additional","affiliation":[]}],"member":"25203","published-online":{"date-parts":[[2008,9,15]]},"container-title":["Logical Methods in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/lmcs.episciences.org\/1141\/pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/lmcs.episciences.org\/1141\/pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,4,11]],"date-time":"2023-04-11T20:04:27Z","timestamp":1681243467000},"score":1,"resource":{"primary":{"URL":"https:\/\/lmcs.episciences.org\/1141"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2008,9,15]]},"references-count":0,"URL":"https:\/\/doi.org\/10.2168\/lmcs-4(3:8)2008","relation":{"is-same-as":[{"id-type":"arxiv","id":"0806.1749","asserted-by":"subject"},{"id-type":"doi","id":"10.48550\/arXiv.0806.1749","asserted-by":"subject"}]},"ISSN":["1860-5974"],"issn-type":[{"type":"electronic","value":"1860-5974"}],"subject":[],"published":{"date-parts":[[2008,9,15]]},"article-number":"1141"}}