The paper reports on a formalization of a proof of wellfoundedness
of the higher-order recursive path ordering (HORPO) in the
proof checker Coq. The development is axiom-free and fully constructive.
Three substantive parts that could be used also in other developments
are the formalizations of the simply-typed lambda calculus, of finite multisets
and of the multiset ordering. The Coq code consists of more than
1000 lemmas and 300 definitions.
|Title of host publication||Rewriting Techniques and Applications (Proceedings 17th International Conference, RTA 2006, Seattle WA, USA, August 12-14, 2006)|
|Place of Publication||Berlin|
|Publication status||Published - 2006|
|Name||Lecture Notes in Computer Science|