Certifying Term Rewriting Proofs in ELAN Export

@misc{citeulike:6067028, abstract = {Term rewriting has been shown to be a good environment for both programming and proving. For analysing and debugging rule-based programs, we propose in this work a formalism based on the rewriting calculus with explicit substitutions ( -calculus). This formalism also allows us to build the proof terms of rewriting derivations. Therefore, term rewriting proofs can be exported to other systems by translating them into the corresponding syntaxes. That is, using a proof checker, one can certify these proofs and vice versa, this method allows us to get term rewriting in proof assistants using an external system. Our method not only works with syntactic rewriting but also with rewriting modulo a set of axioms (e.g. associativity-commutativity).}, author = {Nguyen, Quang-Huy and Inria, Loria}, citeulike-article-id = {6067028}, citeulike-linkout-0 = {http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.23.3527}, keywords = {coq, elan, rewriting}, posted-at = {2009-11-04 08:54:04}, priority = {3}, title = {Certifying Term Rewriting Proofs in ELAN}, url = {http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.23.3527}, year = {2001} }

TY - ELEC ID - citeulike:6067028 L3 - citeulike-article-id:6067028 N2 - Term rewriting has been shown to be a good environment for both programming and proving. For analysing and debugging rule-based programs, we propose in this work a formalism based on the rewriting calculus with explicit substitutions ( -calculus). This formalism also allows us to build the proof terms of rewriting derivations. Therefore, term rewriting proofs can be exported to other systems by translating them into the corresponding syntaxes. That is, using a proof checker, one can certify these proofs and vice versa, this method allows us to get term rewriting in proof assistants using an external system. Our method not only works with syntactic rewriting but also with rewriting modulo a set of axioms (e.g. associativity-commutativity). TI - Certifying Term Rewriting Proofs in ELAN KW - coq KW - elan KW - rewriting AU - Nguyen, Quang-Huy AU - Inria, Loria PY - 2001/// UR - http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.23.3527 ER -