{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,5]],"date-time":"2025-06-05T11:47:21Z","timestamp":1749124041292},"reference-count":35,"publisher":"Elsevier BV","issue":"4","license":[{"start":{"date-parts":[[2001,11,1]],"date-time":"2001-11-01T00:00:00Z","timestamp":1004572800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/tdm\/userlicense\/1.0\/"},{"start":{"date-parts":[[2013,7,29]],"date-time":"2013-07-29T00:00:00Z","timestamp":1375056000000},"content-version":"vor","delay-in-days":4288,"URL":"http:\/\/creativecommons.org\/licenses\/by-nc-nd\/3.0\/"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Electronic Notes in Theoretical Computer Science"],"published-print":{"date-parts":[[2001,11]]},"DOI":"10.1016\/s1571-0661(04)00295-6","type":"journal-article","created":{"date-parts":[[2004,2,5]],"date-time":"2004-02-05T10:34:35Z","timestamp":1075977275000},"page":"320-340","source":"Crossref","is-referenced-by-count":4,"title":["Certifying Term Rewriting Proofs in ELAN"],"prefix":"10.1016","volume":"59","author":[{"given":"Quang-Huy","family":"Nguyen","sequence":"first","affiliation":[]}],"member":"78","reference":[{"key":"10.1016\/S1571-0661(04)00295-6_NEWBIB1","doi-asserted-by":"crossref","unstructured":"M. Abadi, L. Cardelli, P.-L. Curien, and J.-J. L\u00e9vy. Explicit substitutions. In ACM, editor, Conf. Rec. 17th Symp. POPL, pages 31\u201346, 1990.","DOI":"10.1145\/96709.96712"},{"key":"10.1016\/S1571-0661(04)00295-6_NEWBIB2","unstructured":"C. Alvarado and Q-H. Nguyen. ELAN for equational reasoning in Coq. In J. Despeyroux, editor, Proc. of 2nd Workshop on Logical Frameworks and Metalanguages. Institut National de Recherche en Informatique et en Automatique, ISBN 2-7261-1166-1, June 2000."},{"key":"10.1016\/S1571-0661(04)00295-6_NEWBIB3","unstructured":"B. Barras. Auto-validation d'un syst\u00e8me de preuves avec familles inductives. PhD thesis, Universit\u00e9 Paris VII, November 1999."},{"key":"10.1016\/S1571-0661(04)00295-6_NEWBIB4","unstructured":"E. Beffara, O. Bournez, H. Kacem, and C. Kirchner. Verification of timed automata using rewrite rules and strategies. In N. Dershowitz and A. Frank, editors, Proc. BISFAI 2001, June 2001."},{"issue":"1\u20132","key":"10.1016\/S1571-0661(04)00295-6_NEWBIB5","doi-asserted-by":"crossref","first-page":"203","DOI":"10.1016\/S0747-7171(87)80027-5","article-title":"Complexity of matching problems","volume":"3","author":"Benanav","year":"1987","journal-title":"Journal of Symbolic Computation"},{"key":"10.1016\/S1571-0661(04)00295-6_NEWBIB6","doi-asserted-by":"crossref","unstructured":"S. Berghofer and T. Nipkow. Proof terms for simply typed higher order logic. In J. Harrison and M. Aagaard, editors, Proc. 13th Int. Conf. TPHOL, volume 1869 of Lecture Notes in Computer Science, pages 38\u201352. Springer-Verlag, 2000.","DOI":"10.1007\/3-540-44659-1_3"},{"key":"10.1016\/S1571-0661(04)00295-6_NEWBIB7","doi-asserted-by":"crossref","unstructured":"M. Bezem, D. Hendriks, and H. de Nivelle. Automated proof construction in type theory using resolution. In D. McAllester, editor, Proc. 17th Int. Conf. CADE, volume 1831 of Lecture Notes in Artificial Intelligence, pages 148\u2013163. Springer-Verlag, 2000.","DOI":"10.1007\/10721959_10"},{"key":"10.1016\/S1571-0661(04)00295-6_NEWBIB8","doi-asserted-by":"crossref","unstructured":"S. Boutin. Using reflection to build efficient and certified decision procedures. In M. Abadi and T. Ito, editors, Proc. of the 3rd Int. Symp. TACS, number 1281 in Lecture Notes in Computer Science, pages 515\u2013529. Springer-Verlag, 1997.","DOI":"10.1007\/BFb0014565"},{"key":"10.1016\/S1571-0661(04)00295-6_NEWBIB9","unstructured":"H. Cirstea. Calcul de r\u00e9\u00e9criture: fondements et applications. PhD thesis, Universit\u00e9 Henri Poincar\u00e9 - Nancy I, October 2000."},{"issue":"3","key":"10.1016\/S1571-0661(04)00295-6_NEWBIB10","first-page":"427","article-title":"The rewriting calculus \u2014 Part I and II","volume":"9","author":"Cirstea","year":"2001","journal-title":"Journal of the Interest Group in Pure and Applied Logics"},{"key":"10.1016\/S1571-0661(04)00295-6_NEWBIB11","doi-asserted-by":"crossref","unstructured":"H. Cirstea, C. Kirchner, and L. Liquori. The Rho Cube. In F. Honsell, editor, Proc. of FOSSACS, volume 2030 of Lecture Notes in Computer Science, pages 166\u2013180, April 2001.","DOI":"10.1007\/3-540-45315-6_11"},{"key":"10.1016\/S1571-0661(04)00295-6_NEWBIB12","doi-asserted-by":"crossref","DOI":"10.1016\/0890-5401(88)90005-3","article-title":"The Calculus of Constructions","volume":"76","author":"Coquand","year":"1988","journal-title":"Information and Computation"},{"issue":"2","key":"10.1016\/S1571-0661(04)00295-6_NEWBIB13","doi-asserted-by":"crossref","first-page":"362","DOI":"10.1145\/226643.226675","article-title":"Confluence properties of weak and strong calculi of explicit substitutions","volume":"43","author":"Curien","year":"1996","journal-title":"Journal of the ACM"},{"key":"10.1016\/S1571-0661(04)00295-6_NEWBIB14","doi-asserted-by":"crossref","unstructured":"E. Denney. A prototype proof translator from HOL to Coq. In M. Aagaard and J. Harrison, editors, Proc. 13th Int. Conf. TPHOL, volume 1869 of Lecture Notes in Computer Science, pages 108\u2013125. Springer-Verlag, 2000.","DOI":"10.1007\/3-540-44659-1_8"},{"key":"10.1016\/S1571-0661(04)00295-6_NEWBIB15","series-title":"chapter 6: Rewrite Systems","first-page":"244","article-title":"Handbook of Theoretical Computer Science, volume B","author":"Dershowitz","year":"1990"},{"key":"10.1016\/S1571-0661(04)00295-6_NEWBIB16","unstructured":"G. Dowek, T. Hardin, and C. Kirchner. Theorem proving modulo. Rapport de Recherche 3400, Institut National de Recherche en Informatique et en Automatique, April 1998. ftp:\/\/ftp.inria.fr\/INRIA\/publication\/RR\/RR-3400.ps.gz."},{"key":"10.1016\/S1571-0661(04)00295-6_NEWBIB17","unstructured":"F. Gadducci. On the Algebraic Approach to Concurrent Term Rewriting. PhD thesis, Universit\u00e0 di Pisa, January 1996."},{"key":"10.1016\/S1571-0661(04)00295-6_NEWBIB18","series-title":"Principles and Practice of Constraint Programming","article-title":"Designing CLP using Computational Systems","author":"Kirchner","year":"1995"},{"key":"10.1016\/S1571-0661(04)00295-6_NEWBIB19","series-title":"Handbook of Logic in Computer Science, volume 2, chapter 1","first-page":"1","article-title":"Term rewriting systems","author":"Klop","year":"1992"},{"key":"10.1016\/S1571-0661(04)00295-6_NEWBIB20","unstructured":"LogiCal\/INRIA. The Coq homepage. http:\/\/coq.inria.fr."},{"key":"10.1016\/S1571-0661(04)00295-6_NEWBIB21","doi-asserted-by":"crossref","unstructured":"U. Martin and T. Nipkow. Ordered rewriting and confluence. In M.E. Stickel, editor, Proc. 10th Int. Conf. Automated Deduction, volume 449 of Lecture Notes in Computer Science, pages 366\u2013380. Springer-Verlag, 1990.","DOI":"10.1007\/3-540-52885-7_100"},{"issue":"1","key":"10.1016\/S1571-0661(04)00295-6_NEWBIB22","doi-asserted-by":"crossref","first-page":"73","DOI":"10.1016\/0304-3975(92)90182-F","article-title":"Conditional rewriting logic as a unified model of concurrency","volume":"96","author":"Meseguer","year":"1992","journal-title":"Theoretical Computer Science"},{"key":"10.1016\/S1571-0661(04)00295-6_NEWBIB23","doi-asserted-by":"crossref","unstructured":"J-Y. Moyen. System presentation: an analyser of rewriting systems complexity. In Mark van den Brand and Rakesh Verma, editors, Prceedings of the second RULE workshop, volume 59. Elsevier Science Publishers B. V. (North-Holland), 2001. In this volume.","DOI":"10.1016\/S1571-0661(04)00300-7"},{"key":"10.1016\/S1571-0661(04)00295-6_NEWBIB24","doi-asserted-by":"crossref","unstructured":"P. Naumov, M-O. Stehr, and J. Meseguer. The HOL\/NuPRL proof translator: A practical approach to formal interoperability. In R.J. Boulton and P.B. Jackson, editors, Proc. 14th Int. Conf. TPHOL, volume 2152 of Lecture Notes in Computer Science, pages 329\u2013345. Springer-Verlag, 2001.","DOI":"10.1007\/3-540-44755-5_23"},{"key":"10.1016\/S1571-0661(04)00295-6_NEWBIB25","unstructured":"University of Utrecht. The STRATEGO homepage. http:\/\/www.stratego-language.org."},{"key":"10.1016\/S1571-0661(04)00295-6_NEWBIB26","doi-asserted-by":"crossref","unstructured":"C. Paulin-Mohring. Extracting \u03c9's programs from proofs in the calculus of constructions. In ACM, editor, Proc. 16th Symp. POPL, January 11\u201313, 1989, Austin, TX, pages 89\u2013104. ACM Press, 1989.","DOI":"10.1145\/75277.75285"},{"key":"10.1016\/S1571-0661(04)00295-6_NEWBIB27","doi-asserted-by":"crossref","unstructured":"C. Paulin-Mohring. Inductive definitions in the system Coq: Rules and properties. In M. Bezem and J. F. Groote, editors, Proc. of the 1st Int. Conf. TLCA, volume 664 of Lecture Notes in Computer Science, pages 328\u2013345, Berlin, 1993. Springer-Verlag.","DOI":"10.1007\/BFb0037116"},{"key":"10.1016\/S1571-0661(04)00295-6_NEWBIB28","unstructured":"PROTHEO\/LORIA. The ELAN homepage. http:\/\/elan.loria.fr."},{"key":"10.1016\/S1571-0661(04)00295-6_NEWBIB29","unstructured":"Carnegie Mellon School of Computer Science. The twelf project. http:\/\/www-2.cs.cmu.edu\/~twelf\/."},{"key":"10.1016\/S1571-0661(04)00295-6_NEWBIB30","unstructured":"J. Stuber. Experiments with an implementation of Extended Narrowing And Resolution in the rewriting language ELAN (system description). Available at http:\/\/www.loria.fr\/~stuber\/software, December 2000."},{"key":"10.1016\/S1571-0661(04)00295-6_NEWBIB31","unstructured":"A. Stump and D. L. Dill. Generating proofs from a decision procedure. In Proc. of Workshop on Run-Time Result Verification, July 1999. Available at http:\/\/sprout.Stanford.EDU\/~stump."},{"key":"10.1016\/S1571-0661(04)00295-6_NEWBIB32","article-title":"Optimized encodings of fragments of type theory in first-order logic","volume":"8","author":"Tammet","year":"1998","journal-title":"JLC: Journal of Logic and Computation"},{"key":"10.1016\/S1571-0661(04)00295-6_NEWBIB33","doi-asserted-by":"crossref","unstructured":"R. Verma and S. Senanayake. LR2: A laboratory for rapid term graph rewriting. In P. Narendran and M. Rusinowitch, editors, Proc. 10th Int. Conf. RTA, volume 1631 of Lecture Notes in Computer Science, pages 252\u2013255. Springer-Verlag, 1999.","DOI":"10.1007\/3-540-48685-2_21"},{"key":"10.1016\/S1571-0661(04)00295-6_NEWBIB34","unstructured":"Centrum voor Wiskunde en Informatica (CWI). The ATerm homepage. http:\/\/www.cwi.nl\/projects\/MetaEnv\/aterm\/."},{"issue":"2","key":"10.1016\/S1571-0661(04)00295-6_NEWBIB35","doi-asserted-by":"crossref","first-page":"193","DOI":"10.1023\/A:1008643803725","article-title":"Validation of HOL proofs by proof checking","volume":"14","author":"Wong","year":"1999","journal-title":"Formal Methods in System Design: An International Journal"}],"container-title":["Electronic Notes in Theoretical Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S1571066104002956?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S1571066104002956?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2020,3,30]],"date-time":"2020-03-30T12:28:28Z","timestamp":1585571308000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/S1571066104002956"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2001,11]]},"references-count":35,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2001,11]]}},"alternative-id":["S1571066104002956"],"URL":"https:\/\/doi.org\/10.1016\/s1571-0661(04)00295-6","relation":{},"ISSN":["1571-0661"],"issn-type":[{"value":"1571-0661","type":"print"}],"subject":[],"published":{"date-parts":[[2001,11]]}}}