HORPO with Computability Closure : A Reconstruction
classification
💻 cs.LO
keywords
computabilityarbitraryboundclo-closurecomparisonsdecidabledefinition
read the original abstract
This paper provides a new, decidable definition of the higher- order recursive path ordering in which type comparisons are made only when needed, therefore eliminating the need for the computability clo- sure, and bound variables are handled explicitly, making it possible to handle recursors for arbitrary strictly positive inductive types.
This paper has not been read by Pith yet.
discussion (0)
Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.