| Certified Higher-Order Recursive Path Ordering |  |
Abstract:
The paper reports on a formalization of a proof of well-foundedness 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.
Certified Higher-Order Recursive Path Ordering
In
Proceedings of the 17th International Conference on Rewriting Techniques and Applications
( RTA '06),
Seattle, WA, USA.
BibTeX:@inproceedings{horpo-RTA-06,
author = {Adam Koprowski},
title = {Certified Higher-Order Recursive Path Ordering},
booktitle = {Proceedings of the 17th International Conference on Rewriting Techniques and Applications (RTA '06)},
year = {2006},
series = {Lecture Notes in Computer Science},
volume = {4098},
pages = {227--241},
} | 
