Certified higher-order recursive path ordering

A. Koprowski

    Onderzoeksoutput: Hoofdstuk in Boek/Rapport/CongresprocedureConferentiebijdrageAcademicpeer review

    2 Citaten (Scopus)

    Samenvatting

    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.
    Originele taal-2Engels
    TitelRewriting Techniques and Applications (Proceedings 17th International Conference, RTA 2006, Seattle WA, USA, August 12-14, 2006)
    RedacteurenF. Pfenning
    Plaats van productieBerlin
    UitgeverijSpringer
    Pagina's227-241
    ISBN van geprinte versie3-540-36834-5
    DOI's
    StatusGepubliceerd - 2006

    Publicatie series

    NaamLecture Notes in Computer Science
    Volume4098
    ISSN van geprinte versie0302-9743

    Citeer dit