Certified higher-order recursive path ordering

A. Koprowski

    Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

    3 Citations (Scopus)


    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.
    Original languageEnglish
    Title of host publicationRewriting Techniques and Applications (Proceedings 17th International Conference, RTA 2006, Seattle WA, USA, August 12-14, 2006)
    EditorsF. Pfenning
    Place of PublicationBerlin
    ISBN (Print)3-540-36834-5
    Publication statusPublished - 2006

    Publication series

    NameLecture Notes in Computer Science
    ISSN (Print)0302-9743

    Cite this