Coq formalization of the higher-order recursive path ordering

The recursive path ordering (RPO) is a well-known reduction ordering introduced by Dershowitz, that is useful for proving termination of term rewriting systems (TRSs). Jouannaud and Rubio generalized this ordering to the higher-order case thus creating the higher-order recursive path ordering (HORPO). They proved that this ordering can be used for proving termination of higher-order TRSs, which essentially comes down to proving well-foundedness of HORPO. This result entails well-foundedness of RPO and termination of simply typed lambda calculus (as the β-reduction relation is included in HORPO). This paper describes our undertaking of providing a complete, axiom-free, fully constructive formalization of those results in the proof assistant Coq. The formalization can be divided into three parts: finite multisets and two variants of multiset extensions of a relation,simply typed lambda calculus with termination of β-reduction as the main result,HORPO with a proof of its well-foundedness; also decidability of HORPO has been proved and, due to its constructive nature, a certified algorithm to verify whether two terms can be oriented with HORPO can be extracted from the proof.